Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-01-07 20:33
b99ac0e0
View on Github →
feat(NumberTheory/NumberField/Embeddings): definition of totally real field (
#20542
)
Estimated changes
Modified
Mathlib/NumberTheory/NumberField/Embeddings.lean
added
theorem
Rat.isReal_infinitePlace