Def FunLike.coeMulHom

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.coeMulHom View on Github →