Cast of natural numbers to function types

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

Main declarations

• Pi.instNatCast: map n : ℕ to the constant function n : ∀ i, π i

@[instance_reducible]

instance Pi.instNatCast {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → NatCast (π i)] : NatCast ((i : ι) → π i)

Equations

• Pi.instNatCast = { natCast := fun (n : ℕ) (x : ι) => ↑n }

@[simp]

theorem Pi.natCast_apply {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → NatCast (π i)] (n : ℕ) (i : ι) : ↑n i = ↑n

theorem Pi.natCast_def {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → NatCast (π i)] (n : ℕ) : ↑n = fun (x : ι) => ↑n

@[simp]

theorem Sum.elim_natCast_natCast {α : Type u_1} {β : Type u_2} {γ : Type u_3} [NatCast γ] (n : ℕ) : Sum.elim ↑n ↑n = ↑n