Theorem NumberField.isTotallyReal_iff_ofRingEquiv

Modification history

2025-11-17 23:23

Mathlib/NumberTheory/NumberField/InfinitePlace/TotallyRealComplex.lean

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

Added NumberField.isTotallyReal_iff_ofRingEquiv View on Github →