Theorem OneHom.coe_inv

Modification history

2025-09-06 10:02
Mathlib/Algebra/Group/Hom/Basic.lean
feat: instances for `ZeroHom` and `OneHom` (#27305) …
Added OneHom.coe_invView on Github →