Elliptic curve definitions bridging LMFDB knowls to Lean - #71

Merged

Multramate merged 13 commits into

CBirkbeck:mainfrom

JaneShi99:formalize/ec-defs

Sep 21, 2026

Commits on Jun 15, 2026

feat(ForMathlib): elliptic-curve reduction-type definitions (LeanBridge ch.4)

JaneShi99
and
claude
committed
641a2d5

Commits on Jun 19, 2026

Add global minimal-model, height, Frey, and obstruction-class defs (ch.4 EC)

JaneShi99
and
claude
committed
4384c2f
Clean up reduction/height defs to mathlib-idiomatic form (ch.4 EC)

JaneShi99
and
claude
committed
f0c17b0

Commits on Jun 28, 2026

Merge remote-tracking branch 'origin/main' into formalize/ec-defs
JaneShi99
committed
15d7c11
Sync ForMathlib/4-EC.lean to mathlib v4.31.0

JaneShi99
and
claude
committed
e899f9a

Commits on Jun 29, 2026

Address PR review: use mathlib reduction API, restructure ReductionType (ch.4 EC)

JaneShi99
and
claude
committed
943f9ab
Reformulate IsPotentialGoodReduction as a base-change existential (ch.4 EC)

JaneShi99
and
claude
committed
5cfb4e8

Commits on Jul 28, 2026

fixed some comments: imports, [isElliptic],
JaneShi99
committed
e06c826
removed addVal
JaneShi99
committed
14b9ce2
changed up the comments a bit
JaneShi99
committed
783e656
height uses mathlib height now
JaneShi99
committed
f1cef93

Commits on Jul 29, 2026

Three changes
JaneShi99
committed
2114839
AKLB setup is done
JaneShi99
committed
d84dd30