Commit 2022-12-14 16:33 4952d784

View on Github →

feat port: Algebra.Order.Monoid.ToMulBot (#1024) ee0c179cd3c8a45aa5bffbf1b41d8dbede452865

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Order/Monoid/ToMulBot.lean

added def WithZero.toMulBot

added theorem WithZero.toMulBot_coe

added theorem WithZero.toMulBot_coe_of_add

added theorem WithZero.toMulBot_le

added theorem WithZero.toMulBot_lt

added theorem WithZero.toMulBot_strictMono

added theorem WithZero.toMulBot_symm_bot

added theorem WithZero.toMulBot_zero