# Documentation

Mathlib.Data.Pi.Algebra

# Instances and theorems on pi types #

This file provides basic definitions and notation instances for Pi types.

Instances of more sophisticated classes are defined in Pi.lean files elsewhere.

1, 0, +, *, +ᵥ, •, ^, -, ⁻¹, and / are defined pointwise.

instance Pi.instZero {I : Type u} {f : IType v₁} [(i : I) → Zero (f i)] :
Zero ((i : I) → f i)
instance Pi.instOne {I : Type u} {f : IType v₁} [(i : I) → One (f i)] :
One ((i : I) → f i)
@[simp]
theorem Pi.zero_apply {I : Type u} {f : IType v₁} (i : I) [(i : I) → Zero (f i)] :
OfNat.ofNat ((i : I) → f i) 0 Zero.toOfNat0 i = 0
@[simp]
theorem Pi.one_apply {I : Type u} {f : IType v₁} (i : I) [(i : I) → One (f i)] :
OfNat.ofNat ((i : I) → f i) 1 One.toOfNat1 i = 1
theorem Pi.zero_def {I : Type u} {f : IType v₁} [(i : I) → Zero (f i)] :
0 = fun x => 0
theorem Pi.one_def {I : Type u} {f : IType v₁} [(i : I) → One (f i)] :
1 = fun x => 1
@[simp]
theorem Pi.const_zero {α : Type u_1} {β : Type u_2} [Zero β] :
= 0
@[simp]
theorem Pi.const_one {α : Type u_1} {β : Type u_2} [One β] :
= 1
@[simp]
theorem Pi.zero_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero γ] (x : αβ) :
0 x = 0
@[simp]
theorem Pi.one_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [One γ] (x : αβ) :
1 x = 1
@[simp]
theorem Pi.comp_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero β] (x : βγ) :
x 0 = Function.const α (x 0)
@[simp]
theorem Pi.comp_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [One β] (x : βγ) :
x 1 = Function.const α (x 1)
instance Pi.instAdd {I : Type u} {f : IType v₁} [(i : I) → Add (f i)] :
Add ((i : I) → f i)
instance Pi.instMul {I : Type u} {f : IType v₁} [(i : I) → Mul (f i)] :
Mul ((i : I) → f i)
@[simp]
theorem Pi.add_apply {I : Type u} {f : IType v₁} (x : (i : I) → f i) (y : (i : I) → f i) (i : I) [(i : I) → Add (f i)] :
(((i : I) → f i) + ((i : I) → f i)) ((i : I) → f i) instHAdd x y i = x i + y i
@[simp]
theorem Pi.mul_apply {I : Type u} {f : IType v₁} (x : (i : I) → f i) (y : (i : I) → f i) (i : I) [(i : I) → Mul (f i)] :
(((i : I) → f i) * ((i : I) → f i)) ((i : I) → f i) instHMul x y i = x i * y i
theorem Pi.add_def {I : Type u} {f : IType v₁} (x : (i : I) → f i) (y : (i : I) → f i) [(i : I) → Add (f i)] :
x + y = fun i => x i + y i
theorem Pi.mul_def {I : Type u} {f : IType v₁} (x : (i : I) → f i) (y : (i : I) → f i) [(i : I) → Mul (f i)] :
x * y = fun i => x i * y i
@[simp]
theorem Pi.const_add {α : Type u_1} {β : Type u_2} [Add β] (a : β) (b : β) :
+ = Function.const α (a + b)
@[simp]
theorem Pi.const_mul {α : Type u_1} {β : Type u_2} [Mul β] (a : β) (b : β) :
* = Function.const α (a * b)
theorem Pi.add_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Add γ] (x : βγ) (y : βγ) (z : αβ) :
(x + y) z = x z + y z
theorem Pi.mul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Mul γ] (x : βγ) (y : βγ) (z : αβ) :
(x * y) z = x z * y z
instance Pi.instVAdd {I : Type u} {α : Type u_1} {f : IType v₁} [(i : I) → VAdd α (f i)] :
VAdd α ((i : I) → f i)
instance Pi.instSMul {I : Type u} {α : Type u_1} {f : IType v₁} [(i : I) → SMul α (f i)] :
SMul α ((i : I) → f i)
instance Pi.instPow {I : Type u} {β : Type u_2} {f : IType v₁} [(i : I) → Pow (f i) β] :
Pow ((i : I) → f i) β
@[simp]
theorem Pi.smul_apply {I : Type u} {β : Type u_2} {f : IType v₁} [(i : I) → SMul β (f i)] (b : β) (x : (i : I) → f i) (i : I) :
(β ((i : I) → f i)) ((i : I) → f i) instHSMul b x i = b x i
@[simp]
theorem Pi.vadd_apply {I : Type u} {β : Type u_2} {f : IType v₁} [(i : I) → VAdd β (f i)] (b : β) (x : (i : I) → f i) (i : I) :
(β +ᵥ ((i : I) → f i)) ((i : I) → f i) instHVAdd b x i = b +ᵥ x i
@[simp]
theorem Pi.pow_apply {I : Type u} {β : Type u_2} {f : IType v₁} [(i : I) → Pow (f i) β] (x : (i : I) → f i) (b : β) (i : I) :
(((i : I) → f i) ^ β) ((i : I) → f i) instHPow x b i = x i ^ b
theorem Pi.smul_def {I : Type u} {β : Type u_2} {f : IType v₁} [(i : I) → SMul β (f i)] (b : β) (x : (i : I) → f i) :
b x = fun i => b x i
theorem Pi.vadd_def {I : Type u} {β : Type u_2} {f : IType v₁} [(i : I) → VAdd β (f i)] (b : β) (x : (i : I) → f i) :
b +ᵥ x = fun i => b +ᵥ x i
theorem Pi.pow_def {I : Type u} {β : Type u_2} {f : IType v₁} [(i : I) → Pow (f i) β] (x : (i : I) → f i) (b : β) :
x ^ b = fun i => x i ^ b
@[simp]
theorem Pi.vadd_const {I : Type u} {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) :
@[simp]
theorem Pi.smul_const {I : Type u} {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) :
@[simp]
theorem Pi.const_pow {I : Type u} {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) :
^ b = Function.const I (a ^ b)
theorem Pi.vadd_comp {I : Type u} {α : Type u_1} {β : Type u_2} {γ : Type u_3} [VAdd α γ] (a : α) (x : βγ) (y : Iβ) :
(a +ᵥ x) y = a +ᵥ x y
theorem Pi.smul_comp {I : Type u} {α : Type u_1} {β : Type u_2} {γ : Type u_3} [SMul α γ] (a : α) (x : βγ) (y : Iβ) :
(a x) y = a x y
theorem Pi.pow_comp {I : Type u} {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Pow γ α] (x : βγ) (a : α) (y : Iβ) :
(x ^ a) y = x y ^ a

Porting note: bit0 and bit1 are deprecated. This section can be removed entirely (without replacement?).

@[simp, deprecated]
theorem Pi.bit0_apply {I : Type u} {f : IType v₁} (x : (i : I) → f i) (i : I) [(i : I) → Add (f i)] :
bit0 ((i : I) → f i) Pi.instAdd x i = bit0 (x i)
@[simp, deprecated]
theorem Pi.bit1_apply {I : Type u} {f : IType v₁} (x : (i : I) → f i) (i : I) [(i : I) → Add (f i)] [(i : I) → One (f i)] :
bit1 ((i : I) → f i) Pi.instOne Pi.instAdd x i = bit1 (x i)
instance Pi.instNeg {I : Type u} {f : IType v₁} [(i : I) → Neg (f i)] :
Neg ((i : I) → f i)
instance Pi.instInv {I : Type u} {f : IType v₁} [(i : I) → Inv (f i)] :
Inv ((i : I) → f i)
@[simp]
theorem Pi.neg_apply {I : Type u} {f : IType v₁} (x : (i : I) → f i) (i : I) [(i : I) → Neg (f i)] :
(-((i : I) → f i)) Pi.instNeg x i = -x i
@[simp]
theorem Pi.inv_apply {I : Type u} {f : IType v₁} (x : (i : I) → f i) (i : I) [(i : I) → Inv (f i)] :
((i : I) → f i)⁻¹ Pi.instInv x i = (x i)⁻¹
theorem Pi.neg_def {I : Type u} {f : IType v₁} (x : (i : I) → f i) [(i : I) → Neg (f i)] :
-x = fun i => -x i
theorem Pi.inv_def {I : Type u} {f : IType v₁} (x : (i : I) → f i) [(i : I) → Inv (f i)] :
x⁻¹ = fun i => (x i)⁻¹
theorem Pi.const_neg {α : Type u_1} {β : Type u_2} [Neg β] (a : β) :
theorem Pi.const_inv {α : Type u_1} {β : Type u_2} [Inv β] (a : β) :
()⁻¹ =
theorem Pi.neg_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Neg γ] (x : βγ) (y : αβ) :
(-x) y = -x y
theorem Pi.inv_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Inv γ] (x : βγ) (y : αβ) :
x⁻¹ y = (x y)⁻¹
instance Pi.instSub {I : Type u} {f : IType v₁} [(i : I) → Sub (f i)] :
Sub ((i : I) → f i)
instance Pi.instDiv {I : Type u} {f : IType v₁} [(i : I) → Div (f i)] :
Div ((i : I) → f i)
@[simp]
theorem Pi.sub_apply {I : Type u} {f : IType v₁} (x : (i : I) → f i) (y : (i : I) → f i) (i : I) [(i : I) → Sub (f i)] :
(((i : I) → f i) - ((i : I) → f i)) ((i : I) → f i) instHSub x y i = x i - y i
@[simp]
theorem Pi.div_apply {I : Type u} {f : IType v₁} (x : (i : I) → f i) (y : (i : I) → f i) (i : I) [(i : I) → Div (f i)] :
(((i : I) → f i) / ((i : I) → f i)) ((i : I) → f i) instHDiv x y i = x i / y i
theorem Pi.sub_def {I : Type u} {f : IType v₁} (x : (i : I) → f i) (y : (i : I) → f i) [(i : I) → Sub (f i)] :
x - y = fun i => x i - y i
theorem Pi.div_def {I : Type u} {f : IType v₁} (x : (i : I) → f i) (y : (i : I) → f i) [(i : I) → Div (f i)] :
x / y = fun i => x i / y i
theorem Pi.sub_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Sub γ] (x : βγ) (y : βγ) (z : αβ) :
(x - y) z = x z - y z
theorem Pi.div_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Div γ] (x : βγ) (y : βγ) (z : αβ) :
(x / y) z = x z / y z
@[simp]
theorem Pi.const_sub {α : Type u_1} {β : Type u_2} [Sub β] (a : β) (b : β) :
- = Function.const α (a - b)
@[simp]
theorem Pi.const_div {α : Type u_1} {β : Type u_2} [Div β] (a : β) (b : β) :
/ = Function.const α (a / b)
def Pi.single {I : Type u} {f : IType v₁} [] [(i : I) → Zero (f i)] (i : I) (x : f i) (j : I) :
f j

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

Instances For
def Pi.mulSingle {I : Type u} {f : IType v₁} [] [(i : I) → One (f i)] (i : I) (x : f i) (j : I) :
f j

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

Instances For
@[simp]
theorem Pi.single_eq_same {I : Type u} {f : IType v₁} [] [(i : I) → Zero (f i)] (i : I) (x : f i) :
Pi.single i x i = x
@[simp]
theorem Pi.mulSingle_eq_same {I : Type u} {f : IType v₁} [] [(i : I) → One (f i)] (i : I) (x : f i) :
Pi.mulSingle i x i = x
@[simp]
theorem Pi.single_eq_of_ne {I : Type u} {f : IType v₁} [] [(i : I) → Zero (f i)] {i : I} {i' : I} (h : i' i) (x : f i) :
Pi.single i x i' = 0
@[simp]
theorem Pi.mulSingle_eq_of_ne {I : Type u} {f : IType v₁} [] [(i : I) → One (f i)] {i : I} {i' : I} (h : i' i) (x : f i) :
Pi.mulSingle i x i' = 1
@[simp]
theorem Pi.single_eq_of_ne' {I : Type u} {f : IType v₁} [] [(i : I) → Zero (f i)] {i : I} {i' : I} (h : i i') (x : f i) :
Pi.single i x i' = 0

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

@[simp]
theorem Pi.mulSingle_eq_of_ne' {I : Type u} {f : IType v₁} [] [(i : I) → One (f i)] {i : I} {i' : I} (h : i i') (x : f i) :
Pi.mulSingle i x i' = 1

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

@[simp]
theorem Pi.single_zero {I : Type u} {f : IType v₁} [] [(i : I) → Zero (f i)] (i : I) :
= 0
@[simp]
theorem Pi.mulSingle_one {I : Type u} {f : IType v₁} [] [(i : I) → One (f i)] (i : I) :
= 1
theorem Pi.single_apply {I : Type u} {β : Type u_2} [] [Zero β] (i : I) (x : β) (i' : I) :
Pi.single i x i' = if i' = i then x else 0

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

theorem Pi.mulSingle_apply {I : Type u} {β : Type u_2} [] [One β] (i : I) (x : β) (i' : I) :
Pi.mulSingle i x i' = if i' = i then x else 1

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

theorem Pi.single_comm {I : Type u} {β : Type u_2} [] [Zero β] (i : I) (x : β) (i' : I) :
Pi.single i x i' = Pi.single i' x i

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

theorem Pi.mulSingle_comm {I : Type u} {β : Type u_2} [] [One β] (i : I) (x : β) (i' : I) :

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

theorem Pi.apply_single {I : Type u} {f : IType v₁} {g : IType v₂} [] [(i : I) → Zero (f i)] [(i : I) → Zero (g i)] (f' : (i : I) → f ig i) (hf' : ∀ (i : I), f' i 0 = 0) (i : I) (x : f i) (j : I) :
f' j (Pi.single i x j) = Pi.single i (f' i x) j
theorem Pi.apply_mulSingle {I : Type u} {f : IType v₁} {g : IType v₂} [] [(i : I) → One (f i)] [(i : I) → One (g i)] (f' : (i : I) → f ig i) (hf' : ∀ (i : I), f' i 1 = 1) (i : I) (x : f i) (j : I) :
f' j (Pi.mulSingle i x j) = Pi.mulSingle i (f' i x) j
theorem Pi.apply_single₂ {I : Type u} {f : IType v₁} {g : IType v₂} {h : IType v₃} [] [(i : I) → Zero (f i)] [(i : I) → Zero (g i)] [(i : I) → Zero (h i)] (f' : (i : I) → f ig ih i) (hf' : ∀ (i : I), f' i 0 0 = 0) (i : I) (x : f i) (y : g i) (j : I) :
f' j (Pi.single i x j) (Pi.single i y j) = Pi.single i (f' i x y) j
theorem Pi.apply_mulSingle₂ {I : Type u} {f : IType v₁} {g : IType v₂} {h : IType v₃} [] [(i : I) → One (f i)] [(i : I) → One (g i)] [(i : I) → One (h i)] (f' : (i : I) → f ig ih i) (hf' : ∀ (i : I), f' i 1 1 = 1) (i : I) (x : f i) (y : g i) (j : I) :
f' j (Pi.mulSingle i x j) (Pi.mulSingle i y j) = Pi.mulSingle i (f' i x y) j
theorem Pi.single_op {I : Type u} {f : IType v₁} [] [(i : I) → Zero (f i)] {g : IType u_4} [(i : I) → Zero (g i)] (op : (i : I) → f ig i) (h : ∀ (i : I), op i 0 = 0) (i : I) (x : f i) :
Pi.single i (op i x) = fun j => op j (Pi.single i x j)
theorem Pi.mulSingle_op {I : Type u} {f : IType v₁} [] [(i : I) → One (f i)] {g : IType u_4} [(i : I) → One (g i)] (op : (i : I) → f ig i) (h : ∀ (i : I), op i 1 = 1) (i : I) (x : f i) :
Pi.mulSingle i (op i x) = fun j => op j (Pi.mulSingle i x j)
theorem Pi.single_op₂ {I : Type u} {f : IType v₁} [] [(i : I) → Zero (f i)] {g₁ : IType u_4} {g₂ : IType u_5} [(i : I) → Zero (g₁ i)] [(i : I) → Zero (g₂ i)] (op : (i : I) → g₁ ig₂ if i) (h : ∀ (i : I), op i 0 0 = 0) (i : I) (x₁ : g₁ i) (x₂ : g₂ i) :
Pi.single i (op i x₁ x₂) = fun j => op j (Pi.single i x₁ j) (Pi.single i x₂ j)
theorem Pi.mulSingle_op₂ {I : Type u} {f : IType v₁} [] [(i : I) → One (f i)] {g₁ : IType u_4} {g₂ : IType u_5} [(i : I) → One (g₁ i)] [(i : I) → One (g₂ i)] (op : (i : I) → g₁ ig₂ if i) (h : ∀ (i : I), op i 1 1 = 1) (i : I) (x₁ : g₁ i) (x₂ : g₂ i) :
Pi.mulSingle i (op i x₁ x₂) = fun j => op j (Pi.mulSingle i x₁ j) (Pi.mulSingle i x₂ j)
theorem Pi.single_injective {I : Type u} (f : IType v₁) [] [(i : I) → Zero (f i)] (i : I) :
theorem Pi.mulSingle_injective {I : Type u} (f : IType v₁) [] [(i : I) → One (f i)] (i : I) :
@[simp]
theorem Pi.single_inj {I : Type u} (f : IType v₁) [] [(i : I) → Zero (f i)] (i : I) {x : f i} {y : f i} :
= x = y
@[simp]
theorem Pi.mulSingle_inj {I : Type u} (f : IType v₁) [] [(i : I) → One (f i)] (i : I) {x : f i} {y : f i} :
= x = y
def Pi.prod {I : Type u} {f : IType v₁} {g : IType v₂} (f' : (i : I) → f i) (g' : (i : I) → g i) (i : I) :
f i × g i

The mapping into a product type built from maps into each component.

Instances For
theorem Pi.prod_fst_snd {α : Type u_1} {β : Type u_2} :
Pi.prod Prod.fst Prod.snd = id
theorem Pi.prod_snd_fst {α : Type u_1} {β : Type u_2} :
Pi.prod Prod.snd Prod.fst = Prod.swap
theorem Function.extend_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero γ] (f : αβ) :
= 0
theorem Function.extend_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [One γ] (f : αβ) :
= 1
theorem Function.extend_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Add γ] (f : αβ) (g₁ : αγ) (g₂ : αγ) (e₁ : βγ) (e₂ : βγ) :
Function.extend f (g₁ + g₂) (e₁ + e₂) = Function.extend f g₁ e₁ + Function.extend f g₂ e₂
theorem Function.extend_mul {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Mul γ] (f : αβ) (g₁ : αγ) (g₂ : αγ) (e₁ : βγ) (e₂ : βγ) :
Function.extend f (g₁ * g₂) (e₁ * e₂) = Function.extend f g₁ e₁ * Function.extend f g₂ e₂
theorem Function.extend_neg {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Neg γ] (f : αβ) (g : αγ) (e : βγ) :
theorem Function.extend_inv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Inv γ] (f : αβ) (g : αγ) (e : βγ) :
= ()⁻¹
theorem Function.extend_sub {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Sub γ] (f : αβ) (g₁ : αγ) (g₂ : αγ) (e₁ : βγ) (e₂ : βγ) :
Function.extend f (g₁ - g₂) (e₁ - e₂) = Function.extend f g₁ e₁ - Function.extend f g₂ e₂
theorem Function.extend_div {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Div γ] (f : αβ) (g₁ : αγ) (g₂ : αγ) (e₁ : βγ) (e₂ : βγ) :
Function.extend f (g₁ / g₂) (e₁ / e₂) = Function.extend f g₁ e₁ / Function.extend f g₂ e₂
theorem Function.surjective_pi_map {I : Type u} {f : IType v₁} {g : IType v₂} {F : (i : I) → f ig i} (hF : ∀ (i : I), Function.Surjective (F i)) :
Function.Surjective fun x i => F i (x i)
theorem Function.injective_pi_map {I : Type u} {f : IType v₁} {g : IType v₂} {F : (i : I) → f ig i} (hF : ∀ (i : I), Function.Injective (F i)) :
Function.Injective fun x i => F i (x i)
theorem Function.bijective_pi_map {I : Type u} {f : IType v₁} {g : IType v₂} {F : (i : I) → f ig i} (hF : ∀ (i : I), Function.Bijective (F i)) :
Function.Bijective fun x i => F i (x i)
def uniqueOfSurjectiveZero (α : Type u_4) {β : Type u_5} [Zero β] (h : ) :

If the zero function is surjective, the codomain is trivial.

Instances For
def uniqueOfSurjectiveOne (α : Type u_4) {β : Type u_5} [One β] (h : ) :

If the one function is surjective, the codomain is trivial.

Instances For
theorem Subsingleton.pi_single_eq {I : Type u} {α : Type u_4} [] [] [Zero α] (i : I) (x : α) :
= fun x => x
theorem Subsingleton.pi_mulSingle_eq {I : Type u} {α : Type u_4} [] [] [One α] (i : I) (x : α) :
= fun x => x
@[simp]
theorem Sum.elim_zero_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero γ] :
Sum.elim 0 0 = 0
@[simp]
theorem Sum.elim_one_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [One γ] :
Sum.elim 1 1 = 1
@[simp]
theorem Sum.elim_single_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [Zero γ] (i : α) (c : γ) :
Sum.elim () 0 = Pi.single () c
@[simp]
theorem Sum.elim_mulSingle_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [One γ] (i : α) (c : γ) :
@[simp]
theorem Sum.elim_zero_single {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [Zero γ] (i : β) (c : γ) :
Sum.elim 0 () = Pi.single () c
@[simp]
theorem Sum.elim_one_mulSingle {α : Type u_1} {β : Type u_2} {γ : Type u_3} [] [] [One γ] (i : β) (c : γ) :
theorem Sum.elim_neg_neg {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : αγ) (b : βγ) [Neg γ] :
Sum.elim (-a) (-b) = -Sum.elim a b
theorem Sum.elim_inv_inv {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : αγ) (b : βγ) [Inv γ] :
theorem Sum.elim_add_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : αγ) (a' : αγ) (b : βγ) (b' : βγ) [Add γ] :
Sum.elim (a + a') (b + b') = Sum.elim a b + Sum.elim a' b'
theorem Sum.elim_mul_mul {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : αγ) (a' : αγ) (b : βγ) (b' : βγ) [Mul γ] :
Sum.elim (a * a') (b * b') = Sum.elim a b * Sum.elim a' b'
theorem Sum.elim_sub_sub {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : αγ) (a' : αγ) (b : βγ) (b' : βγ) [Sub γ] :
Sum.elim (a - a') (b - b') = Sum.elim a b - Sum.elim a' b'
theorem Sum.elim_div_div {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : αγ) (a' : αγ) (b : βγ) (b' : βγ) [Div γ] :
Sum.elim (a / a') (b / b') = Sum.elim a b / Sum.elim a' b'