Theorem NumberField.maximalRealSubfield_eq_top_iff_isTotallyReal

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.maximalRealSubfield_eq_top_iff_isTotallyReal View on Github →