Theorem NumberField.IsCMField.index_unitsMulComplexConjInv_range_dvd

Modification history

2025-09-29 15:10
Mathlib/NumberTheory/NumberField/CMField.lean
feat(NumberField/IsCM): compute the index of the subgroup of real units (#26108) …
Added NumberField.IsCMField.index_unitsMulComplexConjInv_range_dvdView on Github →