Documentation

Mathlib.Data.Int.Cast.Pi

Cast of integers to function types #

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

Main declarations #

source
instance Pi.instIntCast {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → IntCast (π i)] :
IntCast ((i : ι) → π i)
Equations
  • Pi.instIntCast = { intCast := fun (n : ℤ) (x : ι) => ↑n }
source
theorem Pi.intCast_apply {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → IntCast (π i)] (n : ℤ) (i : ι) :
↑n i = ↑n
source
@[simp]
theorem Pi.intCast_def {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → IntCast (π i)] (n : ℤ) :
↑n = fun (x : ι) => ↑n
source
@[deprecated Pi.intCast_apply]
theorem Pi.int_apply {ι : Type u_1} {π : ι → Type u_2} [(i : ι) → IntCast (π i)] (n : ℤ) (i : ι) :
↑n i = ↑n

Alias of Pi.intCast_apply.

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

Alias of Pi.intCast_def.

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