Commit 2025-06-09 10:18 210d1c31

View on Github →

feat(Algebra/Group/Pi): add injectivity and coe lemmas (#25525) for OneHom.mulSingle and MonoidHom.mulSingle.

Estimated changes

added theorem OneHom.coe_mulSingle