Commit 2022-12-06 13:59 92593ea4

View on Github →

feat: port Algebra.Order.Monoid.WithZero (#851) mathlib3 SHA: dad7ecf9a1feae63e6e49f07619b7087403fb8d4 Ports Algebra.Order.Monoid.WithZero.[Defs, Basic].

depends on #841
depends on leanprover-community/mathlib#17820 I'm planning to wait until leanprover-community/mathlib#17820 is approved before doing a final refactor to move lemmas where they're needed.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/WithOne/Defs.lean

Created Mathlib/Algebra/Order/Monoid/WithZero/Basic.lean

Created Mathlib/Algebra/Order/Monoid/WithZero/Defs.lean

added theorem WithZero.coe_le_coe

added theorem WithZero.coe_lt_coe

added theorem WithZero.zero_eq_bot

added theorem WithZero.zero_le

added theorem WithZero.zero_lt_coe