Theorem NumberField.mem_maximalRealSubfield_iff

Modification history

2025-09-18 14:30
Mathlib/NumberTheory/NumberField/InfinitePlace/TotallyRealComplex.lean
chore(NumberField/CMField): refactor (#29746) …
Added NumberField.mem_maximalRealSubfield_iffView on Github →