# Very basic algebraic operations on pi types #

This file provides very basic algebraic operations on functions.

source
def Pi.mulSingle {ι : Type u_1} {M : ι → Type u_6} [(i : ι) → One (M i)] [DecidableEq ι] (i : ι) (x : M i) (j : ι) :
M j

The function supported at `i`, with value `x` there, and `1` elsewhere.

Equations

- Pi.mulSingle i x = Function.update 1 i x

Instances For

source
def Pi.single {ι : Type u_1} {M : ι → Type u_6} [(i : ι) → Zero (M i)] [DecidableEq ι] (i : ι) (x : M i) (j : ι) :
M j

The function supported at `i`, with value `x` there, and `0` elsewhere.

Equations

- Pi.single i x = Function.update 0 i x

Instances For

source
@[simp]
theorem Pi.mulSingle_eq_same {ι : Type u_1} {M : ι → Type u_6} [(i : ι) → One (M i)] [DecidableEq ι] (i : ι) (x : M i) :
mulSingle i x i = x
source
@[simp]
theorem Pi.single_eq_same {ι : Type u_1} {M : ι → Type u_6} [(i : ι) → Zero (M i)] [DecidableEq ι] (i : ι) (x : M i) :
single i x i = x
source
@[simp]
theorem Pi.mulSingle_eq_of_ne {ι : Type u_1} {M : ι → Type u_6} [(i : ι) → One (M i)] [DecidableEq ι] {i i' : ι} (h : i' ≠ i) (x : M i) :
mulSingle i x i' = 1
source
@[simp]
theorem Pi.single_eq_of_ne {ι : Type u_1} {M : ι → Type u_6} [(i : ι) → Zero (M i)] [DecidableEq ι] {i i' : ι} (h : i' ≠ i) (x : M i) :
single i x i' = 0
source
@[simp]
theorem Pi.mulSingle_eq_of_ne' {ι : Type u_1} {M : ι → Type u_6} [(i : ι) → One (M i)] [DecidableEq ι] {i i' : ι} (h : i ≠ i') (x : M i) :
mulSingle i x i' = 1

Abbreviation for `mulSingle_eq_of_ne h.symm`, for ease of use by `simp`.

source
@[simp]
theorem Pi.single_eq_of_ne' {ι : Type u_1} {M : ι → Type u_6} [(i : ι) → Zero (M i)] [DecidableEq ι] {i i' : ι} (h : i ≠ i') (x : M i) :
single i x i' = 0

Abbreviation for `single_eq_of_ne h.symm`, for ease of use by `simp`.

source
@[simp]
theorem Pi.mulSingle_one {ι : Type u_1} {M : ι → Type u_6} [(i : ι) → One (M i)] [DecidableEq ι] (i : ι) :
mulSingle i 1 = 1
source
@[simp]
theorem Pi.single_zero {ι : Type u_1} {M : ι → Type u_6} [(i : ι) → Zero (M i)] [DecidableEq ι] (i : ι) :
single i 0 = 0
source
@[simp]
theorem Pi.mulSingle_eq_one_iff {ι : Type u_1} {M : ι → Type u_6} [(i : ι) → One (M i)] [DecidableEq ι] {i : ι} {x : M i} :
mulSingle i x = 1 ↔ x = 1
source
@[simp]
theorem Pi.single_eq_zero_iff {ι : Type u_1} {M : ι → Type u_6} [(i : ι) → Zero (M i)] [DecidableEq ι] {i : ι} {x : M i} :
single i x = 0 ↔ x = 0
source
theorem Pi.mulSingle_ne_one_iff {ι : Type u_1} {M : ι → Type u_6} [(i : ι) → One (M i)] [DecidableEq ι] {i : ι} {x : M i} :
mulSingle i x ≠ 1 ↔ x ≠ 1
source
theorem Pi.single_ne_zero_iff {ι : Type u_1} {M : ι → Type u_6} [(i : ι) → Zero (M i)] [DecidableEq ι] {i : ι} {x : M i} :
single i x ≠ 0 ↔ x ≠ 0
source
theorem Pi.apply_mulSingle {ι : Type u_1} {M : ι → Type u_6} {N : ι → Type u_7} [(i : ι) → One (M i)] [(i : ι) → One (N i)] [DecidableEq ι] (f' : (i : ι) → M i → N i) (hf' : ∀ (i : ι), f' i 1 = 1) (i : ι) (x : M i) (j : ι) :
f' j (mulSingle i x j) = mulSingle i (f' i x) j
source
theorem Pi.apply_single {ι : Type u_1} {M : ι → Type u_6} {N : ι → Type u_7} [(i : ι) → Zero (M i)] [(i : ι) → Zero (N i)] [DecidableEq ι] (f' : (i : ι) → M i → N i) (hf' : ∀ (i : ι), f' i 0 = 0) (i : ι) (x : M i) (j : ι) :
f' j (single i x j) = single i (f' i x) j
source
theorem Pi.apply_mulSingle₂ {ι : Type u_1} {M : ι → Type u_6} {N : ι → Type u_7} {O : ι → Type u_8} [(i : ι) → One (M i)] [(i : ι) → One (N i)] [(i : ι) → One (O i)] [DecidableEq ι] (f' : (i : ι) → M i → N i → O i) (hf' : ∀ (i : ι), f' i 1 1 = 1) (i : ι) (x : M i) (y : N i) (j : ι) :
f' j (mulSingle i x j) (mulSingle i y j) = mulSingle i (f' i x y) j
source
theorem Pi.apply_single₂ {ι : Type u_1} {M : ι → Type u_6} {N : ι → Type u_7} {O : ι → Type u_8} [(i : ι) → Zero (M i)] [(i : ι) → Zero (N i)] [(i : ι) → Zero (O i)] [DecidableEq ι] (f' : (i : ι) → M i → N i → O i) (hf' : ∀ (i : ι), f' i 0 0 = 0) (i : ι) (x : M i) (y : N i) (j : ι) :
f' j (single i x j) (single i y j) = single i (f' i x y) j
source
theorem Pi.mulSingle_op {ι : Type u_1} {M : ι → Type u_6} {N : ι → Type u_7} [(i : ι) → One (M i)] [(i : ι) → One (N i)] [DecidableEq ι] (op : (i : ι) → M i → N i) (h : ∀ (i : ι), op i 1 = 1) (i : ι) (x : M i) :
mulSingle i (op i x) = fun (j : ι) => op j (mulSingle i x j)
source
theorem Pi.single_op {ι : Type u_1} {M : ι → Type u_6} {N : ι → Type u_7} [(i : ι) → Zero (M i)] [(i : ι) → Zero (N i)] [DecidableEq ι] (op : (i : ι) → M i → N i) (h : ∀ (i : ι), op i 0 = 0) (i : ι) (x : M i) :
single i (op i x) = fun (j : ι) => op j (single i x j)
source
theorem Pi.mulSingle_op₂ {ι : Type u_1} {M : ι → Type u_6} {N : ι → Type u_7} {O : ι → Type u_8} [(i : ι) → One (M i)] [(i : ι) → One (N i)] [(i : ι) → One (O i)] [DecidableEq ι] (op : (i : ι) → M i → N i → O i) (h : ∀ (i : ι), op i 1 1 = 1) (i : ι) (x : M i) (y : N i) :
mulSingle i (op i x y) = fun (j : ι) => op j (mulSingle i x j) (mulSingle i y j)
source
theorem Pi.single_op₂ {ι : Type u_1} {M : ι → Type u_6} {N : ι → Type u_7} {O : ι → Type u_8} [(i : ι) → Zero (M i)] [(i : ι) → Zero (N i)] [(i : ι) → Zero (O i)] [DecidableEq ι] (op : (i : ι) → M i → N i → O i) (h : ∀ (i : ι), op i 0 0 = 0) (i : ι) (x : M i) (y : N i) :
single i (op i x y) = fun (j : ι) => op j (single i x j) (single i y j)
source
theorem Pi.mulSingle_injective {ι : Type u_1} {M : ι → Type u_6} [(i : ι) → One (M i)] [DecidableEq ι] (i : ι) :
Function.Injective (mulSingle i)
source
theorem Pi.single_injective {ι : Type u_1} {M : ι → Type u_6} [(i : ι) → Zero (M i)] [DecidableEq ι] (i : ι) :
Function.Injective (single i)
source
@[simp]
theorem Pi.mulSingle_inj {ι : Type u_1} {M : ι → Type u_6} [(i : ι) → One (M i)] [DecidableEq ι] (i : ι) {x y : M i} :
mulSingle i x = mulSingle i y ↔ x = y
source
@[simp]
theorem Pi.single_inj {ι : Type u_1} {M : ι → Type u_6} [(i : ι) → Zero (M i)] [DecidableEq ι] (i : ι) {x y : M i} :
single i x = single i y ↔ x = y
source
theorem Pi.mulSingle_apply {ι : Type u_1} [DecidableEq ι] {M : Type u_9} [One M] (i : ι) (x : M) (i' : ι) :
mulSingle i x i' = if i' = i then x else 1

On non-dependent functions, `Pi.mulSingle` can be expressed as an `ite`

source
theorem Pi.single_apply {ι : Type u_1} [DecidableEq ι] {M : Type u_9} [Zero M] (i : ι) (x : M) (i' : ι) :
single i x i' = if i' = i then x else 0

On non-dependent functions, `Pi.single` can be expressed as an `ite`

source
theorem Pi.mulSingle_comm {ι : Type u_1} [DecidableEq ι] {M : Type u_9} [One M] (i : ι) (x : M) (j : ι) :
mulSingle i x j = mulSingle j x i

On non-dependent functions, `Pi.mulSingle` is symmetric in the two indices.

source
theorem Pi.single_comm {ι : Type u_1} [DecidableEq ι] {M : Type u_9} [Zero M] (i : ι) (x : M) (j : ι) :
single i x j = single j x i

On non-dependent functions, `Pi.single` is symmetric in the two indices.

source
@[simp]
theorem Pi.curry_mulSingle {ι : Type u_1} {ι' : Type u_2} [DecidableEq ι] {M : Type u_9} [One M] [DecidableEq ι'] (i : ι × ι') (b : M) :
Function.curry (mulSingle i b) = mulSingle i.fst (mulSingle i.snd b)
source
@[simp]
theorem Pi.curry_single {ι : Type u_1} {ι' : Type u_2} [DecidableEq ι] {M : Type u_9} [Zero M] [DecidableEq ι'] (i : ι × ι') (b : M) :
Function.curry (single i b) = single i.fst (single i.snd b)
source
@[simp]
theorem Pi.uncurry_mulSingle_mulSingle {ι : Type u_1} {ι' : Type u_2} [DecidableEq ι] {M : Type u_9} [One M] [DecidableEq ι'] (i : ι) (i' : ι') (b : M) :
Function.uncurry (mulSingle i (mulSingle i' b)) = mulSingle (i, i') b
source
@[simp]
theorem Pi.uncurry_single_single {ι : Type u_1} {ι' : Type u_2} [DecidableEq ι] {M : Type u_9} [Zero M] [DecidableEq ι'] (i : ι) (i' : ι') (b : M) :
Function.uncurry (single i (single i' b)) = single (i, i') b