Documentation

Mathlib.Algebra.Ring.Pi

Pi instances for ring #

This file defines instances for ring, semiring and related structures on Pi Types

source
@[implicit_reducible]
instance Pi.distrib {I : Type u} {f : I → Type v} [(i : I) → Distrib (f i)] :
Distrib ((i : I) → f i)
source
@[implicit_reducible]
instance Pi.hasDistribNeg {I : Type u} {f : I → Type v} [(i : I) → Mul (f i)] [(i : I) → HasDistribNeg (f i)] :
HasDistribNeg ((i : I) → f i)
source
@[implicit_reducible]
instance Pi.addMonoidWithOne {I : Type u} {f : I → Type v} [(i : I) → AddMonoidWithOne (f i)] :
AddMonoidWithOne ((i : I) → f i)
source
@[implicit_reducible]
instance Pi.addGroupWithOne {I : Type u} {f : I → Type v} [(i : I) → AddGroupWithOne (f i)] :
AddGroupWithOne ((i : I) → f i)
source
@[implicit_reducible]
instance Pi.nonUnitalNonAssocSemiring {I : Type u} {f : I → Type v} [(i : I) → NonUnitalNonAssocSemiring (f i)] :
NonUnitalNonAssocSemiring ((i : I) → f i)
source
@[implicit_reducible]
instance Pi.nonUnitalSemiring {I : Type u} {f : I → Type v} [(i : I) → NonUnitalSemiring (f i)] :
NonUnitalSemiring ((i : I) → f i)
source
@[implicit_reducible]
instance Pi.nonAssocSemiring {I : Type u} {f : I → Type v} [(i : I) → NonAssocSemiring (f i)] :
NonAssocSemiring ((i : I) → f i)
source
@[implicit_reducible]
instance Pi.semiring {I : Type u} {f : I → Type v} [(i : I) → Semiring (f i)] :
Semiring ((i : I) → f i)
source
@[implicit_reducible]
instance Pi.nonUnitalCommSemiring {I : Type u} {f : I → Type v} [(i : I) → NonUnitalCommSemiring (f i)] :
NonUnitalCommSemiring ((i : I) → f i)
source
@[implicit_reducible]
instance Pi.commSemiring {I : Type u} {f : I → Type v} [(i : I) → CommSemiring (f i)] :
CommSemiring ((i : I) → f i)
source
@[implicit_reducible]
instance Pi.nonUnitalNonAssocRing {I : Type u} {f : I → Type v} [(i : I) → NonUnitalNonAssocRing (f i)] :
NonUnitalNonAssocRing ((i : I) → f i)
source
@[implicit_reducible]
instance Pi.nonUnitalRing {I : Type u} {f : I → Type v} [(i : I) → NonUnitalRing (f i)] :
NonUnitalRing ((i : I) → f i)
source
@[implicit_reducible]
instance Pi.nonAssocRing {I : Type u} {f : I → Type v} [(i : I) → NonAssocRing (f i)] :
NonAssocRing ((i : I) → f i)
source
@[implicit_reducible]
instance Pi.ring {I : Type u} {f : I → Type v} [(i : I) → Ring (f i)] :
Ring ((i : I) → f i)
source
@[implicit_reducible]
instance Pi.nonUnitalCommRing {I : Type u} {f : I → Type v} [(i : I) → NonUnitalCommRing (f i)] :
NonUnitalCommRing ((i : I) → f i)
source
@[implicit_reducible]
instance Pi.commRing {I : Type u} {f : I → Type v} [(i : I) → CommRing (f i)] :
CommRing ((i : I) → f i)
source
def NonUnitalRingHom.pi {I : Type u} {f : I → Type u_1} {γ : Type u_2} [(i : I) → NonUnitalNonAssocSemiring (f i)] [NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i) :
γ →ₙ+* (i : I) → f i

A family of non-unital ring homomorphisms f a : γ →ₙ+* β a defines a non-unital ring homomorphism NonUnitalRingHom.pi f : γ →+* Π a, β a given by NonUnitalRingHom.pi f x b = f b x.

Instances For
    source
    @[simp]
    theorem NonUnitalRingHom.pi_apply {I : Type u} {f : I → Type u_1} {γ : Type u_2} [(i : I) → NonUnitalNonAssocSemiring (f i)] [NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i) (x : γ) (b : I) :
    (pi g) x b = (g b) x
    source
    @[deprecated NonUnitalRingHom.pi (since := "2026-05-30")]
    def Pi.nonUnitalRingHom {I : Type u} {f : I → Type u_1} {γ : Type u_2} [(i : I) → NonUnitalNonAssocSemiring (f i)] [NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i) :
    γ →ₙ+* (i : I) → f i

    Alias of NonUnitalRingHom.pi.

    A family of non-unital ring homomorphisms f a : γ →ₙ+* β a defines a non-unital ring homomorphism NonUnitalRingHom.pi f : γ →+* Π a, β a given by NonUnitalRingHom.pi f x b = f b x.

    Instances For
      source
      @[deprecated NonUnitalRingHom.pi_apply (since := "2026-05-30")]
      theorem Pi.nonUnitalRingHom_apply {I : Type u} {f : I → Type u_1} {γ : Type u_2} [(i : I) → NonUnitalNonAssocSemiring (f i)] [NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i) (x : γ) (b : I) :
      (NonUnitalRingHom.pi g) x b = (g b) x

      Alias of NonUnitalRingHom.pi_apply.

      source
      theorem NonUnitalRingHom.pi_injective {I : Type u} {f : I → Type u_1} {γ : Type u_2} [Nonempty I] [(i : I) → NonUnitalNonAssocSemiring (f i)] [NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) :
      Function.Injective ⇑(pi g)
      source
      @[deprecated NonUnitalRingHom.pi_injective (since := "2026-05-30")]
      theorem Pi.nonUnitalRingHom_injective {I : Type u} {f : I → Type u_1} {γ : Type u_2} [Nonempty I] [(i : I) → NonUnitalNonAssocSemiring (f i)] [NonUnitalNonAssocSemiring γ] (g : (i : I) → γ →ₙ+* f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) :
      Function.Injective ⇑(NonUnitalRingHom.pi g)

      Alias of NonUnitalRingHom.pi_injective.

      source
      def Pi.evalNonUnitalRingHom {I : Type u} (f : I → Type v) [(i : I) → NonUnitalNonAssocSemiring (f i)] (i : I) :
      ((i : I) → f i) →ₙ+* f i

      Evaluation of functions into an indexed collection of non-unital rings at a point is a non-unital ring homomorphism. This is Function.eval as a NonUnitalRingHom.

      Instances For
        source
        @[simp]
        theorem Pi.evalNonUnitalRingHom_apply {I : Type u} (f : I → Type v) [(i : I) → NonUnitalNonAssocSemiring (f i)] (i : I) (g : (i : I) → f i) :
        (evalNonUnitalRingHom f i) g = g i
        source
        def Pi.constNonUnitalRingHom (α : Type u_1) (β : Type u_2) [NonUnitalNonAssocSemiring β] :
        β →ₙ+* α → β

        Function.const as a NonUnitalRingHom.

        Instances For
          source
          @[simp]
          theorem Pi.constNonUnitalRingHom_apply (α : Type u_1) (β : Type u_2) [NonUnitalNonAssocSemiring β] (a : β) (a✝ : α) :
          (constNonUnitalRingHom α β) a a✝ = Function.const α a a✝
          source
          def NonUnitalRingHom.compLeft {α : Type u_1} {β : Type u_2} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) (I : Type u_3) :
          (I → α) →ₙ+* I → β

          Non-unital ring homomorphism between the function spaces I → α and I → β, induced by a non-unital ring homomorphism f between α and β.

          Instances For
            source
            @[simp]
            theorem NonUnitalRingHom.compLeft_apply {α : Type u_1} {β : Type u_2} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) (I : Type u_3) (h : I → α) (a✝ : I) :
            (f.compLeft I) h a✝ = (⇑f ∘ h) a✝
            source
            def RingHom.pi {I : Type u} {f : I → Type u_1} {γ : Type u_2} [(i : I) → NonAssocSemiring (f i)] [NonAssocSemiring γ] (g : (i : I) → γ →+* f i) :
            γ →+* (i : I) → f i

            A family of ring homomorphisms f a : γ →+* β a defines a ring homomorphism RingHom.pi f : γ →+* Π a, β a given by RingHom.pi f x b = f b x.

            Instances For
              source
              @[simp]
              theorem RingHom.pi_apply {I : Type u} {f : I → Type u_1} {γ : Type u_2} [(i : I) → NonAssocSemiring (f i)] [NonAssocSemiring γ] (g : (i : I) → γ →+* f i) (x : γ) (b : I) :
              (RingHom.pi g) x b = (g b) x
              source
              @[deprecated RingHom.pi (since := "2026-05-30")]
              def Pi.ringHom {I : Type u} {f : I → Type u_1} {γ : Type u_2} [(i : I) → NonAssocSemiring (f i)] [NonAssocSemiring γ] (g : (i : I) → γ →+* f i) :
              γ →+* (i : I) → f i

              Alias of RingHom.pi.

              A family of ring homomorphisms f a : γ →+* β a defines a ring homomorphism RingHom.pi f : γ →+* Π a, β a given by RingHom.pi f x b = f b x.

              Instances For
                source
                @[deprecated RingHom.pi_apply (since := "2026-05-30")]
                theorem Pi.ringHom_apply {I : Type u} {f : I → Type u_1} {γ : Type u_2} [(i : I) → NonAssocSemiring (f i)] [NonAssocSemiring γ] (g : (i : I) → γ →+* f i) (x : γ) (b : I) :
                (RingHom.pi g) x b = (g b) x

                Alias of RingHom.pi_apply.

                source
                theorem RingHom.pi_injective {I : Type u} {f : I → Type u_1} {γ : Type u_2} [Nonempty I] [(i : I) → NonAssocSemiring (f i)] [NonAssocSemiring γ] (g : (i : I) → γ →+* f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) :
                Function.Injective ⇑(RingHom.pi g)
                source
                @[deprecated RingHom.pi_injective (since := "2026-05-30")]
                theorem Pi.ringHom_injective {I : Type u} {f : I → Type u_1} {γ : Type u_2} [Nonempty I] [(i : I) → NonAssocSemiring (f i)] [NonAssocSemiring γ] (g : (i : I) → γ →+* f i) (hg : ∀ (i : I), Function.Injective ⇑(g i)) :
                Function.Injective ⇑(RingHom.pi g)

                Alias of RingHom.pi_injective.

                source
                def Pi.evalRingHom {I : Type u} (f : I → Type v) [(i : I) → NonAssocSemiring (f i)] (i : I) :
                ((i : I) → f i) →+* f i

                Evaluation of functions into an indexed collection of rings at a point is a ring homomorphism. This is Function.eval as a RingHom.

                Instances For
                  source
                  @[simp]
                  theorem Pi.evalRingHom_apply {I : Type u} (f : I → Type v) [(i : I) → NonAssocSemiring (f i)] (i : I) (g : (i : I) → f i) :
                  (evalRingHom f i) g = g i
                  source
                  instance instRingHomSurjectiveForallEvalRingHom {I : Type u} (f : I → Type u_1) [(i : I) → Semiring (f i)] (i : I) :
                  RingHomSurjective (Pi.evalRingHom f i)
                  source
                  def Pi.constRingHom (α : Type u_1) (β : Type u_2) [NonAssocSemiring β] :
                  β →+* α → β

                  Function.const as a RingHom.

                  Instances For
                    source
                    @[simp]
                    theorem Pi.constRingHom_apply (α : Type u_1) (β : Type u_2) [NonAssocSemiring β] (a : β) (a✝ : α) :
                    (constRingHom α β) a a✝ = Function.const α a a✝
                    source
                    def RingHom.compLeft {α : Type u_1} {β : Type u_2} [NonAssocSemiring α] [NonAssocSemiring β] (f : α →+* β) (I : Type u_3) :
                    (I → α) →+* I → β

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

                    Instances For
                      source
                      @[simp]
                      theorem RingHom.compLeft_apply {α : Type u_1} {β : Type u_2} [NonAssocSemiring α] [NonAssocSemiring β] (f : α →+* β) (I : Type u_3) (h : I → α) (a✝ : I) :
                      (f.compLeft I) h a✝ = (⇑f ∘ h) a✝