Def NumberField.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.maximalRealSubfield View on Github →