Theorem FunLike.coe_natCast

Modification history

2026-10-13 20:38
Mathlib/Algebra/Group/IsApply.lean
refactor(Algebra): make the arguments of `Is*Apply` implicit (#42704) …
Modified FunLike.coe_natCastView on Github →
2026-10-06 23:08
Mathlib/Algebra/Group/IsApply.lean
feat(Data/FunLike): add `abbrev`s for pointwise multiplication (#40899) …
Added FunLike.coe_natCastView on Github →
2026-07-27 16:25
Mathlib/Data/FunLike/IsApply.lean
chore(Data/FunLike): tag `IsApply` lemmas as simp (#42027) …
Deleted FunLike.coe_natCastView 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_natCastView on Github →