Commit 2025-06-11 14:29 124c4b2d

View on Github →

feat(GroupWithZero/WithZero): injectivity and monotonicity of WithZero.map' (#25660) factored out of #22420

Estimated changes

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

added theorem WithOne.«exists»

added theorem WithOne.«forall»

Modified Mathlib/Algebra/GroupWithZero/WithZero.lean

added theorem WithZero.map'_injective_iff

Modified Mathlib/Algebra/Order/GroupWithZero/Canonical.lean

added theorem WithZero.map'_mono

added theorem WithZero.map'_strictMono

added theorem WithZero.not_coe_le_zero

added theorem WithZero.not_lt_zero

modified theorem WithZero.zero_le

modified theorem WithZero.zero_lt_coe