Theorem OneHom.coe_mulSingle

Modification history

2025-06-09 10:18
Mathlib/Algebra/Group/Pi/Lemmas.lean
feat(Algebra/Group/Pi): add injectivity and coe lemmas (#25525) …
Added OneHom.coe_mulSingleView on Github →