Theorem NumberField.IsCMField.closure_realFundSystem_sup_torsion

Modification history

2025-10-10 08:52
Mathlib/NumberTheory/NumberField/CMField.lean
feat(NumberField/IsCM): compute ratio of regulators (#26104) …
Added NumberField.IsCMField.closure_realFundSystem_sup_torsionView on Github →