Theorem NumberField.IsCMField.ringOfIntegersComplexConj_eq_self_iff

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.ringOfIntegersComplexConj_eq_self_iffView on Github →
2025-09-18 14:30
Mathlib/NumberTheory/NumberField/CMField.lean
chore(NumberField/CMField): refactor (#29746) …
Deleted NumberField.IsCMField.ringOfIntegersComplexConj_eq_self_iffView on Github →
2025-09-16 20:21
Mathlib/NumberTheory/NumberField/CMField.lean
feat(NumberField/IsCM): first results about the action of `complexConjugation` on units (#26107) …
Added NumberField.IsCMField.ringOfIntegersComplexConj_eq_self_iffView on Github →