mathlib documentation

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.

@[protected, instance]
def pi.has_zero {I : Type u} {f : I → Type v₁} [Π (i : I), has_zero (f i)] :
has_zero (Π (i : I), f i)
Equations
@[protected, instance]
def pi.has_one {I : Type u} {f : I → Type v₁} [Π (i : I), has_one (f i)] :
has_one (Π (i : I), f i)
Equations
@[simp]
theorem pi.zero_apply {I : Type u} {f : I → Type v₁} (i : I) [Π (i : I), has_zero (f i)] :
0 i = 0
@[simp]
theorem pi.one_apply {I : Type u} {f : I → Type v₁} (i : I) [Π (i : I), has_one (f i)] :
1 i = 1
theorem pi.one_def {I : Type u} {f : I → Type v₁} [Π (i : I), has_one (f i)] :
1 = λ (i : I), 1
theorem pi.zero_def {I : Type u} {f : I → Type v₁} [Π (i : I), has_zero (f i)] :
0 = λ (i : I), 0
@[simp]
theorem pi.const_one {α : Type u_1} {β : Type u_2} [has_one β] :
@[simp]
theorem pi.const_zero {α : Type u_1} {β : Type u_2} [has_zero β] :
@[simp]
theorem pi.zero_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (x : α → β) :
0 x = 0
@[simp]
theorem pi.one_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_one γ] (x : α → β) :
1 x = 1
@[simp]
theorem pi.comp_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero β] (x : β → γ) :
x 0 = function.const α (x 0)
@[simp]
theorem pi.comp_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_one β] (x : β → γ) :
x 1 = function.const α (x 1)
@[protected, instance]
def pi.has_mul {I : Type u} {f : I → Type v₁} [Π (i : I), has_mul (f i)] :
has_mul (Π (i : I), f i)
Equations
@[protected, instance]
def pi.has_add {I : Type u} {f : I → Type v₁} [Π (i : I), has_add (f i)] :
has_add (Π (i : I), f i)
Equations
@[simp]
theorem pi.add_apply {I : Type u} {f : I → Type v₁} (x y : Π (i : I), f i) (i : I) [Π (i : I), has_add (f i)] :
(x + y) i = x i + y i
@[simp]
theorem pi.mul_apply {I : Type u} {f : I → Type v₁} (x y : Π (i : I), f i) (i : I) [Π (i : I), has_mul (f i)] :
(x * y) i = x i * y i
theorem pi.mul_def {I : Type u} {f : I → Type v₁} (x y : Π (i : I), f i) [Π (i : I), has_mul (f i)] :
x * y = λ (i : I), x i * y i
theorem pi.add_def {I : Type u} {f : I → Type v₁} (x y : Π (i : I), f i) [Π (i : I), has_add (f i)] :
x + y = λ (i : I), x i + y i
@[simp]
theorem pi.const_add {α : Type u_1} {β : Type u_2} [has_add β] (a b : β) :
@[simp]
theorem pi.const_mul {α : Type u_1} {β : Type u_2} [has_mul β] (a b : β) :
theorem pi.mul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_mul γ] (x y : β → γ) (z : α → β) :
(x * y) z = x z * y z
theorem pi.add_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_add γ] (x y : β → γ) (z : α → β) :
(x + y) z = x z + y z
@[protected, instance]
def pi.has_vadd {I : Type u} {α : Type u_1} {f : I → Type v₁} [Π (i : I), has_vadd α (f i)] :
has_vadd α (Π (i : I), f i)
Equations
@[protected, instance]
def pi.has_smul {I : Type u} {α : Type u_1} {f : I → Type v₁} [Π (i : I), has_smul α (f i)] :
has_smul α (Π (i : I), f i)
Equations
@[simp]
theorem pi.vadd_apply {I : Type u} {α : Type u_1} {f : I → Type v₁} [Π (i : I), has_vadd α (f i)] (s : α) (x : Π (i : I), f i) (i : I) :
(s +ᵥ x) i = s +ᵥ x i
@[simp]
theorem pi.smul_apply {I : Type u} {α : Type u_1} {f : I → Type v₁} [Π (i : I), has_smul α (f i)] (s : α) (x : Π (i : I), f i) (i : I) :
(s x) i = s x i
theorem pi.vadd_def {I : Type u} {α : Type u_1} {f : I → Type v₁} [Π (i : I), has_vadd α (f i)] (s : α) (x : Π (i : I), f i) :
s +ᵥ x = λ (i : I), s +ᵥ x i
theorem pi.smul_def {I : Type u} {α : Type u_1} {f : I → Type v₁} [Π (i : I), has_smul α (f i)] (s : α) (x : Π (i : I), f i) :
s x = λ (i : I), s x i
@[simp]
theorem pi.vadd_const {I : Type u} {α : Type u_1} {β : Type u_2} [has_vadd α β] (a : α) (b : β) :
@[simp]
theorem pi.smul_const {I : Type u} {α : Type u_1} {β : Type u_2} [has_smul α β] (a : α) (b : β) :
theorem pi.smul_comp {I : Type u} {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_smul α γ] (a : α) (x : β → γ) (y : I → β) :
(a x) y = a x y
theorem pi.vadd_comp {I : Type u} {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_vadd α γ] (a : α) (x : β → γ) (y : I → β) :
(a +ᵥ x) y = a +ᵥ x y
@[protected, instance]
def pi.has_pow {I : Type u} {β : Type u_2} {f : I → Type v₁} [Π (i : I), has_pow (f i) β] :
has_pow (Π (i : I), f i) β
Equations
@[simp]
theorem pi.pow_apply {I : Type u} {β : Type u_2} {f : I → Type v₁} [Π (i : I), has_pow (f i) β] (x : Π (i : I), f i) (b : β) (i : I) :
(x ^ b) i = x i ^ b
theorem pi.pow_def {I : Type u} {β : Type u_2} {f : I → Type v₁} [Π (i : I), has_pow (f i) β] (x : Π (i : I), f i) (b : β) :
x ^ b = λ (i : I), x i ^ b
@[simp]
theorem pi.const_pow {I : Type u} {α : Type u_1} {β : Type u_2} [has_pow β α] (b : β) (a : α) :
theorem pi.pow_comp {I : Type u} {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_pow γ α] (x : β → γ) (a : α) (y : I → β) :
(x ^ a) y = x y ^ a
@[simp]
theorem pi.bit0_apply {I : Type u} {f : I → Type v₁} (x : Π (i : I), f i) (i : I) [Π (i : I), has_add (f i)] :
bit0 x i = bit0 (x i)
@[simp]
theorem pi.bit1_apply {I : Type u} {f : I → Type v₁} (x : Π (i : I), f i) (i : I) [Π (i : I), has_add (f i)] [Π (i : I), has_one (f i)] :
bit1 x i = bit1 (x i)
@[protected, instance]
def pi.has_inv {I : Type u} {f : I → Type v₁} [Π (i : I), has_inv (f i)] :
has_inv (Π (i : I), f i)
Equations
@[protected, instance]
def pi.has_neg {I : Type u} {f : I → Type v₁} [Π (i : I), has_neg (f i)] :
has_neg (Π (i : I), f i)
Equations
@[simp]
theorem pi.neg_apply {I : Type u} {f : I → Type v₁} (x : Π (i : I), f i) (i : I) [Π (i : I), has_neg (f i)] :
(-x) i = -x i
@[simp]
theorem pi.inv_apply {I : Type u} {f : I → Type v₁} (x : Π (i : I), f i) (i : I) [Π (i : I), has_inv (f i)] :
x⁻¹ i = (x i)⁻¹
theorem pi.neg_def {I : Type u} {f : I → Type v₁} (x : Π (i : I), f i) [Π (i : I), has_neg (f i)] :
-x = λ (i : I), -x i
theorem pi.inv_def {I : Type u} {f : I → Type v₁} (x : Π (i : I), f i) [Π (i : I), has_inv (f i)] :
x⁻¹ = λ (i : I), (x i)⁻¹
theorem pi.const_inv {α : Type u_1} {β : Type u_2} [has_inv β] (a : β) :
theorem pi.const_neg {α : Type u_1} {β : Type u_2} [has_neg β] (a : β) :
theorem pi.inv_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_inv γ] (x : β → γ) (y : α → β) :
x⁻¹ y = (x y)⁻¹
theorem pi.neg_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_neg γ] (x : β → γ) (y : α → β) :
(-x) y = -x y
@[protected, instance]
def pi.has_sub {I : Type u} {f : I → Type v₁} [Π (i : I), has_sub (f i)] :
has_sub (Π (i : I), f i)
Equations
@[protected, instance]
def pi.has_div {I : Type u} {f : I → Type v₁} [Π (i : I), has_div (f i)] :
has_div (Π (i : I), f i)
Equations
@[simp]
theorem pi.div_apply {I : Type u} {f : I → Type v₁} (x y : Π (i : I), f i) (i : I) [Π (i : I), has_div (f i)] :
(x / y) i = x i / y i
@[simp]
theorem pi.sub_apply {I : Type u} {f : I → Type v₁} (x y : Π (i : I), f i) (i : I) [Π (i : I), has_sub (f i)] :
(x - y) i = x i - y i
theorem pi.div_def {I : Type u} {f : I → Type v₁} (x y : Π (i : I), f i) [Π (i : I), has_div (f i)] :
x / y = λ (i : I), x i / y i
theorem pi.sub_def {I : Type u} {f : I → Type v₁} (x y : Π (i : I), f i) [Π (i : I), has_sub (f i)] :
x - y = λ (i : I), x i - y i
theorem pi.sub_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_sub γ] (x y : β → γ) (z : α → β) :
(x - y) z = x z - y z
theorem pi.div_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_div γ] (x y : β → γ) (z : α → β) :
(x / y) z = x z / y z
@[simp]
theorem pi.const_sub {α : Type u_1} {β : Type u_2} [has_sub β] (a b : β) :
@[simp]
theorem pi.const_div {α : Type u_1} {β : Type u_2} [has_div β] (a b : β) :
def pi.single {I : Type u} {f : I → Type v₁} [decidable_eq I] [Π (i : I), has_zero (f i)] (i : I) (x : f i) (i_1 : I) :
f i_1

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

Equations
def pi.mul_single {I : Type u} {f : I → Type v₁} [decidable_eq I] [Π (i : I), has_one (f i)] (i : I) (x : f i) (i_1 : I) :
f i_1

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

Equations
@[simp]
theorem pi.mul_single_eq_same {I : Type u} {f : I → Type v₁} [decidable_eq I] [Π (i : I), has_one (f i)] (i : I) (x : f i) :
@[simp]
theorem pi.single_eq_same {I : Type u} {f : I → Type v₁} [decidable_eq I] [Π (i : I), has_zero (f i)] (i : I) (x : f i) :
pi.single i x i = x
@[simp]
theorem pi.single_eq_of_ne {I : Type u} {f : I → Type v₁} [decidable_eq I] [Π (i : I), has_zero (f i)] {i i' : I} (h : i' i) (x : f i) :
pi.single i x i' = 0
@[simp]
theorem pi.mul_single_eq_of_ne {I : Type u} {f : I → Type v₁} [decidable_eq I] [Π (i : I), has_one (f i)] {i i' : I} (h : i' i) (x : f i) :
pi.mul_single i x i' = 1
@[simp]
theorem pi.mul_single_eq_of_ne' {I : Type u} {f : I → Type v₁} [decidable_eq I] [Π (i : I), has_one (f i)] {i i' : I} (h : i i') (x : f i) :
pi.mul_single i x i' = 1

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

@[simp]
theorem pi.single_eq_of_ne' {I : Type u} {f : I → Type v₁} [decidable_eq I] [Π (i : I), has_zero (f 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.single_zero {I : Type u} {f : I → Type v₁} [decidable_eq I] [Π (i : I), has_zero (f i)] (i : I) :
pi.single i 0 = 0
@[simp]
theorem pi.mul_single_one {I : Type u} {f : I → Type v₁} [decidable_eq I] [Π (i : I), has_one (f i)] (i : I) :
theorem pi.single_apply {I : Type u} [decidable_eq I] {β : Type u_1} [has_zero β] (i : I) (x : β) (i' : I) :
pi.single i x i' = ite (i' = i) x 0

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

theorem pi.mul_single_apply {I : Type u} [decidable_eq I] {β : Type u_1} [has_one β] (i : I) (x : β) (i' : I) :
pi.mul_single i x i' = ite (i' = i) x 1

On non-dependent functions, pi.mul_single can be expressed as an ite

theorem pi.single_comm {I : Type u} [decidable_eq I] {β : Type u_1} [has_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.mul_single_comm {I : Type u} [decidable_eq I] {β : Type u_1} [has_one β] (i : I) (x : β) (i' : I) :

On non-dependent functions, pi.mul_single is symmetric in the two indices.

theorem pi.apply_single {I : Type u} {f : I → Type v₁} {g : I → Type v₂} [decidable_eq I] [Π (i : I), has_zero (f i)] [Π (i : I), has_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_mul_single {I : Type u} {f : I → Type v₁} {g : I → Type v₂} [decidable_eq I] [Π (i : I), has_one (f i)] [Π (i : I), has_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.mul_single i x j) = pi.mul_single i (f' i x) j
theorem pi.apply_single₂ {I : Type u} {f : I → Type v₁} {g : I → Type v₂} {h : I → Type v₃} [decidable_eq I] [Π (i : I), has_zero (f i)] [Π (i : I), has_zero (g i)] [Π (i : I), has_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_mul_single₂ {I : Type u} {f : I → Type v₁} {g : I → Type v₂} {h : I → Type v₃} [decidable_eq I] [Π (i : I), has_one (f i)] [Π (i : I), has_one (g i)] [Π (i : I), has_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.mul_single i x j) (pi.mul_single i y j) = pi.mul_single i (f' i x y) j
theorem pi.single_op {I : Type u} {f : I → Type v₁} [decidable_eq I] [Π (i : I), has_zero (f i)] {g : I → Type u_1} [Π (i : I), has_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) = λ (j : I), op j (pi.single i x j)
theorem pi.mul_single_op {I : Type u} {f : I → Type v₁} [decidable_eq I] [Π (i : I), has_one (f i)] {g : I → Type u_1} [Π (i : I), has_one (g i)] (op : Π (i : I), f ig i) (h : ∀ (i : I), op i 1 = 1) (i : I) (x : f i) :
pi.mul_single i (op i x) = λ (j : I), op j (pi.mul_single i x j)
theorem pi.mul_single_op₂ {I : Type u} {f : I → Type v₁} [decidable_eq I] [Π (i : I), has_one (f i)] {g₁ : I → Type u_1} {g₂ : I → Type u_2} [Π (i : I), has_one (g₁ i)] [Π (i : I), has_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.mul_single i (op i x₁ x₂) = λ (j : I), op j (pi.mul_single i x₁ j) (pi.mul_single i x₂ j)
theorem pi.single_op₂ {I : Type u} {f : I → Type v₁} [decidable_eq I] [Π (i : I), has_zero (f i)] {g₁ : I → Type u_1} {g₂ : I → Type u_2} [Π (i : I), has_zero (g₁ i)] [Π (i : I), has_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₂) = λ (j : I), op j (pi.single i x₁ j) (pi.single i x₂ j)
theorem pi.mul_single_injective {I : Type u} (f : I → Type v₁) [decidable_eq I] [Π (i : I), has_one (f i)] (i : I) :
theorem pi.single_injective {I : Type u} (f : I → Type v₁) [decidable_eq I] [Π (i : I), has_zero (f i)] (i : I) :
@[simp]
theorem pi.single_inj {I : Type u} (f : I → Type v₁) [decidable_eq I] [Π (i : I), has_zero (f i)] (i : I) {x y : f i} :
pi.single i x = pi.single i y x = y
@[simp]
theorem pi.mul_single_inj {I : Type u} (f : I → Type v₁) [decidable_eq I] [Π (i : I), has_one (f i)] (i : I) {x y : f i} :
@[protected, simp]
def pi.prod {I : Type u} {f : I → Type v₁} {g : I → Type 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.

Equations
@[simp]
theorem pi.prod_fst_snd {α : Type u_1} {β : Type u_2} :
@[simp]
theorem pi.prod_snd_fst {α : Type u_1} {β : Type u_2} :
theorem function.extend_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_one γ] (f : α → β) :
theorem function.extend_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] (f : α → β) :
theorem function.extend_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_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} [has_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} [has_neg γ] (f : α → β) (g : α → γ) (e : β → γ) :
theorem function.extend_inv {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_inv γ] (f : α → β) (g : α → γ) (e : β → γ) :
theorem function.extend_div {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_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.extend_sub {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_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.surjective_pi_map {I : Type u} {f : I → Type v₁} {g : I → Type v₂} {F : Π (i : I), f ig i} (hF : ∀ (i : I), function.surjective (F i)) :
function.surjective (λ (x : Π (i : I), f i) (i : I), F i (x i))
theorem function.injective_pi_map {I : Type u} {f : I → Type v₁} {g : I → Type v₂} {F : Π (i : I), f ig i} (hF : ∀ (i : I), function.injective (F i)) :
function.injective (λ (x : Π (i : I), f i) (i : I), F i (x i))
theorem function.bijective_pi_map {I : Type u} {f : I → Type v₁} {g : I → Type v₂} {F : Π (i : I), f ig i} (hF : ∀ (i : I), function.bijective (F i)) :
function.bijective (λ (x : Π (i : I), f i) (i : I), F i (x i))
def unique_of_surjective_one (α : Type u_1) {β : Type u_2} [has_one β] (h : function.surjective 1) :

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

Equations
def unique_of_surjective_zero (α : Type u_1) {β : Type u_2} [has_zero β] (h : function.surjective 0) :

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

Equations
theorem subsingleton.pi_mul_single_eq {I : Type u} {α : Type u_1} [decidable_eq I] [subsingleton I] [has_one α] (i : I) (x : α) :
pi.mul_single i x = λ (_x : I), x
theorem subsingleton.pi_single_eq {I : Type u} {α : Type u_1} [decidable_eq I] [subsingleton I] [has_zero α] (i : I) (x : α) :
pi.single i x = λ (_x : I), x
@[simp]
theorem sum.elim_one_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_one γ] :
sum.elim 1 1 = 1
@[simp]
theorem sum.elim_zero_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [has_zero γ] :
sum.elim 0 0 = 0
@[simp]
theorem sum.elim_single_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq α] [decidable_eq β] [has_zero γ] (i : α) (c : γ) :
@[simp]
theorem sum.elim_mul_single_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq α] [decidable_eq β] [has_one γ] (i : α) (c : γ) :
@[simp]
theorem sum.elim_zero_single {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq α] [decidable_eq β] [has_zero γ] (i : β) (c : γ) :
@[simp]
theorem sum.elim_one_mul_single {α : Type u_1} {β : Type u_2} {γ : Type u_3} [decidable_eq α] [decidable_eq β] [has_one γ] (i : β) (c : γ) :
theorem sum.elim_inv_inv {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α → γ) (b : β → γ) [has_inv γ] :
theorem sum.elim_neg_neg {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a : α → γ) (b : β → γ) [has_neg γ] :
sum.elim (-a) (-b) = -sum.elim a b
theorem sum.elim_add_add {α : Type u_1} {β : Type u_2} {γ : Type u_3} (a a' : α → γ) (b b' : β → γ) [has_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' : β → γ) [has_mul γ] :
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' : β → γ) [has_div γ] :
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' : β → γ) [has_sub γ] :
sum.elim (a - a') (b - b') = sum.elim a b - sum.elim a' b'