Cast of integers to function types #
This file provides a (pointwise) cast from ℤ to function types.
Main declarations #
Pi.instIntCast: mapn : ℤto the constant functionn : ∀ i, π i
instance
Pi.instIntCast
{ι : Type u_1}
{π : ι → Type u_2}
[(i : ι) → IntCast (π i)]
:
IntCast ((i : ι) → π i)
Equations
- Pi.instIntCast = { intCast := fun (n : ℤ) (x : ι) => ↑n }
@[deprecated Pi.intCast_apply (since := "2024-04-05")]
theorem
Pi.int_apply
{ι : Type u_1}
{π : ι → Type u_2}
[(i : ι) → IntCast (π i)]
(n : ℤ)
(i : ι)
:
↑n i = ↑n
Alias of Pi.intCast_apply.
@[deprecated Pi.intCast_def (since := "2024-04-05")]
theorem
Pi.coe_int
{ι : Type u_1}
{π : ι → Type u_2}
[(i : ι) → IntCast (π i)]
(n : ℤ)
:
↑n = fun (x : ι) => ↑n
Alias of Pi.intCast_def.