Documentation

Mathlib.Algebra.Notation.Pi.Defs

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.

def Pi.prod {ι : Type u_1} {α : ι → Type u_7} {β : ι → Type u_8} (f : (i : ι) → α i) (g : (i : ι) → β i) (i : ι) :

α i × β i

The mapping into a product type built from maps into each component.

Equations

Pi.prod f g i = (f i, g i)

Instances For

theorem Pi.prod_fst_snd {α : Type u_2} {β : Type u_3} :

Pi.prod Prod.fst Prod.snd = id

theorem Pi.prod_snd_fst {α : Type u_2} {β : Type u_3} :

Pi.prod Prod.snd Prod.fst = Prod.swap

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

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

instance Pi.instZero {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → Zero (M i)] :

Zero ((i : ι) → M i)

Equations

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

@[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_7} [One M] :

const α 1 = 1

@[simp]

theorem Function.const_zero {α : Type u_2} {M : Type u_7} [Zero M] :

const α 0 = 0

@[simp]

theorem Pi.one_comp {α : Type u_2} {β : Type u_3} {M : Type u_7} [One M] (f : α → β) :

1 ∘ f = 1

@[simp]

theorem Pi.zero_comp {α : Type u_2} {β : Type u_3} {M : Type u_7} [Zero M] (f : α → β) :

0 ∘ f = 0

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

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_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

instance Pi.instInv {ι : Type u_1} {G : ι → Type u_4} [(i : ι) → Inv (G i)] :

Inv ((i : ι) → G i)

Equations

Pi.instInv = { inv := fun (f : (i : ι) → G i) (i : ι) => (f i)⁻¹ }

instance Pi.instNeg {ι : Type u_1} {G : ι → Type u_4} [(i : ι) → Neg (G i)] :

Neg ((i : ι) → G i)

Equations

Pi.instNeg = { neg := fun (f : (i : ι) → G i) (i : ι) => -f i }

@[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_7} [Inv G] (a : G) :

(const ι a)⁻¹ = const ι a⁻¹

theorem Function.const_neg {ι : Type u_1} {G : Type u_7} [Neg G] (a : G) :

-const ι a = const ι (-a)

theorem Pi.inv_comp {α : Type u_2} {β : Type u_3} {G : Type u_7} [Inv G] (f : β → G) (g : α → β) :

f⁻¹ ∘ g = (f ∘ g)⁻¹

theorem Pi.neg_comp {α : Type u_2} {β : Type u_3} {G : Type u_7} [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_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)

instance Pi.instSMul {ι : Type u_1} {α : Type u_2} {M : ι → Type u_5} [(i : ι) → SMul α (M i)] :

SMul α ((i : ι) → M i)

Equations

Pi.instSMul = { smul := fun (a : α) (f : (i : ι) → M i) (i : ι) => a • f i }

instance Pi.instVAdd {ι : Type u_1} {α : Type u_2} {M : ι → Type u_5} [(i : ι) → VAdd α (M i)] :

VAdd α ((i : ι) → M i)

Equations

Pi.instVAdd = { vadd := fun (a : α) (f : (i : ι) → M i) (i : ι) => a +ᵥ f i }

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

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

@[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.vadd_const {ι : Type u_1} {M : Type u_7} {α : Type u_2} [VAdd α M] (b : α) (a : M) :

b +ᵥ const ι a = const ι (b +ᵥ a)

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

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

theorem Pi.vadd_comp {ι : Type u_1} {α : Type u_2} {β : Type u_3} {M : Type u_7} [VAdd α M] (a : α) (f : β → M) (g : ι → β) :

(a +ᵥ f) ∘ g = a +ᵥ f ∘ g

instance Pi.instStarForall {ι : Type u_1} {R : ι → Type u_6} [(i : ι) → Star (R i)] :

Star ((i : ι) → R i)

Equations

Pi.instStarForall = { star := fun (x : (i : ι) → R i) (i : ι) => star (x i) }

@[simp]

theorem Pi.star_apply {ι : Type u_1} {R : ι → Type u_6} [(i : ι) → Star (R i)] (x : (i : ι) → R i) (i : ι) :

star x i = star (x i)

theorem Pi.star_def {ι : Type u_1} {R : ι → Type u_6} [(i : ι) → Star (R i)] (x : (i : ι) → R i) :

star x = fun (i : ι) => star (x i)