Theorem NumberField.IsTotallyReal.mult_eq

Modification history

2025-10-10 08:52
Mathlib/NumberTheory/NumberField/InfinitePlace/TotallyRealComplex.lean
feat(NumberField/IsCM): compute ratio of regulators (#26104) …
Added NumberField.IsTotallyReal.mult_eqView on Github →