Theorem FunLike.intCast_eq_zsmul_one

Modification history

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