Theorem FunLike.coe_smul

Modification history

2026-09-18 15:04
Mathlib/Data/FunLike/IsApply.lean
chore: catch up on a lot of `to_additive` debt (#43814) …
Deleted FunLike.coe_smulView on Github →
2026-05-21 01:59
Mathlib/Data/FunLike/IsApply.lean
feat(Data/FunLike): introduce typeclasses for algebraic properties of `FunLike` (#37779) …
Added FunLike.coe_smulView on Github →