Theorem NumberField.CMExtension.card_infinitePlace_eq_card_infinitePlace

Modification history

2025-09-18 14:30
Mathlib/NumberTheory/NumberField/CMField.lean
chore(NumberField/CMField): refactor (#29746) …
Deleted NumberField.CMExtension.card_infinitePlace_eq_card_infinitePlaceView on Github →
2025-06-05 09:09
Mathlib/NumberTheory/NumberField/CMField.lean
chore(NumberField.CMField): Fix some proofs (#25457) …
Added NumberField.CMExtension.card_infinitePlace_eq_card_infinitePlaceView on Github →