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. There is also
an instance of the Star notation typeclass, but no default notation is included.
1, 0, +, *, +ᵥ, •, ^, -, ⁻¹, and / are defined pointwise.
@[implicit_reducible]
@[implicit_reducible]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp]
theorem
Pi.comp_one
{α : Type u_2}
{β : Type u_3}
{M : Type u_7}
[One M]
(f : M → β)
:
f ∘ 1 = Function.const α (f 1)
@[simp]
theorem
Pi.comp_zero
{α : Type u_2}
{β : Type u_3}
{M : Type u_7}
[Zero M]
(f : M → β)
:
f ∘ 0 = Function.const α (f 0)
@[implicit_reducible]
@[implicit_reducible]
@[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_7}
[Mul M]
(a b : M)
:
const ι a * const ι b = const ι (a * b)
@[simp]
theorem
Function.const_add
{ι : Type u_1}
{M : Type u_7}
[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_7}
[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_7}
[Add M]
(f g : β → M)
(z : α → β)
:
(f + g) ∘ z = f ∘ z + g ∘ z
@[implicit_reducible]
@[implicit_reducible]
@[simp]
theorem
Pi.inv_apply
{ι : Type u_1}
{G : ι → Type u_4}
[(i : ι) → Inv (G i)]
(f : (i : ι) → G i)
(i : ι)
:
@[simp]
theorem
Pi.neg_apply
{ι : Type u_1}
{G : ι → Type u_4}
[(i : ι) → Neg (G i)]
(f : (i : ι) → G i)
(i : ι)
:
@[implicit_reducible]
@[implicit_reducible]
@[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_7}
[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_7}
[Sub G]
(f g : β → G)
(z : α → β)
:
(f - g) ∘ z = f ∘ z - g ∘ z
@[simp]
theorem
Function.const_div
{ι : Type u_1}
{G : Type u_7}
[Div G]
(a b : G)
:
const ι a / const ι b = const ι (a / b)
@[simp]
theorem
Function.const_sub
{ι : Type u_1}
{G : Type u_7}
[Sub G]
(a b : G)
:
const ι a - const ι b = const ι (a - b)
@[implicit_reducible]
instance
Pi.instPow
{ι : Type u_1}
{α : Type u_2}
{M : ι → Type u_5}
[(i : ι) → Pow (M i) α]
:
Pow ((i : ι) → M i) α
@[implicit_reducible]
@[implicit_reducible]
instance
Pi.instSMul
{ι : Type u_1}
{α : Type u_2}
{M : ι → Type u_5}
[(i : ι) → SMul α (M i)]
:
SMul α ((i : ι) → M i)
@[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.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
@[simp]
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.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_7}
[Pow M α]
(a : M)
(b : α)
:
const ι a ^ b = const ι (a ^ b)
@[simp]
theorem
Function.smul_const
{ι : Type u_1}
{M : Type u_7}
{α : Type u_2}
[SMul α M]
(b : α)
(a : M)
:
b • const ι a = const ι (b • a)
@[simp]
theorem
Pi.pow_comp
{ι : Type u_1}
{α : Type u_2}
{β : Type u_3}
{M : Type u_7}
[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_7}
[SMul α M]
(a : α)
(f : β → M)
(g : ι → β)
:
(a • f) ∘ g = a • f ∘ g
@[implicit_reducible]
instance
Pi.instStarForall
{ι : Type u_1}
{R : ι → Type u_6}
[(i : ι) → Star (R i)]
:
Star ((i : ι) → R i)
@[simp]