Theorem NumberField.IsCMField.regulator_div_regulator_eq_two_pow_mul_indexRealUnits_inv

Modification history

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