Mathlib Changelog
v4
Changelog
About
Github
Theorem
NumberField.IsTotally.of_algebra
Modification history
2025-05-19 12:48
Mathlib/NumberTheory/NumberField/InfinitePlace/TotallyRealComplex.lean
chore(NumberField/IsTotallyReal): fixed a typo introduced in #23760 (#25016)
Deleted
NumberField.IsTotally.of_algebra
View on Github →
2025-05-19 08:29
Mathlib/NumberTheory/NumberField/InfinitePlace/TotallyRealComplex.lean
feat(NumberField): define the `maximalRealSubfield` of a number field (#23760) …
Added
NumberField.IsTotally.of_algebra
View on Github →