Theorem WithOne.coe_injective

Modification history

2025-08-05 14:12

Mathlib/Algebra/Group/WithOne/Defs.lean

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

Added WithOne.coe_injective View on Github →