Theorem FunLike.natCast_eq_nsmul_one

Modification history

2026-07-27 16:25
Mathlib/Data/FunLike/IsApply.lean
chore(Data/FunLike): tag `IsApply` lemmas as simp (#42027) …
Added FunLike.natCast_eq_nsmul_oneView on Github →