Documentation

Mathlib.Algebra.Group.Pi.Lemmas

Extra lemmas about products of monoids and groups #

This file proves lemmas about the instances defined in Algebra.Group.Pi.Basic that require more imports.

@[simp]
theorem Set.range_zero {α : Type u_3} {β : Type u_4} [Zero β] [Nonempty α] :
Set.range 0 = {0}
@[simp]
theorem Set.range_one {α : Type u_3} {β : Type u_4} [One β] [Nonempty α] :
Set.range 1 = {1}
theorem Set.preimage_zero {α : Type u_3} {β : Type u_4} [Zero β] (s : Set β) [Decidable (0 s)] :
0 ⁻¹' s = if 0 s then Set.univ else
theorem Set.preimage_one {α : Type u_3} {β : Type u_4} [One β] (s : Set β) [Decidable (1 s)] :
1 ⁻¹' s = if 1 s then Set.univ else
theorem Pi.zero_mono {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] [Zero β] :
theorem Pi.one_mono {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] [One β] :
theorem Pi.zero_anti {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] [Zero β] :
theorem Pi.one_anti {α : Type u_3} {β : Type u_4} [Preorder α] [Preorder β] [One β] :
theorem AddHom.coe_add {M : Type u_3} {N : Type u_4} :
∀ {x : Add M} {x_1 : AddCommSemigroup N} (f g : AddHom M N), f + g = fun (x_2 : M) => f x_2 + g x_2
theorem MulHom.coe_mul {M : Type u_3} {N : Type u_4} :
∀ {x : Mul M} {x_1 : CommSemigroup N} (f g : M →ₙ* N), f * g = fun (x_2 : M) => f x_2 * g x_2
theorem Pi.addHom.proof_1 {I : Type u_1} {f : IType u_2} {γ : Type u_3} [(i : I) → Add (f i)] [Add γ] (g : (i : I) → AddHom γ (f i)) (x : γ) (y : γ) :
(fun (x : γ) (i : I) => (g i) x) (x + y) = (fun (x : γ) (i : I) => (g i) x) x + (fun (x : γ) (i : I) => (g i) x) y
def Pi.addHom {I : Type u} {f : IType v} {γ : Type w} [(i : I) → Add (f i)] [Add γ] (g : (i : I) → AddHom γ (f i)) :
AddHom γ ((i : I) → f i)

A family of AddHom's f a : γ → β a defines an AddHom Pi.addHom f : γ → Π a, β a given by Pi.addHom f x b = f b x.

Equations
  • Pi.addHom g = { toFun := fun (x : γ) (i : I) => (g i) x, map_add' := }
Instances For
    @[simp]
    theorem Pi.mulHom_apply {I : Type u} {f : IType v} {γ : Type w} [(i : I) → Mul (f i)] [Mul γ] (g : (i : I) → γ →ₙ* f i) (x : γ) (i : I) :
    (Pi.mulHom g) x i = (g i) x
    @[simp]
    theorem Pi.addHom_apply {I : Type u} {f : IType v} {γ : Type w} [(i : I) → Add (f i)] [Add γ] (g : (i : I) → AddHom γ (f i)) (x : γ) (i : I) :
    (Pi.addHom g) x i = (g i) x
    def Pi.mulHom {I : Type u} {f : IType v} {γ : Type w} [(i : I) → Mul (f i)] [Mul γ] (g : (i : I) → γ →ₙ* f i) :
    γ →ₙ* (i : I) → f i

    A family of MulHom's f a : γ →ₙ* β a defines a MulHom Pi.mulHom f : γ →ₙ* Π a, β a given by Pi.mulHom f x b = f b x.

    Equations
    • Pi.mulHom g = { toFun := fun (x : γ) (i : I) => (g i) x, map_mul' := }
    Instances For
      theorem Pi.addHom_injective {I : Type u} {f : IType v} {γ : Type w} [Nonempty I] [(i : I) → Add (f i)] [Add γ] (g : (i : I) → AddHom γ (f i)) (hg : ∀ (i : I), Function.Injective (g i)) :
      theorem Pi.mulHom_injective {I : Type u} {f : IType v} {γ : Type w} [Nonempty I] [(i : I) → Mul (f i)] [Mul γ] (g : (i : I) → γ →ₙ* f i) (hg : ∀ (i : I), Function.Injective (g i)) :
      def Pi.addMonoidHom {I : Type u} {f : IType v} {γ : Type w} [(i : I) → AddZeroClass (f i)] [AddZeroClass γ] (g : (i : I) → γ →+ f i) :
      γ →+ (i : I) → f i

      A family of additive monoid homomorphisms f a : γ →+ β a defines a monoid homomorphism Pi.addMonoidHom f : γ →+ Π a, β a given by Pi.addMonoidHom f x b = f b x.

      Equations
      • Pi.addMonoidHom g = { toFun := fun (x : γ) (i : I) => (g i) x, map_zero' := , map_add' := }
      Instances For
        theorem Pi.addMonoidHom.proof_2 {I : Type u_1} {f : IType u_2} {γ : Type u_3} [(i : I) → AddZeroClass (f i)] [AddZeroClass γ] (g : (i : I) → γ →+ f i) (x : γ) (y : γ) :
        (Pi.addHom fun (i : I) => (g i)).toFun (x + y) = (Pi.addHom fun (i : I) => (g i)).toFun x + (Pi.addHom fun (i : I) => (g i)).toFun y
        theorem Pi.addMonoidHom.proof_1 {I : Type u_1} {f : IType u_2} {γ : Type u_3} [(i : I) → AddZeroClass (f i)] [AddZeroClass γ] (g : (i : I) → γ →+ f i) :
        (fun (x : γ) (i : I) => (g i) x) 0 = 0
        @[simp]
        theorem Pi.monoidHom_apply {I : Type u} {f : IType v} {γ : Type w} [(i : I) → MulOneClass (f i)] [MulOneClass γ] (g : (i : I) → γ →* f i) (x : γ) (i : I) :
        (Pi.monoidHom g) x i = (g i) x
        @[simp]
        theorem Pi.addMonoidHom_apply {I : Type u} {f : IType v} {γ : Type w} [(i : I) → AddZeroClass (f i)] [AddZeroClass γ] (g : (i : I) → γ →+ f i) (x : γ) (i : I) :
        (Pi.addMonoidHom g) x i = (g i) x
        def Pi.monoidHom {I : Type u} {f : IType v} {γ : Type w} [(i : I) → MulOneClass (f i)] [MulOneClass γ] (g : (i : I) → γ →* f i) :
        γ →* (i : I) → f i

        A family of monoid homomorphisms f a : γ →* β a defines a monoid homomorphism Pi.monoidHom f : γ →* Π a, β a given by Pi.monoidHom f x b = f b x.

        Equations
        • Pi.monoidHom g = { toFun := fun (x : γ) (i : I) => (g i) x, map_one' := , map_mul' := }
        Instances For
          theorem Pi.addMonoidHom_injective {I : Type u} {f : IType v} {γ : Type w} [Nonempty I] [(i : I) → AddZeroClass (f i)] [AddZeroClass γ] (g : (i : I) → γ →+ f i) (hg : ∀ (i : I), Function.Injective (g i)) :
          theorem Pi.monoidHom_injective {I : Type u} {f : IType v} {γ : Type w} [Nonempty I] [(i : I) → MulOneClass (f i)] [MulOneClass γ] (g : (i : I) → γ →* f i) (hg : ∀ (i : I), Function.Injective (g i)) :
          def Pi.evalAddHom {I : Type u} (f : IType v) [(i : I) → Add (f i)] (i : I) :
          AddHom ((i : I) → f i) (f i)

          Evaluation of functions into an indexed collection of additive semigroups at a point is an additive semigroup homomorphism. This is Function.eval i as an AddHom.

          Equations
          • Pi.evalAddHom f i = { toFun := fun (g : (i : I) → f i) => g i, map_add' := }
          Instances For
            @[simp]
            theorem Pi.evalAddHom_apply {I : Type u} (f : IType v) [(i : I) → Add (f i)] (i : I) (g : (i : I) → f i) :
            (Pi.evalAddHom f i) g = g i
            @[simp]
            theorem Pi.evalMulHom_apply {I : Type u} (f : IType v) [(i : I) → Mul (f i)] (i : I) (g : (i : I) → f i) :
            (Pi.evalMulHom f i) g = g i
            def Pi.evalMulHom {I : Type u} (f : IType v) [(i : I) → Mul (f i)] (i : I) :
            ((i : I) → f i) →ₙ* f i

            Evaluation of functions into an indexed collection of semigroups at a point is a semigroup homomorphism. This is Function.eval i as a MulHom.

            Equations
            • Pi.evalMulHom f i = { toFun := fun (g : (i : I) → f i) => g i, map_mul' := }
            Instances For
              theorem Pi.constAddHom.proof_1 (α : Type u_1) (β : Type u_2) [Add β] :
              ∀ (x x_1 : β), Function.const α (x + x_1) = Function.const α (x + x_1)
              def Pi.constAddHom (α : Type u_3) (β : Type u_4) [Add β] :
              AddHom β (αβ)

              Function.const as an AddHom.

              Equations
              Instances For
                @[simp]
                theorem Pi.constAddHom_apply (α : Type u_3) (β : Type u_4) [Add β] (a : β) :
                ∀ (a_1 : α), (Pi.constAddHom α β) a a_1 = Function.const α a a_1
                @[simp]
                theorem Pi.constMulHom_apply (α : Type u_3) (β : Type u_4) [Mul β] (a : β) :
                ∀ (a_1 : α), (Pi.constMulHom α β) a a_1 = Function.const α a a_1
                def Pi.constMulHom (α : Type u_3) (β : Type u_4) [Mul β] :
                β →ₙ* αβ

                Function.const as a MulHom.

                Equations
                Instances For
                  def AddHom.coeFn (α : Type u_3) (β : Type u_4) [Add α] [AddCommSemigroup β] :
                  AddHom (AddHom α β) (αβ)

                  Coercion of an AddHom into a function is itself an AddHom.

                  See also AddHom.eval.

                  Equations
                  Instances For
                    theorem AddHom.coeFn.proof_1 (α : Type u_1) (β : Type u_2) [Add α] [AddCommSemigroup β] :
                    ∀ (x x_1 : AddHom α β), (fun (g : AddHom α β) => g) (x + x_1) = (fun (g : AddHom α β) => g) (x + x_1)
                    @[simp]
                    theorem MulHom.coeFn_apply (α : Type u_3) (β : Type u_4) [Mul α] [CommSemigroup β] (g : α →ₙ* β) (a : α) :
                    (MulHom.coeFn α β) g a = g a
                    @[simp]
                    theorem AddHom.coeFn_apply (α : Type u_3) (β : Type u_4) [Add α] [AddCommSemigroup β] (g : AddHom α β) (a : α) :
                    (AddHom.coeFn α β) g a = g a
                    def MulHom.coeFn (α : Type u_3) (β : Type u_4) [Mul α] [CommSemigroup β] :
                    (α →ₙ* β) →ₙ* αβ

                    Coercion of a MulHom into a function is itself a MulHom.

                    See also MulHom.eval.

                    Equations
                    Instances For
                      def AddHom.compLeft {α : Type u_3} {β : Type u_4} [Add α] [Add β] (f : AddHom α β) (I : Type u_5) :
                      AddHom (Iα) (Iβ)

                      Additive semigroup homomorphism between the function spaces I → α and I → β, induced by an additive semigroup homomorphism f between α and β

                      Equations
                      • f.compLeft I = { toFun := fun (h : Iα) => f h, map_add' := }
                      Instances For
                        theorem AddHom.compLeft.proof_1 {α : Type u_3} {β : Type u_2} [Add α] [Add β] (f : AddHom α β) (I : Type u_1) :
                        ∀ (x x_1 : Iα), (fun (h : Iα) => f h) (x + x_1) = (fun (h : Iα) => f h) x + (fun (h : Iα) => f h) x_1
                        @[simp]
                        theorem MulHom.compLeft_apply {α : Type u_3} {β : Type u_4} [Mul α] [Mul β] (f : α →ₙ* β) (I : Type u_5) (h : Iα) :
                        ∀ (a : I), (f.compLeft I) h a = (f h) a
                        @[simp]
                        theorem AddHom.compLeft_apply {α : Type u_3} {β : Type u_4} [Add α] [Add β] (f : AddHom α β) (I : Type u_5) (h : Iα) :
                        ∀ (a : I), (f.compLeft I) h a = (f h) a
                        def MulHom.compLeft {α : Type u_3} {β : Type u_4} [Mul α] [Mul β] (f : α →ₙ* β) (I : Type u_5) :
                        (Iα) →ₙ* Iβ

                        Semigroup homomorphism between the function spaces I → α and I → β, induced by a semigroup homomorphism f between α and β.

                        Equations
                        • f.compLeft I = { toFun := fun (h : Iα) => f h, map_mul' := }
                        Instances For
                          theorem Pi.evalAddMonoidHom.proof_2 {I : Type u_2} (f : IType u_1) [(i : I) → AddZeroClass (f i)] (i : I) :
                          ∀ (x x_1 : (i : I) → f i), (x + x_1) i = x i + x_1 i
                          def Pi.evalAddMonoidHom {I : Type u} (f : IType v) [(i : I) → AddZeroClass (f i)] (i : I) :
                          ((i : I) → f i) →+ f i

                          Evaluation of functions into an indexed collection of additive monoids at a point is an additive monoid homomorphism. This is Function.eval i as an AddMonoidHom.

                          Equations
                          • Pi.evalAddMonoidHom f i = { toFun := fun (g : (i : I) → f i) => g i, map_zero' := , map_add' := }
                          Instances For
                            theorem Pi.evalAddMonoidHom.proof_1 {I : Type u_2} (f : IType u_1) [(i : I) → AddZeroClass (f i)] (i : I) :
                            0 i = 0
                            @[simp]
                            theorem Pi.evalAddMonoidHom_apply {I : Type u} (f : IType v) [(i : I) → AddZeroClass (f i)] (i : I) (g : (i : I) → f i) :
                            @[simp]
                            theorem Pi.evalMonoidHom_apply {I : Type u} (f : IType v) [(i : I) → MulOneClass (f i)] (i : I) (g : (i : I) → f i) :
                            (Pi.evalMonoidHom f i) g = g i
                            def Pi.evalMonoidHom {I : Type u} (f : IType v) [(i : I) → MulOneClass (f i)] (i : I) :
                            ((i : I) → f i) →* f i

                            Evaluation of functions into an indexed collection of monoids at a point is a monoid homomorphism. This is Function.eval i as a MonoidHom.

                            Equations
                            • Pi.evalMonoidHom f i = { toFun := fun (g : (i : I) → f i) => g i, map_one' := , map_mul' := }
                            Instances For
                              def Pi.constAddMonoidHom (α : Type u_3) (β : Type u_4) [AddZeroClass β] :
                              β →+ αβ

                              Function.const as an AddMonoidHom.

                              Equations
                              Instances For
                                theorem Pi.constAddMonoidHom.proof_2 (α : Type u_1) (β : Type u_2) [AddZeroClass β] :
                                ∀ (x x_1 : β), { toFun := Function.const α, map_zero' := }.toFun (x + x_1) = { toFun := Function.const α, map_zero' := }.toFun (x + x_1)
                                @[simp]
                                theorem Pi.constMonoidHom_apply (α : Type u_3) (β : Type u_4) [MulOneClass β] (a : β) :
                                ∀ (a_1 : α), (Pi.constMonoidHom α β) a a_1 = Function.const α a a_1
                                @[simp]
                                theorem Pi.constAddMonoidHom_apply (α : Type u_3) (β : Type u_4) [AddZeroClass β] (a : β) :
                                ∀ (a_1 : α), (Pi.constAddMonoidHom α β) a a_1 = Function.const α a a_1
                                def Pi.constMonoidHom (α : Type u_3) (β : Type u_4) [MulOneClass β] :
                                β →* αβ

                                Function.const as a MonoidHom.

                                Equations
                                Instances For
                                  theorem AddMonoidHom.coeFn.proof_2 (α : Type u_1) (β : Type u_2) [AddZeroClass α] [AddCommMonoid β] :
                                  ∀ (x x_1 : α →+ β), { toFun := fun (g : α →+ β) => g, map_zero' := }.toFun (x + x_1) = { toFun := fun (g : α →+ β) => g, map_zero' := }.toFun (x + x_1)
                                  theorem AddMonoidHom.coeFn.proof_1 (α : Type u_1) (β : Type u_2) [AddZeroClass α] [AddCommMonoid β] :
                                  (fun (g : α →+ β) => g) 0 = (fun (g : α →+ β) => g) 0
                                  def AddMonoidHom.coeFn (α : Type u_3) (β : Type u_4) [AddZeroClass α] [AddCommMonoid β] :
                                  (α →+ β) →+ αβ

                                  Coercion of an AddMonoidHom into a function is itself an AddMonoidHom.

                                  See also AddMonoidHom.eval.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem MonoidHom.coeFn_apply (α : Type u_3) (β : Type u_4) [MulOneClass α] [CommMonoid β] (g : α →* β) (a : α) :
                                    (MonoidHom.coeFn α β) g a = g a
                                    @[simp]
                                    theorem AddMonoidHom.coeFn_apply (α : Type u_3) (β : Type u_4) [AddZeroClass α] [AddCommMonoid β] (g : α →+ β) (a : α) :
                                    (AddMonoidHom.coeFn α β) g a = g a
                                    def MonoidHom.coeFn (α : Type u_3) (β : Type u_4) [MulOneClass α] [CommMonoid β] :
                                    (α →* β) →* αβ

                                    Coercion of a MonoidHom into a function is itself a MonoidHom.

                                    See also MonoidHom.eval.

                                    Equations
                                    Instances For
                                      theorem AddMonoidHom.compLeft.proof_1 {α : Type u_3} {β : Type u_2} [AddZeroClass α] [AddZeroClass β] (f : α →+ β) (I : Type u_1) :
                                      (fun (h : Iα) => f h) 0 = 0
                                      theorem AddMonoidHom.compLeft.proof_2 {α : Type u_3} {β : Type u_2} [AddZeroClass α] [AddZeroClass β] (f : α →+ β) (I : Type u_1) :
                                      ∀ (x x_1 : Iα), { toFun := fun (h : Iα) => f h, map_zero' := }.toFun (x + x_1) = { toFun := fun (h : Iα) => f h, map_zero' := }.toFun x + { toFun := fun (h : Iα) => f h, map_zero' := }.toFun x_1
                                      def AddMonoidHom.compLeft {α : Type u_3} {β : Type u_4} [AddZeroClass α] [AddZeroClass β] (f : α →+ β) (I : Type u_5) :
                                      (Iα) →+ Iβ

                                      Additive monoid homomorphism between the function spaces I → α and I → β, induced by an additive monoid homomorphism f between α and β

                                      Equations
                                      • f.compLeft I = { toFun := fun (h : Iα) => f h, map_zero' := , map_add' := }
                                      Instances For
                                        @[simp]
                                        theorem MonoidHom.compLeft_apply {α : Type u_3} {β : Type u_4} [MulOneClass α] [MulOneClass β] (f : α →* β) (I : Type u_5) (h : Iα) :
                                        ∀ (a : I), (f.compLeft I) h a = (f h) a
                                        @[simp]
                                        theorem AddMonoidHom.compLeft_apply {α : Type u_3} {β : Type u_4} [AddZeroClass α] [AddZeroClass β] (f : α →+ β) (I : Type u_5) (h : Iα) :
                                        ∀ (a : I), (f.compLeft I) h a = (f h) a
                                        def MonoidHom.compLeft {α : Type u_3} {β : Type u_4} [MulOneClass α] [MulOneClass β] (f : α →* β) (I : Type u_5) :
                                        (Iα) →* Iβ

                                        Monoid homomorphism between the function spaces I → α and I → β, induced by a monoid homomorphism f between α and β.

                                        Equations
                                        • f.compLeft I = { toFun := fun (h : Iα) => f h, map_one' := , map_mul' := }
                                        Instances For
                                          def ZeroHom.single {I : Type u} (f : IType v) [DecidableEq I] [(i : I) → Zero (f i)] (i : I) :
                                          ZeroHom (f i) ((i : I) → f i)

                                          The zero-preserving homomorphism including a single value into a dependent family of values, as functions supported at a point.

                                          This is the ZeroHom version of Pi.single.

                                          Equations
                                          Instances For
                                            def OneHom.mulSingle {I : Type u} (f : IType v) [DecidableEq I] [(i : I) → One (f i)] (i : I) :
                                            OneHom (f i) ((i : I) → f i)

                                            The one-preserving homomorphism including a single value into a dependent family of values, as functions supported at a point.

                                            This is the OneHom version of Pi.mulSingle.

                                            Equations
                                            Instances For
                                              @[simp]
                                              theorem ZeroHom.single_apply {I : Type u} (f : IType v) [DecidableEq I] [(i : I) → Zero (f i)] (i : I) (x : f i) :
                                              @[simp]
                                              theorem OneHom.mulSingle_apply {I : Type u} (f : IType v) [DecidableEq I] [(i : I) → One (f i)] (i : I) (x : f i) :
                                              def AddMonoidHom.single {I : Type u} (f : IType v) [DecidableEq I] [(i : I) → AddZeroClass (f i)] (i : I) :
                                              f i →+ (i : I) → f i

                                              The additive monoid homomorphism including a single additive monoid into a dependent family of additive monoids, as functions supported at a point.

                                              This is the AddMonoidHom version of Pi.single.

                                              Equations
                                              Instances For
                                                theorem AddMonoidHom.single.proof_1 {I : Type u_1} (f : IType u_2) [DecidableEq I] [(i : I) → AddZeroClass (f i)] (i : I) (x₁ : f i) (x₂ : f i) :
                                                Pi.single i (x₁ + x₂) = fun (j : I) => Pi.single i x₁ j + Pi.single i x₂ j
                                                def MonoidHom.mulSingle {I : Type u} (f : IType v) [DecidableEq I] [(i : I) → MulOneClass (f i)] (i : I) :
                                                f i →* (i : I) → f i

                                                The monoid homomorphism including a single monoid into a dependent family of additive monoids, as functions supported at a point.

                                                This is the MonoidHom version of Pi.mulSingle.

                                                Equations
                                                Instances For
                                                  @[simp]
                                                  theorem AddMonoidHom.single_apply {I : Type u} (f : IType v) [DecidableEq I] [(i : I) → AddZeroClass (f i)] (i : I) (x : f i) :
                                                  @[simp]
                                                  theorem MonoidHom.mulSingle_apply {I : Type u} (f : IType v) [DecidableEq I] [(i : I) → MulOneClass (f i)] (i : I) (x : f i) :
                                                  theorem Pi.single_sup {I : Type u} {f : IType v} [DecidableEq I] [(i : I) → SemilatticeSup (f i)] [(i : I) → Zero (f i)] (i : I) (x : f i) (y : f i) :
                                                  theorem Pi.mulSingle_sup {I : Type u} {f : IType v} [DecidableEq I] [(i : I) → SemilatticeSup (f i)] [(i : I) → One (f i)] (i : I) (x : f i) (y : f i) :
                                                  theorem Pi.single_inf {I : Type u} {f : IType v} [DecidableEq I] [(i : I) → SemilatticeInf (f i)] [(i : I) → Zero (f i)] (i : I) (x : f i) (y : f i) :
                                                  theorem Pi.mulSingle_inf {I : Type u} {f : IType v} [DecidableEq I] [(i : I) → SemilatticeInf (f i)] [(i : I) → One (f i)] (i : I) (x : f i) (y : f i) :
                                                  theorem Pi.single_add {I : Type u} {f : IType v} [DecidableEq I] [(i : I) → AddZeroClass (f i)] (i : I) (x : f i) (y : f i) :
                                                  Pi.single i (x + y) = Pi.single i x + Pi.single i y
                                                  theorem Pi.mulSingle_mul {I : Type u} {f : IType v} [DecidableEq I] [(i : I) → MulOneClass (f i)] (i : I) (x : f i) (y : f i) :
                                                  theorem Pi.single_neg {I : Type u} {f : IType v} [DecidableEq I] [(i : I) → AddGroup (f i)] (i : I) (x : f i) :
                                                  theorem Pi.mulSingle_inv {I : Type u} {f : IType v} [DecidableEq I] [(i : I) → Group (f i)] (i : I) (x : f i) :
                                                  theorem Pi.single_sub {I : Type u} {f : IType v} [DecidableEq I] [(i : I) → AddGroup (f i)] (i : I) (x : f i) (y : f i) :
                                                  Pi.single i (x - y) = Pi.single i x - Pi.single i y
                                                  theorem Pi.mulSingle_div {I : Type u} {f : IType v} [DecidableEq I] [(i : I) → Group (f i)] (i : I) (x : f i) (y : f i) :
                                                  theorem Pi.single_nsmul {I : Type u} {f : IType v} [DecidableEq I] [(i : I) → AddMonoid (f i)] (i : I) (x : f i) (n : ) :
                                                  Pi.single i (n x) = n Pi.single i x
                                                  theorem Pi.mulSingle_pow {I : Type u} {f : IType v} [DecidableEq I] [(i : I) → Monoid (f i)] (i : I) (x : f i) (n : ) :
                                                  Pi.mulSingle i (x ^ n) = Pi.mulSingle i x ^ n
                                                  theorem Pi.single_zsmul {I : Type u} {f : IType v} [DecidableEq I] [(i : I) → AddGroup (f i)] (i : I) (x : f i) (n : ) :
                                                  Pi.single i (n x) = n Pi.single i x
                                                  theorem Pi.mulSingle_zpow {I : Type u} {f : IType v} [DecidableEq I] [(i : I) → Group (f i)] (i : I) (x : f i) (n : ) :
                                                  Pi.mulSingle i (x ^ n) = Pi.mulSingle i x ^ n
                                                  theorem Pi.single_addCommute {I : Type u} {f : IType v} [DecidableEq I] [(i : I) → AddZeroClass (f i)] :
                                                  Pairwise fun (i j : I) => ∀ (x : f i) (y : f j), AddCommute (Pi.single i x) (Pi.single j y)

                                                  The injection into an additive pi group at different indices commutes.

                                                  For injections of commuting elements at the same index, see AddCommute.map

                                                  theorem Pi.mulSingle_commute {I : Type u} {f : IType v} [DecidableEq I] [(i : I) → MulOneClass (f i)] :
                                                  Pairwise fun (i j : I) => ∀ (x : f i) (y : f j), Commute (Pi.mulSingle i x) (Pi.mulSingle j y)

                                                  The injection into a pi group at different indices commutes.

                                                  For injections of commuting elements at the same index, see Commute.map

                                                  theorem Pi.single_apply_addCommute {I : Type u} {f : IType v} [DecidableEq I] [(i : I) → AddZeroClass (f i)] (x : (i : I) → f i) (i : I) (j : I) :
                                                  AddCommute (Pi.single i (x i)) (Pi.single j (x j))

                                                  The injection into an additive pi group with the same values commutes.

                                                  theorem Pi.mulSingle_apply_commute {I : Type u} {f : IType v} [DecidableEq I] [(i : I) → MulOneClass (f i)] (x : (i : I) → f i) (i : I) (j : I) :
                                                  Commute (Pi.mulSingle i (x i)) (Pi.mulSingle j (x j))

                                                  The injection into a pi group with the same values commutes.

                                                  theorem Pi.update_eq_sub_add_single {I : Type u} {f : IType v} (i : I) [DecidableEq I] [(i : I) → AddGroup (f i)] (g : (i : I) → f i) (x : f i) :
                                                  Function.update g i x = g - Pi.single i (g i) + Pi.single i x
                                                  theorem Pi.update_eq_div_mul_mulSingle {I : Type u} {f : IType v} (i : I) [DecidableEq I] [(i : I) → Group (f i)] (g : (i : I) → f i) (x : f i) :
                                                  theorem Pi.single_add_single_eq_single_add_single {I : Type u} [DecidableEq I] {M : Type u_3} [AddCommMonoid M] {k : I} {l : I} {m : I} {n : I} {u : M} {v : M} (hu : u 0) (hv : v 0) :
                                                  Pi.single k u + Pi.single l v = Pi.single m u + Pi.single n v k = m l = n u = v k = n l = m u + v = 0 k = l m = n
                                                  theorem Pi.mulSingle_mul_mulSingle_eq_mulSingle_mul_mulSingle {I : Type u} [DecidableEq I] {M : Type u_3} [CommMonoid M] {k : I} {l : I} {m : I} {n : I} {u : M} {v : M} (hu : u 1) (hv : v 1) :
                                                  Pi.mulSingle k u * Pi.mulSingle l v = Pi.mulSingle m u * Pi.mulSingle n v k = m l = n u = v k = n l = m u * v = 1 k = l m = n
                                                  theorem AddSemiconjBy.pi {I : Type u} {f : IType v} [(i : I) → Add (f i)] {x : (i : I) → f i} {y : (i : I) → f i} {z : (i : I) → f i} (h : ∀ (i : I), AddSemiconjBy (x i) (y i) (z i)) :
                                                  theorem SemiconjBy.pi {I : Type u} {f : IType v} [(i : I) → Mul (f i)] {x : (i : I) → f i} {y : (i : I) → f i} {z : (i : I) → f i} (h : ∀ (i : I), SemiconjBy (x i) (y i) (z i)) :
                                                  theorem Pi.addSemiconjBy_iff {I : Type u} {f : IType v} [(i : I) → Add (f i)] {x : (i : I) → f i} {y : (i : I) → f i} {z : (i : I) → f i} :
                                                  AddSemiconjBy x y z ∀ (i : I), AddSemiconjBy (x i) (y i) (z i)
                                                  theorem Pi.semiconjBy_iff {I : Type u} {f : IType v} [(i : I) → Mul (f i)] {x : (i : I) → f i} {y : (i : I) → f i} {z : (i : I) → f i} :
                                                  SemiconjBy x y z ∀ (i : I), SemiconjBy (x i) (y i) (z i)
                                                  theorem AddCommute.pi {I : Type u} {f : IType v} [(i : I) → Add (f i)] {x : (i : I) → f i} {y : (i : I) → f i} (h : ∀ (i : I), AddCommute (x i) (y i)) :
                                                  theorem Commute.pi {I : Type u} {f : IType v} [(i : I) → Mul (f i)] {x : (i : I) → f i} {y : (i : I) → f i} (h : ∀ (i : I), Commute (x i) (y i)) :
                                                  theorem Pi.addCommute_iff {I : Type u} {f : IType v} [(i : I) → Add (f i)] {x : (i : I) → f i} {y : (i : I) → f i} :
                                                  AddCommute x y ∀ (i : I), AddCommute (x i) (y i)
                                                  theorem Pi.commute_iff {I : Type u} {f : IType v} [(i : I) → Mul (f i)] {x : (i : I) → f i} {y : (i : I) → f i} :
                                                  Commute x y ∀ (i : I), Commute (x i) (y i)
                                                  @[simp]
                                                  theorem Function.update_zero {I : Type u} {f : IType v} [(i : I) → Zero (f i)] [DecidableEq I] (i : I) :
                                                  @[simp]
                                                  theorem Function.update_one {I : Type u} {f : IType v} [(i : I) → One (f i)] [DecidableEq I] (i : I) :
                                                  theorem Function.update_add {I : Type u} {f : IType v} [(i : I) → Add (f i)] [DecidableEq I] (f₁ : (i : I) → f i) (f₂ : (i : I) → f i) (i : I) (x₁ : f i) (x₂ : f i) :
                                                  Function.update (f₁ + f₂) i (x₁ + x₂) = Function.update f₁ i x₁ + Function.update f₂ i x₂
                                                  theorem Function.update_mul {I : Type u} {f : IType v} [(i : I) → Mul (f i)] [DecidableEq I] (f₁ : (i : I) → f i) (f₂ : (i : I) → f i) (i : I) (x₁ : f i) (x₂ : f i) :
                                                  Function.update (f₁ * f₂) i (x₁ * x₂) = Function.update f₁ i x₁ * Function.update f₂ i x₂
                                                  theorem Function.update_neg {I : Type u} {f : IType v} [(i : I) → Neg (f i)] [DecidableEq I] (f₁ : (i : I) → f i) (i : I) (x₁ : f i) :
                                                  Function.update (-f₁) i (-x₁) = -Function.update f₁ i x₁
                                                  theorem Function.update_inv {I : Type u} {f : IType v} [(i : I) → Inv (f i)] [DecidableEq I] (f₁ : (i : I) → f i) (i : I) (x₁ : f i) :
                                                  theorem Function.update_sub {I : Type u} {f : IType v} [(i : I) → Sub (f i)] [DecidableEq I] (f₁ : (i : I) → f i) (f₂ : (i : I) → f i) (i : I) (x₁ : f i) (x₂ : f i) :
                                                  Function.update (f₁ - f₂) i (x₁ - x₂) = Function.update f₁ i x₁ - Function.update f₂ i x₂
                                                  theorem Function.update_div {I : Type u} {f : IType v} [(i : I) → Div (f i)] [DecidableEq I] (f₁ : (i : I) → f i) (f₂ : (i : I) → f i) (i : I) (x₁ : f i) (x₂ : f i) :
                                                  Function.update (f₁ / f₂) i (x₁ / x₂) = Function.update f₁ i x₁ / Function.update f₂ i x₂
                                                  @[simp]
                                                  theorem Function.const_eq_zero {ι : Type u_1} {α : Type u_2} [Zero α] [Nonempty ι] {a : α} :
                                                  Function.const ι a = 0 a = 0
                                                  @[simp]
                                                  theorem Function.const_eq_one {ι : Type u_1} {α : Type u_2} [One α] [Nonempty ι] {a : α} :
                                                  Function.const ι a = 1 a = 1
                                                  theorem Function.const_ne_zero {ι : Type u_1} {α : Type u_2} [Zero α] [Nonempty ι] {a : α} :
                                                  theorem Function.const_ne_one {ι : Type u_1} {α : Type u_2} [One α] [Nonempty ι] {a : α} :
                                                  theorem Set.piecewise_add {I : Type u} {f : IType v} [(i : I) → Add (f i)] (s : Set I) [(i : I) → Decidable (i s)] (f₁ : (i : I) → f i) (f₂ : (i : I) → f i) (g₁ : (i : I) → f i) (g₂ : (i : I) → f i) :
                                                  s.piecewise (f₁ + f₂) (g₁ + g₂) = s.piecewise f₁ g₁ + s.piecewise f₂ g₂
                                                  theorem Set.piecewise_mul {I : Type u} {f : IType v} [(i : I) → Mul (f i)] (s : Set I) [(i : I) → Decidable (i s)] (f₁ : (i : I) → f i) (f₂ : (i : I) → f i) (g₁ : (i : I) → f i) (g₂ : (i : I) → f i) :
                                                  s.piecewise (f₁ * f₂) (g₁ * g₂) = s.piecewise f₁ g₁ * s.piecewise f₂ g₂
                                                  theorem Set.piecewise_neg {I : Type u} {f : IType v} [(i : I) → Neg (f i)] (s : Set I) [(i : I) → Decidable (i s)] (f₁ : (i : I) → f i) (g₁ : (i : I) → f i) :
                                                  s.piecewise (-f₁) (-g₁) = -s.piecewise f₁ g₁
                                                  theorem Set.piecewise_inv {I : Type u} {f : IType v} [(i : I) → Inv (f i)] (s : Set I) [(i : I) → Decidable (i s)] (f₁ : (i : I) → f i) (g₁ : (i : I) → f i) :
                                                  s.piecewise f₁⁻¹ g₁⁻¹ = (s.piecewise f₁ g₁)⁻¹
                                                  theorem Set.piecewise_sub {I : Type u} {f : IType v} [(i : I) → Sub (f i)] (s : Set I) [(i : I) → Decidable (i s)] (f₁ : (i : I) → f i) (f₂ : (i : I) → f i) (g₁ : (i : I) → f i) (g₂ : (i : I) → f i) :
                                                  s.piecewise (f₁ - f₂) (g₁ - g₂) = s.piecewise f₁ g₁ - s.piecewise f₂ g₂
                                                  theorem Set.piecewise_div {I : Type u} {f : IType v} [(i : I) → Div (f i)] (s : Set I) [(i : I) → Decidable (i s)] (f₁ : (i : I) → f i) (f₂ : (i : I) → f i) (g₁ : (i : I) → f i) (g₂ : (i : I) → f i) :
                                                  s.piecewise (f₁ / f₂) (g₁ / g₂) = s.piecewise f₁ g₁ / s.piecewise f₂ g₂
                                                  theorem Function.ExtendByZero.hom.proof_1 {ι : Type u_3} {η : Type u_1} (R : Type u_2) (s : ιη) [AddZeroClass R] :
                                                  noncomputable def Function.ExtendByZero.hom {ι : Type u_1} {η : Type v} (R : Type w) (s : ιη) [AddZeroClass R] :
                                                  (ιR) →+ ηR

                                                  Function.extend s f 0 as a bundled hom.

                                                  Equations
                                                  Instances For
                                                    theorem Function.ExtendByZero.hom.proof_2 {ι : Type u_3} {η : Type u_1} (R : Type u_2) (s : ιη) [AddZeroClass R] (f : ιR) (g : ιR) :
                                                    { toFun := fun (f : ιR) => Function.extend s f 0, map_zero' := }.toFun (f + g) = { toFun := fun (f : ιR) => Function.extend s f 0, map_zero' := }.toFun f + { toFun := fun (f : ιR) => Function.extend s f 0, map_zero' := }.toFun g
                                                    @[simp]
                                                    theorem Function.ExtendByOne.hom_apply {ι : Type u_1} {η : Type v} (R : Type w) (s : ιη) [MulOneClass R] (f : ιR) :
                                                    ∀ (a : η), (Function.ExtendByOne.hom R s) f a = Function.extend s f 1 a
                                                    @[simp]
                                                    theorem Function.ExtendByZero.hom_apply {ι : Type u_1} {η : Type v} (R : Type w) (s : ιη) [AddZeroClass R] (f : ιR) :
                                                    ∀ (a : η), (Function.ExtendByZero.hom R s) f a = Function.extend s f 0 a
                                                    noncomputable def Function.ExtendByOne.hom {ι : Type u_1} {η : Type v} (R : Type w) (s : ιη) [MulOneClass R] :
                                                    (ιR) →* ηR

                                                    Function.extend s f 1 as a bundled hom.

                                                    Equations
                                                    Instances For
                                                      theorem Pi.single_mono {I : Type u} {f : IType v} (i : I) [DecidableEq I] [(i : I) → Preorder (f i)] [(i : I) → Zero (f i)] :
                                                      theorem Pi.mulSingle_mono {I : Type u} {f : IType v} (i : I) [DecidableEq I] [(i : I) → Preorder (f i)] [(i : I) → One (f i)] :
                                                      theorem Pi.single_strictMono {I : Type u} {f : IType v} (i : I) [DecidableEq I] [(i : I) → Preorder (f i)] [(i : I) → Zero (f i)] :
                                                      theorem Pi.mulSingle_strictMono {I : Type u} {f : IType v} (i : I) [DecidableEq I] [(i : I) → Preorder (f i)] [(i : I) → One (f i)] :
                                                      @[simp]
                                                      theorem Sigma.curry_zero {α : Type u_3} {β : αType u_4} {γ : (a : α) → β aType u_5} [(a : α) → (b : β a) → Zero (γ a b)] :
                                                      @[simp]
                                                      theorem Sigma.curry_one {α : Type u_3} {β : αType u_4} {γ : (a : α) → β aType u_5} [(a : α) → (b : β a) → One (γ a b)] :
                                                      @[simp]
                                                      theorem Sigma.uncurry_zero {α : Type u_3} {β : αType u_4} {γ : (a : α) → β aType u_5} [(a : α) → (b : β a) → Zero (γ a b)] :
                                                      @[simp]
                                                      theorem Sigma.uncurry_one {α : Type u_3} {β : αType u_4} {γ : (a : α) → β aType u_5} [(a : α) → (b : β a) → One (γ a b)] :
                                                      @[simp]
                                                      theorem Sigma.curry_add {α : Type u_3} {β : αType u_4} {γ : (a : α) → β aType u_5} [(a : α) → (b : β a) → Add (γ a b)] (x : (i : (a : α) × β a) → γ i.fst i.snd) (y : (i : (a : α) × β a) → γ i.fst i.snd) :
                                                      @[simp]
                                                      theorem Sigma.curry_mul {α : Type u_3} {β : αType u_4} {γ : (a : α) → β aType u_5} [(a : α) → (b : β a) → Mul (γ a b)] (x : (i : (a : α) × β a) → γ i.fst i.snd) (y : (i : (a : α) × β a) → γ i.fst i.snd) :
                                                      @[simp]
                                                      theorem Sigma.uncurry_add {α : Type u_3} {β : αType u_4} {γ : (a : α) → β aType u_5} [(a : α) → (b : β a) → Add (γ a b)] (x : (a : α) → (b : β a) → γ a b) (y : (a : α) → (b : β a) → γ a b) :
                                                      @[simp]
                                                      theorem Sigma.uncurry_mul {α : Type u_3} {β : αType u_4} {γ : (a : α) → β aType u_5} [(a : α) → (b : β a) → Mul (γ a b)] (x : (a : α) → (b : β a) → γ a b) (y : (a : α) → (b : β a) → γ a b) :
                                                      @[simp]
                                                      theorem Sigma.curry_neg {α : Type u_3} {β : αType u_4} {γ : (a : α) → β aType u_5} [(a : α) → (b : β a) → Neg (γ a b)] (x : (i : (a : α) × β a) → γ i.fst i.snd) :
                                                      @[simp]
                                                      theorem Sigma.curry_inv {α : Type u_3} {β : αType u_4} {γ : (a : α) → β aType u_5} [(a : α) → (b : β a) → Inv (γ a b)] (x : (i : (a : α) × β a) → γ i.fst i.snd) :
                                                      @[simp]
                                                      theorem Sigma.uncurry_neg {α : Type u_3} {β : αType u_4} {γ : (a : α) → β aType u_5} [(a : α) → (b : β a) → Neg (γ a b)] (x : (a : α) → (b : β a) → γ a b) :
                                                      @[simp]
                                                      theorem Sigma.uncurry_inv {α : Type u_3} {β : αType u_4} {γ : (a : α) → β aType u_5} [(a : α) → (b : β a) → Inv (γ a b)] (x : (a : α) → (b : β a) → γ a b) :
                                                      @[simp]
                                                      theorem Sigma.curry_single {α : Type u_3} {β : αType u_4} {γ : (a : α) → β aType u_5} [DecidableEq α] [(a : α) → DecidableEq (β a)] [(a : α) → (b : β a) → Zero (γ a b)] (i : (a : α) × β a) (x : γ i.fst i.snd) :
                                                      Sigma.curry (Pi.single i x) = Pi.single i.fst (Pi.single i.snd x)
                                                      @[simp]
                                                      theorem Sigma.curry_mulSingle {α : Type u_3} {β : αType u_4} {γ : (a : α) → β aType u_5} [DecidableEq α] [(a : α) → DecidableEq (β a)] [(a : α) → (b : β a) → One (γ a b)] (i : (a : α) × β a) (x : γ i.fst i.snd) :
                                                      @[simp]
                                                      theorem Sigma.uncurry_single_single {α : Type u_3} {β : αType u_4} {γ : (a : α) → β aType u_5} [DecidableEq α] [(a : α) → DecidableEq (β a)] [(a : α) → (b : β a) → Zero (γ a b)] (a : α) (b : β a) (x : γ a b) :
                                                      @[simp]
                                                      theorem Sigma.uncurry_mulSingle_mulSingle {α : Type u_3} {β : αType u_4} {γ : (a : α) → β aType u_5} [DecidableEq α] [(a : α) → DecidableEq (β a)] [(a : α) → (b : β a) → One (γ a b)] (a : α) (b : β a) (x : γ a b) :