Theorem NumberField.IsTotallyReal.maximalRealSubfield_eq_top

Modification history

2025-11-26 15:01
Mathlib/NumberTheory/NumberField/InfinitePlace/TotallyRealComplex.lean
chore(TotallyReal/TotallyComplex): remove the `NumberField` hypothesis (#31810) …
Modified NumberField.IsTotallyReal.maximalRealSubfield_eq_topView on Github →
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.maximalRealSubfield_eq_topView on Github →