CurveCycle.lean: a 2-cycle of curves shares its CM discriminant - #31

Closed

dannywillems wants to merge 11 commits into

daira:indiff-countingfrom

dannywillems:curve-cycle-discriminant

Commits on Aug 17, 2026

PastaSSWU.lean: Make the spatial metaphor for applying the isogeny
daira
committed
ae6c227

Commits on Aug 18, 2026

CurveCycle.lean: a 2-cycle of curves shares its CM discriminant

dannywillems
and
claude
committed
62d6ece
CurveCycle.lean: correct what ordinariness does and does not buy

dannywillems
and
claude
committed
d0dca00

Commits on Aug 19, 2026

CurveCycle.lean: document the three declarations that had no docstring

dannywillems
and
claude
committed
c76f7e8
CurveCycle.lean: drop three declarations nothing consumes

dannywillems
and
claude
committed
6438050
CurveCycle.lean: keep the module doc to what the result needs

dannywillems
and
claude
committed
c1e5ab6
CurveCycle.lean: drop the group-hash aside from the Pasta paragraph

authored and
soc
committed
743b0a9
CurveCycle.lean: say what V is on the theorem that states it

dannywillems
and
claude
committed
171d43c
CurveCycle.lean: spell out the AdjoinRoot arguments instead of _

dannywillems
and
claude
committed
9920f53
CurveCycle.lean: drop frobeniusElt_def for Lean's generated eq_def

authored and
soc
committed
4140e07
CurveCycle.lean: say why being a root is the well-definedness condition

authored and
soc
committed
f9e3f1e