Commit 2025-08-05 14:12 6ae95cf1

View on Github →

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

Estimated changes

added theorem WithOne.map_inj
added theorem WithOne.map_injective'
added theorem WithOne.map_injective
added theorem WithOne.coe_injective