Theorem NumberField.isTotallyReal_iff_le_maximalRealSubfield

Modification history

2025-05-19 08:29
Mathlib/NumberTheory/NumberField/InfinitePlace/TotallyRealComplex.lean
feat(NumberField): define the `maximalRealSubfield` of a number field (#23760) …
Added NumberField.isTotallyReal_iff_le_maximalRealSubfieldView on Github →