Theorem Pi.natCast_apply

Modification history

2026-10-06 23:08
Mathlib/Data/Nat/Cast/Basic.lean
feat(Data/FunLike): add `abbrev`s for pointwise multiplication (#40899) …
Modified Pi.natCast_applyView on Github →
2024-04-07 17:47
Mathlib/Data/Nat/Cast/Basic.lean
chore: Rename `coe_nat`/`coe_int`/`coe_rat` to `natCast`/`intCast`/`ratCast` (#11499) …
Added Pi.natCast_applyView on Github →