Documentation

Mathlib.Algebra.Notation.Pi

Notation for algebraic operators on pi types #

This file provides only the notation for (pointwise) 0, 1, +, *, •, ^, ⁻¹ on pi types. See Mathlib.Algebra.Group.Pi.Basic for the Monoid and Group instances.

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

source
instance Pi.instOne {I : Type u} {f : I → Type v₁} [(i : I) → One (f i)] :
One ((i : I) → f i)
Equations
source
instance Pi.instZero {I : Type u} {f : I → Type v₁} [(i : I) → Zero (f i)] :
Zero ((i : I) → f i)
Equations
source
@[simp]
theorem Pi.one_apply {I : Type u} {f : I → Type v₁} (i : I) [(i : I) → One (f i)] :
1 i = 1
source
@[simp]
theorem Pi.zero_apply {I : Type u} {f : I → Type v₁} (i : I) [(i : I) → Zero (f i)] :
0 i = 0
source
theorem Pi.one_def {I : Type u} {f : I → Type v₁} [(i : I) → One (f i)] :
1 = fun (x : I) => 1
source
theorem Pi.zero_def {I : Type u} {f : I → Type v₁} [(i : I) → Zero (f i)] :
0 = fun (x : I) => 0
source
@[simp]
theorem Function.const_one {α : Type u_1} {β : Type u_2} [One β] :
const α 1 = 1
source
@[simp]
theorem Function.const_zero {α : Type u_1} {β : Type u_2} [Zero β] :
const α 0 = 0
source
@[simp]
theorem Pi.one_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [One γ] (x : α → β) :
1 ∘ x = 1
source
@[simp]
theorem Pi.zero_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero γ] (x : α → β) :
0 ∘ x = 0
source
@[simp]
theorem Pi.comp_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [One β] (x : β → γ) :
x ∘ 1 = Function.const α (x 1)
source
@[simp]
theorem Pi.comp_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero β] (x : β → γ) :
x ∘ 0 = Function.const α (x 0)
source
instance Pi.instMul {I : Type u} {f : I → Type 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 }
source
instance Pi.instAdd {I : Type u} {f : I → Type 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 }
source
@[simp]
theorem Pi.mul_apply {I : Type u} {f : I → Type v₁} (x y : (i : I) → f i) (i : I) [(i : I) → Mul (f i)] :
(x * y) i = x i * y i
source
@[simp]
theorem Pi.add_apply {I : Type u} {f : I → Type v₁} (x y : (i : I) → f i) (i : I) [(i : I) → Add (f i)] :
(x + y) i = x i + y i
source
theorem Pi.mul_def {I : Type u} {f : I → Type v₁} (x y : (i : I) → f i) [(i : I) → Mul (f i)] :
x * y = fun (i : I) => x i * y i
source
theorem Pi.add_def {I : Type u} {f : I → Type v₁} (x y : (i : I) → f i) [(i : I) → Add (f i)] :
x + y = fun (i : I) => x i + y i
source
@[simp]
theorem Function.const_mul {α : Type u_1} {β : Type u_2} [Mul β] (a b : β) :
const α a * const α b = const α (a * b)
source
@[simp]
theorem Function.const_add {α : Type u_1} {β : Type u_2} [Add β] (a b : β) :
const α a + const α b = const α (a + b)
source
theorem Pi.mul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Mul γ] (x y : β → γ) (z : α → β) :
(x * y) ∘ z = x ∘ z * y ∘ z
source
theorem Pi.add_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Add γ] (x y : β → γ) (z : α → β) :
(x + y) ∘ z = x ∘ z + y ∘ z
source
instance Pi.instSMul {I : Type u} {α : Type u_1} {f : I → Type 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 }
source
instance Pi.instVAdd {I : Type u} {α : Type u_1} {f : I → Type 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 }
source
instance Pi.instPow {I : Type u} {β : Type u_2} {f : I → Type 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 }
source
@[simp]
theorem Pi.pow_apply {I : Type u} {β : Type u_2} {f : I → Type v₁} [(i : I) → Pow (f i) β] (x : (i : I) → f i) (b : β) (i : I) :
(x ^ b) i = x i ^ b
source
@[simp]
theorem Pi.vadd_apply {I : Type u} {β : Type u_2} {f : I → Type v₁} [(i : I) → VAdd β (f i)] (b : β) (x : (i : I) → f i) (i : I) :
(b +ᵥ x) i = b +ᵥ x i
source
@[simp]
theorem Pi.smul_apply {I : Type u} {β : Type u_2} {f : I → Type v₁} [(i : I) → SMul β (f i)] (b : β) (x : (i : I) → f i) (i : I) :
(b • x) i = b • x i
source
theorem Pi.pow_def {I : Type u} {β : Type u_2} {f : I → Type v₁} [(i : I) → Pow (f i) β] (x : (i : I) → f i) (b : β) :
x ^ b = fun (i : I) => x i ^ b
source
theorem Pi.smul_def {I : Type u} {β : Type u_2} {f : I → Type v₁} [(i : I) → SMul β (f i)] (b : β) (x : (i : I) → f i) :
b • x = fun (i : I) => b • x i
source
theorem Pi.vadd_def {I : Type u} {β : Type u_2} {f : I → Type v₁} [(i : I) → VAdd β (f i)] (b : β) (x : (i : I) → f i) :
b +ᵥ x = fun (i : I) => b +ᵥ x i
source
@[simp]
theorem Function.const_pow {I : Type u} {α : Type u_1} {β : Type u_2} [Pow α β] (a : α) (b : β) :
const I a ^ b = const I (a ^ b)
source
@[simp]
theorem Function.smul_const {I : Type u} {β : Type u_2} {α : Type u_1} [SMul β α] (b : β) (a : α) :
b • const I a = const I (b • a)
source
@[simp]
theorem Function.vadd_const {I : Type u} {β : Type u_2} {α : Type u_1} [VAdd β α] (b : β) (a : α) :
b +ᵥ const I a = const I (b +ᵥ a)
source
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
source
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
source
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
source
instance Pi.instInv {I : Type u} {f : I → Type v₁} [(i : I) → Inv (f i)] :
Inv ((i : I) → f i)
Equations
source
instance Pi.instNeg {I : Type u} {f : I → Type 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 }
source
@[simp]
theorem Pi.inv_apply {I : Type u} {f : I → Type v₁} (x : (i : I) → f i) (i : I) [(i : I) → Inv (f i)] :
x⁻¹ i = (x i)⁻¹
source
@[simp]
theorem Pi.neg_apply {I : Type u} {f : I → Type v₁} (x : (i : I) → f i) (i : I) [(i : I) → Neg (f i)] :
(-x) i = -x i
source
theorem Pi.inv_def {I : Type u} {f : I → Type v₁} (x : (i : I) → f i) [(i : I) → Inv (f i)] :
x⁻¹ = fun (i : I) => (x i)⁻¹
source
theorem Pi.neg_def {I : Type u} {f : I → Type v₁} (x : (i : I) → f i) [(i : I) → Neg (f i)] :
-x = fun (i : I) => -x i
source
theorem Function.const_inv {α : Type u_1} {β : Type u_2} [Inv β] (a : β) :
(const α a)⁻¹ = const α a⁻¹
source
theorem Function.const_neg {α : Type u_1} {β : Type u_2} [Neg β] (a : β) :
-const α a = const α (-a)
source
theorem Pi.inv_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Inv γ] (x : β → γ) (y : α → β) :
x⁻¹ ∘ y = (x ∘ y)⁻¹
source
theorem Pi.neg_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Neg γ] (x : β → γ) (y : α → β) :
(-x) ∘ y = -x ∘ y
source
instance Pi.instDiv {I : Type u} {f : I → Type 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 }
source
instance Pi.instSub {I : Type u} {f : I → Type 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 }
source
@[simp]
theorem Pi.div_apply {I : Type u} {f : I → Type v₁} (x y : (i : I) → f i) (i : I) [(i : I) → Div (f i)] :
(x / y) i = x i / y i
source
@[simp]
theorem Pi.sub_apply {I : Type u} {f : I → Type v₁} (x y : (i : I) → f i) (i : I) [(i : I) → Sub (f i)] :
(x - y) i = x i - y i
source
theorem Pi.div_def {I : Type u} {f : I → Type v₁} (x y : (i : I) → f i) [(i : I) → Div (f i)] :
x / y = fun (i : I) => x i / y i
source
theorem Pi.sub_def {I : Type u} {f : I → Type v₁} (x y : (i : I) → f i) [(i : I) → Sub (f i)] :
x - y = fun (i : I) => x i - y i
source
theorem Pi.div_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Div γ] (x y : β → γ) (z : α → β) :
(x / y) ∘ z = x ∘ z / y ∘ z
source
theorem Pi.sub_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Sub γ] (x y : β → γ) (z : α → β) :
(x - y) ∘ z = x ∘ z - y ∘ z
source
@[simp]
theorem Function.const_div {α : Type u_1} {β : Type u_2} [Div β] (a b : β) :
const α a / const α b = const α (a / b)
source
@[simp]
theorem Function.const_sub {α : Type u_1} {β : Type u_2} [Sub β] (a b : β) :
const α a - const α b = const α (a - b)