# Instances and theorems on pi types #

This file provides instances for the typeclass defined in Algebra.Group.Defs. More sophisticated instances are defined in Algebra.Group.Pi.Lemmas files elsewhere.

## Porting note #

This file relied on the pi_instance tactic, which was not available at the time of porting. The comment --pi_instance is inserted before all fields which were previously derived by pi_instance. See this Zulip discussion: [https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/not.20porting.20pi_instance]

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)
Equations
• Pi.instZero = { zero := fun (x : I) => 0 }
instance Pi.instOne {I : Type u} {f : IType v₁} [(i : I) → One (f i)] :
One ((i : I) → f i)
Equations
• Pi.instOne = { one := fun (x : I) => 1 }
@[simp]
theorem Pi.zero_apply {I : Type u} {f : IType v₁} (i : I) [(i : I) → Zero (f i)] :
0 i = 0
@[simp]
theorem Pi.one_apply {I : Type u} {f : IType v₁} (i : I) [(i : I) → One (f i)] :
1 i = 1
theorem Pi.zero_def {I : Type u} {f : IType v₁} [(i : I) → Zero (f i)] :
0 = fun (x : I) => 0
theorem Pi.one_def {I : Type u} {f : IType v₁} [(i : I) → One (f i)] :
1 = fun (x : I) => 1
@[simp]
theorem Function.const_zero {α : Type u_1} {β : Type u_2} [Zero β] :
= 0
@[simp]
theorem Function.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)
Equations
• Pi.instAdd = { add := fun (f_1 g : (i : I) → f i) (i : I) => f_1 i + g i }
instance Pi.instMul {I : Type u} {f : IType v₁} [(i : I) → Mul (f i)] :
Mul ((i : I) → f i)
Equations
• Pi.instMul = { mul := fun (f_1 g : (i : I) → f i) (i : I) => f_1 i * g 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)] :
(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)] :
(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 : 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 : I) => x i * y i
@[simp]
theorem Function.const_add {α : Type u_1} {β : Type u_2} [Add β] (a : β) (b : β) :
+ = Function.const α (a + b)
@[simp]
theorem Function.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)
Equations
• Pi.instVAdd = { vadd := fun (s : α) (x : (i : I) → f i) (i : I) => s +ᵥ x i }
instance Pi.instSMul {I : Type u} {α : Type u_1} {f : IType v₁} [(i : I) → SMul α (f i)] :
SMul α ((i : I) → f i)
Equations
• Pi.instSMul = { smul := fun (s : α) (x : (i : I) → f i) (i : I) => s x i }
instance Pi.instPow {I : Type u} {β : Type u_2} {f : IType v₁} [(i : I) → Pow (f i) β] :
Pow ((i : I) → f i) β
Equations
• Pi.instPow = { pow := fun (x : (i : I) → f i) (b : β) (i : I) => x i ^ b }
@[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) :
(b +ᵥ x) i = b +ᵥ x 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) :
(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) :
(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 : 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 : 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 : I) => x i ^ b
@[simp]
theorem Function.vadd_const {I : Type u} {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) :
@[simp]
theorem Function.smul_const {I : Type u} {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) :
@[simp]
theorem Function.const_pow {I : Type u} {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) :
^ b = Function.const I (a ^ b)
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.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.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 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 x i = bit1 (x i)
instance Pi.instNeg {I : Type u} {f : IType v₁} [(i : I) → Neg (f i)] :
Neg ((i : I) → f i)
Equations
• Pi.instNeg = { neg := fun (f_1 : (i : I) → f i) (i : I) => -f_1 i }
instance Pi.instInv {I : Type u} {f : IType v₁} [(i : I) → Inv (f i)] :
Inv ((i : I) → f i)
Equations
• Pi.instInv = { inv := fun (f_1 : (i : I) → f i) (i : I) => (f_1 i)⁻¹ }
@[simp]
theorem Pi.neg_apply {I : Type u} {f : IType v₁} (x : (i : I) → f i) (i : I) [(i : I) → Neg (f i)] :
(-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)] :
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 : 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 : I) => (x i)⁻¹
theorem Function.const_neg {α : Type u_1} {β : Type u_2} [Neg β] (a : β) :
theorem Function.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)
Equations
• Pi.instSub = { sub := fun (f_1 g : (i : I) → f i) (i : I) => f_1 i - g i }
instance Pi.instDiv {I : Type u} {f : IType v₁} [(i : I) → Div (f i)] :
Div ((i : I) → f i)
Equations
• Pi.instDiv = { div := fun (f_1 g : (i : I) → f i) (i : I) => f_1 i / g 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)] :
(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)] :
(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 : 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 : 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 Function.const_sub {α : Type u_1} {β : Type u_2} [Sub β] (a : β) (b : β) :
- = Function.const α (a - b)
@[simp]
theorem Function.const_div {α : Type u_1} {β : Type u_2} [Div β] (a : β) (b : β) :
/ = Function.const α (a / b)
theorem Pi.addSemigroup.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → AddSemigroup (f i)] :
∀ (a b c : (i : I) → f i), a + b + c = a + (b + c)
instance Pi.addSemigroup {I : Type u} {f : IType v₁} [(i : I) → AddSemigroup (f i)] :
AddSemigroup ((i : I) → f i)
Equations
instance Pi.semigroup {I : Type u} {f : IType v₁} [(i : I) → Semigroup (f i)] :
Semigroup ((i : I) → f i)
Equations
• Pi.semigroup =
instance Pi.addCommSemigroup {I : Type u} {f : IType v₁} [(i : I) → AddCommSemigroup (f i)] :
AddCommSemigroup ((i : I) → f i)
Equations
theorem Pi.addCommSemigroup.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → AddCommSemigroup (f i)] :
∀ (a b : (i : I) → f i), a + b = b + a
instance Pi.commSemigroup {I : Type u} {f : IType v₁} [(i : I) → CommSemigroup (f i)] :
CommSemigroup ((i : I) → f i)
Equations
• Pi.commSemigroup =
instance Pi.addZeroClass {I : Type u} {f : IType v₁} [(i : I) → AddZeroClass (f i)] :
AddZeroClass ((i : I) → f i)
Equations
theorem Pi.addZeroClass.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → AddZeroClass (f i)] :
∀ (a : (i : I) → f i), 0 + a = a
theorem Pi.addZeroClass.proof_2 {I : Type u_1} {f : IType u_2} [(i : I) → AddZeroClass (f i)] :
∀ (a : (i : I) → f i), a + 0 = a
instance Pi.mulOneClass {I : Type u} {f : IType v₁} [(i : I) → MulOneClass (f i)] :
MulOneClass ((i : I) → f i)
Equations
• Pi.mulOneClass =
theorem Pi.negZeroClass.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → NegZeroClass (f i)] :
-0 = 0
instance Pi.negZeroClass {I : Type u} {f : IType v₁} [(i : I) → NegZeroClass (f i)] :
NegZeroClass ((i : I) → f i)
Equations
• Pi.negZeroClass =
instance Pi.invOneClass {I : Type u} {f : IType v₁} [(i : I) → InvOneClass (f i)] :
InvOneClass ((i : I) → f i)
Equations
• Pi.invOneClass =
theorem Pi.addMonoid.proof_4 {I : Type u_1} {f : IType u_2} [(i : I) → AddMonoid (f i)] :
∀ (n : ) (x : (i : I) → f i), (fun (n : ) (x : (i : I) → f i) (i : I) => n x i) (n + 1) x = (fun (n : ) (x : (i : I) → f i) (i : I) => n x i) n x + x
theorem Pi.addMonoid.proof_2 {I : Type u_1} {f : IType u_2} [(i : I) → AddMonoid (f i)] (a : (i : I) → f i) :
a + 0 = a
theorem Pi.addMonoid.proof_3 {I : Type u_1} {f : IType u_2} [(i : I) → AddMonoid (f i)] :
∀ (x : (i : I) → f i), (fun (n : ) (x : (i : I) → f i) (i : I) => n x i) 0 x = 0
theorem Pi.addMonoid.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → AddMonoid (f i)] (a : (i : I) → f i) :
0 + a = a
instance Pi.addMonoid {I : Type u} {f : IType v₁} [(i : I) → AddMonoid (f i)] :
AddMonoid ((i : I) → f i)
Equations
instance Pi.monoid {I : Type u} {f : IType v₁} [(i : I) → Monoid (f i)] :
Monoid ((i : I) → f i)
Equations
• Pi.monoid = let __spread.0 := Pi.semigroup; let __spread.1 := Pi.mulOneClass; Monoid.mk (fun (n : ) (x : (i : I) → f i) (i : I) => x i ^ n)
instance Pi.addCommMonoid {I : Type u} {f : IType v₁} [(i : I) → AddCommMonoid (f i)] :
AddCommMonoid ((i : I) → f i)
Equations
theorem Pi.addCommMonoid.proof_1 {I : Type u_2} {f : IType u_1} [(i : I) → AddCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) :
a + b = b + a
instance Pi.commMonoid {I : Type u} {f : IType v₁} [(i : I) → CommMonoid (f i)] :
CommMonoid ((i : I) → f i)
Equations
• Pi.commMonoid = let __src := Pi.monoid; let __src_1 := Pi.commSemigroup;
instance Pi.subNegMonoid {I : Type u} {f : IType v₁} [(i : I) → SubNegMonoid (f i)] :
SubNegMonoid ((i : I) → f i)
Equations
theorem Pi.subNegMonoid.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → SubNegMonoid (f i)] :
∀ (a b : (i : I) → f i), a - b = a + -b
theorem Pi.subNegMonoid.proof_2 {I : Type u_1} {f : IType u_2} [(i : I) → SubNegMonoid (f i)] :
∀ (a : (i : I) → f i), (fun (z : ) (x : (i : I) → f i) (i : I) => z x i) 0 a = 0
theorem Pi.subNegMonoid.proof_3 {I : Type u_1} {f : IType u_2} [(i : I) → SubNegMonoid (f i)] :
∀ (n : ) (a : (i : I) → f i), (fun (z : ) (x : (i : I) → f i) (i : I) => z x i) () a = (fun (z : ) (x : (i : I) → f i) (i : I) => z x i) () a + a
theorem Pi.subNegMonoid.proof_4 {I : Type u_1} {f : IType u_2} [(i : I) → SubNegMonoid (f i)] :
∀ (n : ) (a : (i : I) → f i), (fun (z : ) (x : (i : I) → f i) (i : I) => z x i) () a = -(fun (z : ) (x : (i : I) → f i) (i : I) => z x i) (()) a
instance Pi.divInvMonoid {I : Type u} {f : IType v₁} [(i : I) → DivInvMonoid (f i)] :
DivInvMonoid ((i : I) → f i)
Equations
• Pi.divInvMonoid = DivInvMonoid.mk (fun (z : ) (x : (i : I) → f i) (i : I) => x i ^ z)
theorem Pi.subNegZeroMonoid.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → SubNegZeroMonoid (f i)] :
-0 = 0
instance Pi.subNegZeroMonoid {I : Type u} {f : IType v₁} [(i : I) → SubNegZeroMonoid (f i)] :
SubNegZeroMonoid ((i : I) → f i)
Equations
• Pi.subNegZeroMonoid =
instance Pi.divInvOneMonoid {I : Type u} {f : IType v₁} [(i : I) → DivInvOneMonoid (f i)] :
DivInvOneMonoid ((i : I) → f i)
Equations
• Pi.divInvOneMonoid =
theorem Pi.involutiveNeg.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → InvolutiveNeg (f i)] :
∀ (x : (i : I) → f i), - -x = x
instance Pi.involutiveNeg {I : Type u} {f : IType v₁} [(i : I) → InvolutiveNeg (f i)] :
InvolutiveNeg ((i : I) → f i)
Equations
• Pi.involutiveNeg =
instance Pi.involutiveInv {I : Type u} {f : IType v₁} [(i : I) → InvolutiveInv (f i)] :
InvolutiveInv ((i : I) → f i)
Equations
• Pi.involutiveInv =
instance Pi.subtractionMonoid {I : Type u} {f : IType v₁} [(i : I) → SubtractionMonoid (f i)] :
SubtractionMonoid ((i : I) → f i)
Equations
theorem Pi.subtractionMonoid.proof_2 {I : Type u_1} {f : IType u_2} [(i : I) → SubtractionMonoid (f i)] :
∀ (a b : (i : I) → f i), -(a + b) = -b + -a
theorem Pi.subtractionMonoid.proof_1 {I : Type u_2} {f : IType u_1} [(i : I) → SubtractionMonoid (f i)] (x : (i : I) → f i) :
- -x = x
theorem Pi.subtractionMonoid.proof_3 {I : Type u_1} {f : IType u_2} [(i : I) → SubtractionMonoid (f i)] :
∀ (a b : (i : I) → f i), a + b = 0-a = b
instance Pi.divisionMonoid {I : Type u} {f : IType v₁} [(i : I) → DivisionMonoid (f i)] :
DivisionMonoid ((i : I) → f i)
Equations
theorem Pi.instSubtractionCommMonoid.proof_1 {I : Type u_2} {f : IType u_1} [(i : I) → ] (a : (i : I) → f i) (b : (i : I) → f i) :
a + b = b + a
instance Pi.instSubtractionCommMonoid {I : Type u} {f : IType v₁} [(i : I) → ] :
SubtractionCommMonoid ((i : I) → f i)
Equations
• Pi.instSubtractionCommMonoid = let __src := Pi.subtractionMonoid; let __src_1 := Pi.addCommSemigroup;
instance Pi.divisionCommMonoid {I : Type u} {f : IType v₁} [(i : I) → DivisionCommMonoid (f i)] :
DivisionCommMonoid ((i : I) → f i)
Equations
• Pi.divisionCommMonoid = let __src := Pi.divisionMonoid; let __src_1 := Pi.commSemigroup;
theorem Pi.addGroup.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → AddGroup (f i)] :
∀ (a : (i : I) → f i), -a + a = 0
instance Pi.addGroup {I : Type u} {f : IType v₁} [(i : I) → AddGroup (f i)] :
AddGroup ((i : I) → f i)
Equations
instance Pi.group {I : Type u} {f : IType v₁} [(i : I) → Group (f i)] :
Group ((i : I) → f i)
Equations
• Pi.group =
theorem Pi.addCommGroup.proof_1 {I : Type u_2} {f : IType u_1} [(i : I) → AddCommGroup (f i)] (a : (i : I) → f i) (b : (i : I) → f i) :
a + b = b + a
instance Pi.addCommGroup {I : Type u} {f : IType v₁} [(i : I) → AddCommGroup (f i)] :
AddCommGroup ((i : I) → f i)
Equations
instance Pi.commGroup {I : Type u} {f : IType v₁} [(i : I) → CommGroup (f i)] :
CommGroup ((i : I) → f i)
Equations
• Pi.commGroup = let __src := Pi.group; let __src_1 := Pi.commMonoid;
instance Pi.instIsAddLeftCancel {I : Type u} {f : IType v₁} [(i : I) → Add (f i)] [∀ (i : I), IsLeftCancelAdd (f i)] :
IsLeftCancelAdd ((i : I) → f i)
Equations
• =
instance Pi.instIsLeftCancelMul {I : Type u} {f : IType v₁} [(i : I) → Mul (f i)] [∀ (i : I), IsLeftCancelMul (f i)] :
IsLeftCancelMul ((i : I) → f i)
Equations
• =
instance Pi.instIsAddRightCancel {I : Type u} {f : IType v₁} [(i : I) → Add (f i)] [∀ (i : I), IsRightCancelAdd (f i)] :
IsRightCancelAdd ((i : I) → f i)
Equations
• =
instance Pi.instIsRightCancelMul {I : Type u} {f : IType v₁} [(i : I) → Mul (f i)] [∀ (i : I), IsRightCancelMul (f i)] :
IsRightCancelMul ((i : I) → f i)
Equations
• =
instance Pi.instIsAddCancel {I : Type u} {f : IType v₁} [(i : I) → Add (f i)] [∀ (i : I), IsCancelAdd (f i)] :
IsCancelAdd ((i : I) → f i)
Equations
• =
instance Pi.instIsCancelMul {I : Type u} {f : IType v₁} [(i : I) → Mul (f i)] [∀ (i : I), IsCancelMul (f i)] :
IsCancelMul ((i : I) → f i)
Equations
• =
theorem Pi.addLeftCancelSemigroup.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → ] :
∀ (x x_1 x_2 : (i : I) → f i), x + x_1 = x + x_2x_1 = x_2
instance Pi.addLeftCancelSemigroup {I : Type u} {f : IType v₁} [(i : I) → ] :
AddLeftCancelSemigroup ((i : I) → f i)
Equations
instance Pi.leftCancelSemigroup {I : Type u} {f : IType v₁} [(i : I) → LeftCancelSemigroup (f i)] :
LeftCancelSemigroup ((i : I) → f i)
Equations
• Pi.leftCancelSemigroup = let __src := Pi.semigroup;
instance Pi.addRightCancelSemigroup {I : Type u} {f : IType v₁} [(i : I) → ] :
AddRightCancelSemigroup ((i : I) → f i)
Equations
theorem Pi.addRightCancelSemigroup.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → ] :
∀ (x x_1 x_2 : (i : I) → f i), x + x_1 = x_2 + x_1x = x_2
instance Pi.rightCancelSemigroup {I : Type u} {f : IType v₁} [(i : I) → RightCancelSemigroup (f i)] :
RightCancelSemigroup ((i : I) → f i)
Equations
• Pi.rightCancelSemigroup = let __src := Pi.semigroup;
theorem Pi.addLeftCancelMonoid.proof_4 {I : Type u_1} {f : IType u_2} [(i : I) → AddLeftCancelMonoid (f i)] (n : ) (x : (i : I) → f i) :
AddMonoid.nsmul (n + 1) x = + x
theorem Pi.addLeftCancelMonoid.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → AddLeftCancelMonoid (f i)] (a : (i : I) → f i) :
0 + a = a
theorem Pi.addLeftCancelMonoid.proof_3 {I : Type u_1} {f : IType u_2} [(i : I) → AddLeftCancelMonoid (f i)] (x : (i : I) → f i) :
= 0
theorem Pi.addLeftCancelMonoid.proof_2 {I : Type u_1} {f : IType u_2} [(i : I) → AddLeftCancelMonoid (f i)] (a : (i : I) → f i) :
a + 0 = a
instance Pi.addLeftCancelMonoid {I : Type u} {f : IType v₁} [(i : I) → AddLeftCancelMonoid (f i)] :
AddLeftCancelMonoid ((i : I) → f i)
Equations
instance Pi.leftCancelMonoid {I : Type u} {f : IType v₁} [(i : I) → LeftCancelMonoid (f i)] :
LeftCancelMonoid ((i : I) → f i)
Equations
• Pi.leftCancelMonoid = let __src := Pi.leftCancelSemigroup; let __src_1 := Pi.monoid; LeftCancelMonoid.mk Monoid.npow
theorem Pi.addRightCancelMonoid.proof_4 {I : Type u_1} {f : IType u_2} [(i : I) → AddRightCancelMonoid (f i)] (n : ) (x : (i : I) → f i) :
AddMonoid.nsmul (n + 1) x = + x
instance Pi.addRightCancelMonoid {I : Type u} {f : IType v₁} [(i : I) → AddRightCancelMonoid (f i)] :
AddRightCancelMonoid ((i : I) → f i)
Equations
theorem Pi.addRightCancelMonoid.proof_3 {I : Type u_1} {f : IType u_2} [(i : I) → AddRightCancelMonoid (f i)] (x : (i : I) → f i) :
= 0
theorem Pi.addRightCancelMonoid.proof_2 {I : Type u_1} {f : IType u_2} [(i : I) → AddRightCancelMonoid (f i)] (a : (i : I) → f i) :
a + 0 = a
theorem Pi.addRightCancelMonoid.proof_1 {I : Type u_1} {f : IType u_2} [(i : I) → AddRightCancelMonoid (f i)] (a : (i : I) → f i) :
0 + a = a
instance Pi.rightCancelMonoid {I : Type u} {f : IType v₁} [(i : I) → RightCancelMonoid (f i)] :
RightCancelMonoid ((i : I) → f i)
Equations
• Pi.rightCancelMonoid = let __src := Pi.rightCancelSemigroup; let __src_1 := Pi.monoid; RightCancelMonoid.mk Monoid.npow
instance Pi.addCancelMonoid {I : Type u} {f : IType v₁} [(i : I) → AddCancelMonoid (f i)] :
AddCancelMonoid ((i : I) → f i)
Equations
theorem Pi.addCancelMonoid.proof_1 {I : Type u_2} {f : IType u_1} [(i : I) → AddCancelMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) (c : (i : I) → f i) :
a + b = c + ba = c
instance Pi.cancelMonoid {I : Type u} {f : IType v₁} [(i : I) → CancelMonoid (f i)] :
CancelMonoid ((i : I) → f i)
Equations
• Pi.cancelMonoid = let __src := Pi.leftCancelMonoid; let __src_1 := Pi.rightCancelMonoid;
instance Pi.addCancelCommMonoid {I : Type u} {f : IType v₁} [(i : I) → AddCancelCommMonoid (f i)] :
AddCancelCommMonoid ((i : I) → f i)
Equations
theorem Pi.addCancelCommMonoid.proof_1 {I : Type u_2} {f : IType u_1} [(i : I) → AddCancelCommMonoid (f i)] (a : (i : I) → f i) (b : (i : I) → f i) :
a + b = b + a
instance Pi.cancelCommMonoid {I : Type u} {f : IType v₁} [(i : I) → CancelCommMonoid (f i)] :
CancelCommMonoid ((i : I) → f i)
Equations
• Pi.cancelCommMonoid = let __src := Pi.leftCancelMonoid; let __src_1 := Pi.commMonoid;
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.

Equations
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.

Equations
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 : I) => 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 : I) => 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 : I) => 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 : I) => 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.

Equations
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 : I) → f i) (i : 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 : I) → f i) (i : 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 : I) → f i) (i : I) => F i (x i)
theorem Function.comp_eq_const_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} (b : β) (f : αβ) {g : βγ} (hg : ) :
g f = Function.const α (g b) f =
theorem Function.comp_eq_zero_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero β] [Zero γ] (f : αβ) {g : βγ} (hg : ) (hg0 : g 0 = 0) :
g f = 0 f = 0
theorem Function.comp_eq_one_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [One β] [One γ] (f : αβ) {g : βγ} (hg : ) (hg0 : g 1 = 1) :
g f = 1 f = 1
theorem Function.comp_ne_zero_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero β] [Zero γ] (f : αβ) {g : βγ} (hg : ) (hg0 : g 0 = 0) :
g f 0 f 0
theorem Function.comp_ne_one_iff {α : Type u_1} {β : Type u_2} {γ : Type u_3} [One β] [One γ] (f : αβ) {g : βγ} (hg : ) (hg0 : g 1 = 1) :
g f 1 f 1
def uniqueOfSurjectiveZero (α : Type u_4) {β : Type u_5} [Zero β] (h : ) :

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

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

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

Equations
Instances For
theorem Subsingleton.pi_single_eq {I : Type u} {α : Type u_4} [] [] [Zero α] (i : I) (x : α) :
= fun (x_1 : I) => x
theorem Subsingleton.pi_mulSingle_eq {I : Type u} {α : Type u_4} [] [] [One α] (i : I) (x : α) :
= fun (x_1 : I) => 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'