Theorem FunLike.coeMonoidHom_injective

Modification history

2026-05-21 01:59
Mathlib/Data/FunLike/Group.lean
feat(Data/FunLike): introduce typeclasses for algebraic properties of `FunLike` (#37779) …
Added FunLike.coeMonoidHom_injectiveView on Github →