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.

@[deprecated Function.prod (since := "2026-04-21")]

def Pi.prod {ι : Sort u_3} {α : ι → Type u_1} {β : ι → Type u_2} (f : (i : ι) → α i) (g : (i : ι) → β i) (i : ι) : α i × β i

Alias of Function.prod.

@[deprecated Function.prod_fst_snd (since := "2026-04-21")]

theorem Pi.prod_fst_snd {α : Type u_1} {β : Type u_2} : Function.prod Prod.fst Prod.snd = id

Alias of Function.prod_fst_snd.

@[deprecated Function.prod_snd_fst (since := "2026-04-21")]

theorem Pi.prod_snd_fst {α : Type u_1} {β : Type u_2} : Function.prod Prod.snd Prod.fst = Prod.swap

Alias of Function.prod_snd_fst.

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

@[implicit_reducible]

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

@[implicit_reducible]

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

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

@[implicit_reducible]

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

@[implicit_reducible]

instance Pi.instAdd {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → Add (M i)] : Add ((i : ι) → M 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

@[implicit_reducible]

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

@[implicit_reducible]

instance Pi.instNeg {ι : Type u_1} {G : ι → Type u_4} [(i : ι) → Neg (G i)] : Neg ((i : ι) → G 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

@[implicit_reducible]

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

@[implicit_reducible]

instance Pi.instSub {ι : Type u_1} {G : ι → Type u_4} [(i : ι) → Sub (G i)] : Sub ((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)

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

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

@[implicit_reducible]

instance Pi.instVAdd {ι : Type u_1} {α : Type u_2} {M : ι → Type u_5} [(i : ι) → VAdd α (M i)] : VAdd α ((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.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

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

@[implicit_reducible]

instance Pi.instStarForall {ι : Type u_1} {R : ι → Type u_6} [(i : ι) → Star (R i)] : Star ((i : ι) → R 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)