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.

source
instance Pi.instOne {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → One (M i)] :
One ((i : ι) → M i)
Equations
    source
    instance Pi.instZero {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → Zero (M i)] :
    Zero ((i : ι) → M i)
    Equations
      source
      @[simp]
      theorem Pi.one_apply {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → One (M i)] (i : ι) :
      1 i = 1
      source
      @[simp]
      theorem Pi.zero_apply {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → Zero (M i)] (i : ι) :
      0 i = 0
      source
      theorem Pi.one_def {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → One (M i)] :
      1 = fun (x : ι) => 1
      source
      theorem Pi.zero_def {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → Zero (M i)] :
      0 = fun (x : ι) => 0
      source
      @[simp]
      theorem Function.const_one {α : Type u_2} {M : Type u_6} [One M] :
      const α 1 = 1
      source
      @[simp]
      theorem Function.const_zero {α : Type u_2} {M : Type u_6} [Zero M] :
      const α 0 = 0
      source
      @[simp]
      theorem Pi.one_comp {α : Type u_2} {β : Type u_3} {M : Type u_6} [One M] (f : α → β) :
      1 ∘ f = 1
      source
      @[simp]
      theorem Pi.zero_comp {α : Type u_2} {β : Type u_3} {M : Type u_6} [Zero M] (f : α → β) :
      0 ∘ f = 0
      source
      @[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)
      source
      @[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)
      source
      instance Pi.instMul {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → Mul (M i)] :
      Mul ((i : ι) → M i)
      Equations
        source
        instance Pi.instAdd {ι : Type u_1} {M : ι → Type u_5} [(i : ι) → Add (M i)] :
        Add ((i : ι) → M i)
        Equations
          source
          @[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
          source
          @[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
          source
          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
          source
          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
          source
          @[simp]
          theorem Function.const_mul {ι : Type u_1} {M : Type u_6} [Mul M] (a b : M) :
          const ι a * const ι b = const ι (a * b)
          source
          @[simp]
          theorem Function.const_add {ι : Type u_1} {M : Type u_6} [Add M] (a b : M) :
          const ι a + const ι b = const ι (a + b)
          source
          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
          source
          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
          source
          instance Pi.instInv {ι : Type u_1} {G : ι → Type u_4} [(i : ι) → Inv (G i)] :
          Inv ((i : ι) → G i)
          Equations
            source
            instance Pi.instNeg {ι : Type u_1} {G : ι → Type u_4} [(i : ι) → Neg (G i)] :
            Neg ((i : ι) → G i)
            Equations
              source
              @[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)⁻¹
              source
              @[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
              source
              theorem Pi.inv_def {ι : Type u_1} {G : ι → Type u_4} [(i : ι) → Inv (G i)] (f : (i : ι) → G i) :
              f⁻¹ = fun (i : ι) => (f i)⁻¹
              source
              theorem Pi.neg_def {ι : Type u_1} {G : ι → Type u_4} [(i : ι) → Neg (G i)] (f : (i : ι) → G i) :
              -f = fun (i : ι) => -f i
              source
              theorem Function.const_inv {ι : Type u_1} {G : Type u_6} [Inv G] (a : G) :
              (const ι a)⁻¹ = const ι a⁻¹
              source
              theorem Function.const_neg {ι : Type u_1} {G : Type u_6} [Neg G] (a : G) :
              -const ι a = const ι (-a)
              source
              theorem Pi.inv_comp {α : Type u_2} {β : Type u_3} {G : Type u_6} [Inv G] (f : β → G) (g : α → β) :
              f⁻¹ ∘ g = (f ∘ g)⁻¹
              source
              theorem Pi.neg_comp {α : Type u_2} {β : Type u_3} {G : Type u_6} [Neg G] (f : β → G) (g : α → β) :
              (-f) ∘ g = -f ∘ g
              source
              instance Pi.instDiv {ι : Type u_1} {G : ι → Type u_4} [(i : ι) → Div (G i)] :
              Div ((i : ι) → G i)
              Equations
                source
                instance Pi.instSub {ι : Type u_1} {G : ι → Type u_4} [(i : ι) → Sub (G i)] :
                Sub ((i : ι) → G i)
                Equations
                  source
                  @[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
                  source
                  @[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
                  source
                  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
                  source
                  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
                  source
                  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
                  source
                  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
                  source
                  @[simp]
                  theorem Function.const_div {ι : Type u_1} {G : Type u_6} [Div G] (a b : G) :
                  const ι a / const ι b = const ι (a / b)
                  source
                  @[simp]
                  theorem Function.const_sub {ι : Type u_1} {G : Type u_6} [Sub G] (a b : G) :
                  const ι a - const ι b = const ι (a - b)
                  source
                  instance Pi.instSMul {ι : Type u_1} {α : Type u_2} {M : ι → Type u_5} [(i : ι) → SMul α (M i)] :
                  SMul α ((i : ι) → M i)
                  Equations
                    source
                    instance Pi.instVAdd {ι : Type u_1} {α : Type u_2} {M : ι → Type u_5} [(i : ι) → VAdd α (M i)] :
                    VAdd α ((i : ι) → M i)
                    Equations
                      source
                      instance Pi.instPow {ι : Type u_1} {α : Type u_2} {M : ι → Type u_5} [(i : ι) → Pow (M i) α] :
                      Pow ((i : ι) → M i) α
                      Equations
                        source
                        @[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
                        source
                        @[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
                        source
                        @[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
                        source
                        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
                        source
                        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
                        source
                        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
                        source
                        @[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)
                        source
                        @[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)
                        source
                        @[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)
                        source
                        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
                        source
                        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
                        source
                        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