Theorem WithOne.map_injective

Modification history

2025-08-26 15:11

Mathlib/Algebra/Group/WithOne/Basic.lean

chore: define WithZero order instances without reference to WithBot (#28957)

Deleted WithOne.map_injective View on Github →

2025-08-05 14:12

Mathlib/Algebra/Group/WithOne/Basic.lean

chore(Algebra/Group/WithOne): injectivity of `coe` and `map` (#27665)

Added WithOne.map_injective View on Github →