Commit 2025-05-19 12:48 ce3f8ce7

View on Github →

chore(NumberField/IsTotallyReal): fixed a typo introduced in #23760 (#25016)

Estimated changes

Modified Mathlib/NumberTheory/NumberField/InfinitePlace/TotallyRealComplex.lean

deleted theorem NumberField.IsTotally.of_algebra

added theorem NumberField.IsTotallyReal.of_algebra