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.lean for the Monoid and Group instances.

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

instance Pi.instOne {ι : Type u_1} {M : ιType u_5} [(i : ι) → One (M i)] :
One ((i : ι) → M i)
Equations
instance Pi.instZero {ι : Type u_1} {M : ιType u_5} [(i : ι) → Zero (M i)] :
Zero ((i : ι) → M i)
Equations
@[simp]
theorem Pi.one_apply {ι : Type u_1} {M : ιType u_5} [(i : ι) → One (M i)] (i : ι) :
1 i = 1
@[simp]
theorem Pi.zero_apply {ι : Type u_1} {M : ιType u_5} [(i : ι) → Zero (M i)] (i : ι) :
0 i = 0
theorem Pi.one_def {ι : Type u_1} {M : ιType u_5} [(i : ι) → One (M i)] :
1 = fun (x : ι) => 1
theorem Pi.zero_def {ι : Type u_1} {M : ιType u_5} [(i : ι) → Zero (M i)] :
0 = fun (x : ι) => 0
@[simp]
theorem Function.const_one {α : Type u_2} {M : Type u_6} [One M] :
const α 1 = 1
@[simp]
theorem Function.const_zero {α : Type u_2} {M : Type u_6} [Zero M] :
const α 0 = 0
@[simp]
theorem Pi.one_comp {α : Type u_2} {β : Type u_3} {M : Type u_6} [One M] (f : αβ) :
1 f = 1
@[simp]
theorem Pi.zero_comp {α : Type u_2} {β : Type u_3} {M : Type u_6} [Zero M] (f : αβ) :
0 f = 0
@[simp]
theorem Pi.comp_one {α : Type u_2} {β : Type u_3} {M : Type u_6} [One M] (f : Mβ) :
f 1 = Function.const α (f 1)
@[simp]
theorem Pi.comp_zero {α : Type u_2} {β : Type u_3} {M : Type u_6} [Zero M] (f : Mβ) :
f 0 = Function.const α (f 0)
instance Pi.instMul {ι : Type u_1} {M : ιType u_5} [(i : ι) → Mul (M i)] :
Mul ((i : ι) → M i)
Equations
  • Pi.instMul = { mul := fun (f g : (i : ι) → M i) (i : ι) => f i * g i }
instance Pi.instAdd {ι : Type u_1} {M : ιType u_5} [(i : ι) → Add (M i)] :
Add ((i : ι) → M i)
Equations
  • Pi.instAdd = { add := fun (f g : (i : ι) → M i) (i : ι) => f i + g i }
@[simp]
theorem Pi.mul_apply {ι : Type u_1} {M : ιType u_5} [(i : ι) → Mul (M i)] (f g : (i : ι) → M i) (i : ι) :
(f * g) i = f i * g i
@[simp]
theorem Pi.add_apply {ι : Type u_1} {M : ιType u_5} [(i : ι) → Add (M i)] (f g : (i : ι) → M i) (i : ι) :
(f + g) i = f i + g i
theorem Pi.mul_def {ι : Type u_1} {M : ιType u_5} [(i : ι) → Mul (M i)] (f g : (i : ι) → M i) :
f * g = fun (i : ι) => f i * g i
theorem Pi.add_def {ι : Type u_1} {M : ιType u_5} [(i : ι) → Add (M i)] (f g : (i : ι) → M i) :
f + g = fun (i : ι) => f i + g i
@[simp]
theorem Function.const_mul {ι : Type u_1} {M : Type u_6} [Mul M] (a b : M) :
const ι a * const ι b = const ι (a * b)
@[simp]
theorem Function.const_add {ι : Type u_1} {M : Type u_6} [Add M] (a b : M) :
const ι a + const ι b = const ι (a + b)
theorem Pi.mul_comp {α : Type u_2} {β : Type u_3} {M : Type u_6} [Mul M] (f g : βM) (z : αβ) :
(f * g) z = f z * g z
theorem Pi.add_comp {α : Type u_2} {β : Type u_3} {M : Type u_6} [Add M] (f g : βM) (z : αβ) :
(f + g) z = f z + g z
instance Pi.instInv {ι : Type u_1} {G : ιType u_4} [(i : ι) → Inv (G i)] :
Inv ((i : ι) → G i)
Equations
instance Pi.instNeg {ι : Type u_1} {G : ιType u_4} [(i : ι) → Neg (G i)] :
Neg ((i : ι) → G i)
Equations
@[simp]
theorem Pi.inv_apply {ι : Type u_1} {G : ιType u_4} [(i : ι) → Inv (G i)] (f : (i : ι) → G i) (i : ι) :
f⁻¹ i = (f i)⁻¹
@[simp]
theorem Pi.neg_apply {ι : Type u_1} {G : ιType u_4} [(i : ι) → Neg (G i)] (f : (i : ι) → G i) (i : ι) :
(-f) i = -f i
theorem Pi.inv_def {ι : Type u_1} {G : ιType u_4} [(i : ι) → Inv (G i)] (f : (i : ι) → G i) :
f⁻¹ = fun (i : ι) => (f i)⁻¹
theorem Pi.neg_def {ι : Type u_1} {G : ιType u_4} [(i : ι) → Neg (G i)] (f : (i : ι) → G i) :
-f = fun (i : ι) => -f i
theorem Function.const_inv {ι : Type u_1} {G : Type u_6} [Inv G] (a : G) :
(const ι a)⁻¹ = const ι a⁻¹
theorem Function.const_neg {ι : Type u_1} {G : Type u_6} [Neg G] (a : G) :
-const ι a = const ι (-a)
theorem Pi.inv_comp {α : Type u_2} {β : Type u_3} {G : Type u_6} [Inv G] (f : βG) (g : αβ) :
f⁻¹ g = (f g)⁻¹
theorem Pi.neg_comp {α : Type u_2} {β : Type u_3} {G : Type u_6} [Neg G] (f : βG) (g : αβ) :
(-f) g = -f g
instance Pi.instDiv {ι : Type u_1} {G : ιType u_4} [(i : ι) → Div (G i)] :
Div ((i : ι) → G i)
Equations
  • Pi.instDiv = { div := fun (f g : (i : ι) → G i) (i : ι) => f i / g i }
instance Pi.instSub {ι : Type u_1} {G : ιType u_4} [(i : ι) → Sub (G i)] :
Sub ((i : ι) → G i)
Equations
  • Pi.instSub = { sub := fun (f g : (i : ι) → G i) (i : ι) => f i - g i }
@[simp]
theorem Pi.div_apply {ι : Type u_1} {G : ιType u_4} [(i : ι) → Div (G i)] (f g : (i : ι) → G i) (i : ι) :
(f / g) i = f i / g i
@[simp]
theorem Pi.sub_apply {ι : Type u_1} {G : ιType u_4} [(i : ι) → Sub (G i)] (f g : (i : ι) → G i) (i : ι) :
(f - g) i = f i - g i
theorem Pi.div_def {ι : Type u_1} {G : ιType u_4} [(i : ι) → Div (G i)] (f g : (i : ι) → G i) :
f / g = fun (i : ι) => f i / g i
theorem Pi.sub_def {ι : Type u_1} {G : ιType u_4} [(i : ι) → Sub (G i)] (f g : (i : ι) → G i) :
f - g = fun (i : ι) => f i - g i
theorem Pi.div_comp {α : Type u_2} {β : Type u_3} {G : Type u_6} [Div G] (f g : βG) (z : αβ) :
(f / g) z = f z / g z
theorem Pi.sub_comp {α : Type u_2} {β : Type u_3} {G : Type u_6} [Sub G] (f g : βG) (z : αβ) :
(f - g) z = f z - g z
@[simp]
theorem Function.const_div {ι : Type u_1} {G : Type u_6} [Div G] (a b : G) :
const ι a / const ι b = const ι (a / b)
@[simp]
theorem Function.const_sub {ι : Type u_1} {G : Type u_6} [Sub G] (a b : G) :
const ι a - const ι b = const ι (a - b)
instance Pi.instSMul {ι : Type u_1} {α : Type u_2} {M : ιType u_5} [(i : ι) → SMul α (M i)] :
SMul α ((i : ι) → M i)
Equations
instance Pi.instVAdd {ι : Type u_1} {α : Type u_2} {M : ιType u_5} [(i : ι) → VAdd α (M i)] :
VAdd α ((i : ι) → M i)
Equations
instance Pi.instPow {ι : Type u_1} {α : Type u_2} {M : ιType u_5} [(i : ι) → Pow (M i) α] :
Pow ((i : ι) → M i) α
Equations
  • Pi.instPow = { pow := fun (f : (i : ι) → M i) (a : α) (i : ι) => f i ^ a }
@[simp]
theorem Pi.pow_apply {ι : Type u_1} {α : Type u_2} {M : ιType u_5} [(i : ι) → Pow (M i) α] (f : (i : ι) → M i) (a : α) (i : ι) :
(f ^ a) i = f i ^ a
@[simp]
theorem Pi.vadd_apply {ι : Type u_1} {α : Type u_2} {M : ιType u_5} [(i : ι) → VAdd α (M i)] (a : α) (f : (i : ι) → M i) (i : ι) :
(a +ᵥ f) i = a +ᵥ f i
@[simp]
theorem Pi.smul_apply {ι : Type u_1} {α : Type u_2} {M : ιType u_5} [(i : ι) → SMul α (M i)] (a : α) (f : (i : ι) → M i) (i : ι) :
(a f) i = a f i
theorem Pi.pow_def {ι : Type u_1} {α : Type u_2} {M : ιType u_5} [(i : ι) → Pow (M i) α] (f : (i : ι) → M i) (a : α) :
f ^ a = fun (i : ι) => f i ^ a
theorem Pi.vadd_def {ι : Type u_1} {α : Type u_2} {M : ιType u_5} [(i : ι) → VAdd α (M i)] (a : α) (f : (i : ι) → M i) :
a +ᵥ f = fun (i : ι) => a +ᵥ f i
theorem Pi.smul_def {ι : Type u_1} {α : Type u_2} {M : ιType u_5} [(i : ι) → SMul α (M i)] (a : α) (f : (i : ι) → M i) :
a f = fun (i : ι) => a f i
@[simp]
theorem Function.const_pow {ι : Type u_1} {α : Type u_2} {M : Type u_6} [Pow M α] (a : M) (b : α) :
const ι a ^ b = const ι (a ^ b)
@[simp]
theorem Function.smul_const {ι : Type u_1} {M : Type u_6} {α : Type u_2} [SMul α M] (b : α) (a : M) :
b const ι a = const ι (b a)
@[simp]
theorem Function.vadd_const {ι : Type u_1} {M : Type u_6} {α : Type u_2} [VAdd α M] (b : α) (a : M) :
b +ᵥ const ι a = const ι (b +ᵥ a)
theorem Pi.pow_comp {ι : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_6} [Pow M α] (f : βM) (a : α) (g : ιβ) :
(f ^ a) g = f g ^ a
theorem Pi.smul_comp {ι : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_6} [SMul α M] (a : α) (f : βM) (g : ιβ) :
(a f) g = a f g
theorem Pi.vadd_comp {ι : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_6} [VAdd α M] (a : α) (f : βM) (g : ιβ) :
(a +ᵥ f) g = a +ᵥ f g