Theorem NumberField.isTotallyReal_top_iff

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