Commit 2025-06-05 09:09 e1bfe126

View on Github →

chore(NumberField.CMField): Fix some proofs (#25457) Fix some proofs in NumberField.CMField.

Estimated changes

Modified Mathlib.lean

Renamed Mathlib/NumberTheory/NumberField/CMField.Lean to Mathlib/NumberTheory/NumberField/CMField.lean

added theorem NumberField.CMExtension.card_infinitePlace_eq_card_infinitePlace

added theorem NumberField.CMExtension.complexConj_apply_apply

added theorem NumberField.CMExtension.complexConj_ne_one

added theorem NumberField.CMExtension.complexEmbedding_complexConj

added theorem NumberField.CMExtension.exists_isConj

added theorem NumberField.CMExtension.isConj_complexConj

added theorem NumberField.CMExtension.isConj_eq_isConj

added theorem NumberField.CMExtension.orderOf_complexConj

added theorem NumberField.CMExtension.units_rank_eq_units_rank

added theorem NumberField.CMExtension.zpowers_complexConj_eq_top

added theorem NumberField.IsCMField.card_infinitePlace_eq_card_infinitePlace

added theorem NumberField.IsCMField.units_rank_eq_units_rank