Skip to content

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
Closed

dannywillems wants to merge 11 commits into
daira:indiff-countingfrom
dannywillems:curve-cycle-discriminant

CurveCycle.lean: say why being a root is the well-definedness condition

f9e3f1e
Select commit
Loading
Failed to load commit list.
Sign in for the full log view

Annotations

1 warning
Field-file generators reproduce
succeeded Aug 19, 2026 in 1m 51s