Theorem NumberField.IsTotallyReal.of_algebra

Modification history

2025-11-26 15:01
Mathlib/NumberTheory/NumberField/InfinitePlace/TotallyRealComplex.lean
chore(TotallyReal/TotallyComplex): remove the `NumberField` hypothesis (#31810) …
Modified NumberField.IsTotallyReal.of_algebraView on Github →
2025-05-19 12:48
Mathlib/NumberTheory/NumberField/InfinitePlace/TotallyRealComplex.lean
chore(NumberField/IsTotallyReal): fixed a typo introduced in #23760 (#25016)
Added NumberField.IsTotallyReal.of_algebraView on Github →