Cast of integers to function types

This file provides a (pointwise) cast from ℤ to function types.

Main declarations

• Pi.instIntCast: map n : ℤ to the constant function n : ∀ 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 }

@[simp]

theorem Pi.intCast_apply {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → IntCast (π i)] (n : ℤ) (i : ι) : ↑n i = ↑n

theorem Pi.intCast_def {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → IntCast (π i)] (n : ℤ) : ↑n = fun (x : ι) => ↑n

@[simp]

theorem Sum.elim_intCast_intCast {α : Type u_1} {β : Type u_2} {γ : Type u_3} [IntCast γ] (n : ℤ) : Sum.elim ↑n ↑n = ↑n