Commit 2025-11-17 23:23 d84b7497

View on Github →

feat(NumberTheory/NumberField/InfinitePlace): A few easy lemmas about totally real fields (#31239)

Estimated changes

Modified Mathlib/NumberTheory/NumberField/InfinitePlace/TotallyRealComplex.lean

added theorem NumberField.IsTotallyReal.maximalRealSubfield_eq_top

added theorem NumberField.isTotallyReal_iff_ofRingEquiv

added theorem NumberField.isTotallyReal_top_iff

added theorem NumberField.maximalRealSubfield_eq_top_iff_isTotallyReal