Commit 2025-10-10 08:52 aec4d456

View on Github →

feat(NumberField/IsCM): compute ratio of regulators (#26104) This PR continues the work from #23696. Compute the ratio between the regulator of K and the regulator of its maximal real subfield.

Estimated changes

Modified Mathlib/NumberTheory/NumberField/CMField.lean

added theorem NumberField.IsCMField.closure_realFundSystem_sup_torsion

added theorem NumberField.IsCMField.equivInfinitePlace_apply

added theorem NumberField.IsCMField.equivInfinitePlace_symm_apply

added theorem NumberField.IsCMField.regOfFamily_realFunSystem

added theorem NumberField.IsCMField.regulator_div_regulator_eq_two_pow_mul_indexRealUnits_inv

Modified Mathlib/NumberTheory/NumberField/InfinitePlace/TotallyRealComplex.lean

added theorem NumberField.IsTotallyComplex.mult_eq

added theorem NumberField.IsTotallyReal.mult_eq