Theorem NumberField.CMExtension.ringOfIntegersComplexConj_eq_self_iff

Modification history

2025-09-18 14:30

Mathlib/NumberTheory/NumberField/CMField.lean

chore(NumberField/CMField): refactor (#29746) …

Deleted NumberField.CMExtension.ringOfIntegersComplexConj_eq_self_iff View 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.CMExtension.ringOfIntegersComplexConj_eq_self_iff View on Github →