Elliptic curve definitions bridging LMFDB knowls to Lean - #71

Open

JaneShi99 wants to merge 13 commits into

CBirkbeck:mainfrom

JaneShi99:formalize/ec-defs

Commits on Jun 15, 2026

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

JaneShi99
and
claude
committed

Commits on Jun 19, 2026

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

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

JaneShi99
and
claude
committed

Commits on Jun 28, 2026

Commits on Jun 29, 2026

Commits on Jul 29, 2026