Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-01-25 10:48
48c2c12f
View on Github →
feat: synchronize with mathlib3
#18080
/18160/18174 (
#1519
)
https://github.com/leanprover-community/mathlib/pull/18080
https://github.com/leanprover-community/mathlib/pull/18160
https://github.com/leanprover-community/mathlib/pull/18174
Estimated changes
Modified
Mathlib/Algebra/Group/Basic.lean
added
theorem
multiplicative_of_symmetric_of_isTotal
Modified
Mathlib/Algebra/Module/Basic.lean
Modified
Mathlib/Algebra/SMulWithZero.lean
Modified
Mathlib/Data/Nat/WithBot.lean
added
theorem
Nat.WithBot.add_one_le_of_lt