Theorem ZeroHom.coe_sub

Modification history

2026-11-10 14:10
Mathlib/Algebra/Group/Hom/Basic.lean
feat: use `IsApply` for `OneHom` (#45472)
Added ZeroHom.coe_subView on Github →