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.

instance Pi.instOne {I : Type u} {f : I → Type v₁} [(i : I) → One (f i)] : One ((i : I) → f i)

Equations

• Pi.instOne = { one := fun (x : I) => 1 }

instance Pi.instZero {I : Type u} {f : I → Type v₁} [(i : I) → Zero (f i)] : Zero ((i : I) → f i)

Equations

• Pi.instZero = { zero := fun (x : I) => 0 }

@[simp]

theorem Pi.one_apply {I : Type u} {f : I → Type v₁} (i : I) [(i : I) → One (f i)] : 1 i = 1

@[simp]

theorem Pi.zero_apply {I : Type u} {f : I → Type v₁} (i : I) [(i : I) → Zero (f i)] : 0 i = 0

theorem Pi.one_def {I : Type u} {f : I → Type v₁} [(i : I) → One (f i)] : 1 = fun (x : I) => 1

theorem Pi.zero_def {I : Type u} {f : I → Type v₁} [(i : I) → Zero (f i)] : 0 = fun (x : I) => 0

@[simp]

theorem Function.const_one {α : Type u_1} {β : Type u_2} [One β] : const α 1 = 1

@[simp]

theorem Function.const_zero {α : Type u_1} {β : Type u_2} [Zero β] : const α 0 = 0

@[simp]

theorem Pi.one_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [One γ] (x : α → β) : 1 ∘ x = 1

@[simp]

theorem Pi.zero_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero γ] (x : α → β) : 0 ∘ x = 0

@[simp]

theorem Pi.comp_one {α : Type u_1} {β : Type u_2} {γ : Type u_3} [One β] (x : β → γ) : x ∘ 1 = Function.const α (x 1)

@[simp]

theorem Pi.comp_zero {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Zero β] (x : β → γ) : x ∘ 0 = Function.const α (x 0)

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 }

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 }

@[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

@[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

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

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

@[simp]

theorem Function.const_mul {α : Type u_1} {β : Type u_2} [Mul β] (a b : β) : const α a * const α b = const α (a * b)

@[simp]

theorem Function.const_add {α : Type u_1} {β : Type u_2} [Add β] (a b : β) : const α a + const α b = const α (a + b)

theorem Pi.mul_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Mul γ] (x y : β → γ) (z : α → β) : (x * y) ∘ z = x ∘ z * y ∘ z

theorem Pi.add_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Add γ] (x y : β → γ) (z : α → β) : (x + y) ∘ z = x ∘ z + y ∘ z

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 }

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 }

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 }

@[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

@[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

@[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

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

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

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

@[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)

@[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)

@[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)

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

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

instance Pi.instInv {I : Type u} {f : I → Type 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)⁻¹ }

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 }

@[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)⁻¹

@[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

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)⁻¹

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

theorem Function.const_inv {α : Type u_1} {β : Type u_2} [Inv β] (a : β) : (const α a)⁻¹ = const α a⁻¹

theorem Function.const_neg {α : Type u_1} {β : Type u_2} [Neg β] (a : β) : -const α a = const α (-a)

theorem Pi.inv_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Inv γ] (x : β → γ) (y : α → β) : x⁻¹ ∘ y = (x ∘ y)⁻¹

theorem Pi.neg_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Neg γ] (x : β → γ) (y : α → β) : (-x) ∘ y = -x ∘ y

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 }

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 }

@[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

@[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

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

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

theorem Pi.div_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Div γ] (x y : β → γ) (z : α → β) : (x / y) ∘ z = x ∘ z / y ∘ z

theorem Pi.sub_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Sub γ] (x y : β → γ) (z : α → β) : (x - y) ∘ z = x ∘ z - y ∘ z

@[simp]

theorem Function.const_div {α : Type u_1} {β : Type u_2} [Div β] (a b : β) : const α a / const α b = const α (a / b)

@[simp]

theorem Function.const_sub {α : Type u_1} {β : Type u_2} [Sub β] (a b : β) : const α a - const α b = const α (a - b)