Theorem NumberField.IsCMField.regOfFamily_realFunSystem

Modification history

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