Mathlib Changelog
v4
Changelog
About
Github
Commit
2025-02-25 19:33
4e8722f3
View on Github →
chore(Order/Max): rename
prod_mk
->
prodMk
(
#22188
)
Estimated changes
Modified
Mathlib/Order/Max.lean
added
theorem
IsBot.prodMk
deleted
theorem
IsBot.prod_mk
added
theorem
IsMax.prodMk
deleted
theorem
IsMax.prod_mk
added
theorem
IsMin.prodMk
deleted
theorem
IsMin.prod_mk
added
theorem
IsTop.prodMk
deleted
theorem
IsTop.prod_mk