Documentation

Mathlib.Algebra.Ring.Prod

Semiring, ring etc structures on R × S #

In this file we define two-binop (Semiring, Ring etc) structures on R × S. We also prove trivial simp lemmas, and define the following operations on RingHoms and similarly for NonUnitalRingHoms:

instance Prod.instDistrib {R : Type u_3} {S : Type u_5} [Distrib R] [Distrib S] :
Distrib (R × S)

Product of two distributive types is distributive.

Equations

Product of two NonUnitalNonAssocSemirings is a NonUnitalNonAssocSemiring.

Equations
  • One or more equations did not get rendered due to their size.

Product of two NonUnitalSemirings is a NonUnitalSemiring.

Equations

Product of two NonAssocSemirings is a NonAssocSemiring.

Equations
  • One or more equations did not get rendered due to their size.
instance Prod.instSemiring {R : Type u_3} {S : Type u_5} [Semiring R] [Semiring S] :
Semiring (R × S)

Product of two semirings is a semiring.

Equations
  • One or more equations did not get rendered due to their size.

Product of two NonUnitalCommSemirings is a NonUnitalCommSemiring.

Equations
instance Prod.instCommSemiring {R : Type u_3} {S : Type u_5} [CommSemiring R] [CommSemiring S] :

Product of two commutative semirings is a commutative semiring.

Equations
Equations
instance Prod.instNonUnitalRing {R : Type u_3} {S : Type u_5} [NonUnitalRing R] [NonUnitalRing S] :
Equations
instance Prod.instNonAssocRing {R : Type u_3} {S : Type u_5} [NonAssocRing R] [NonAssocRing S] :
Equations
  • One or more equations did not get rendered due to their size.
instance Prod.instRing {R : Type u_3} {S : Type u_5} [Ring R] [Ring S] :
Ring (R × S)

Product of two rings is a ring.

Equations
  • One or more equations did not get rendered due to their size.

Product of two NonUnitalCommRings is a NonUnitalCommRing.

Equations
instance Prod.instCommRing {R : Type u_3} {S : Type u_5} [CommRing R] [CommRing S] :
CommRing (R × S)

Product of two commutative rings is a commutative ring.

Equations

Given non-unital semirings R, S, the natural projection homomorphism from R × S to R.

Equations
Instances For

    Given non-unital semirings R, S, the natural projection homomorphism from R × S to S.

    Equations
    Instances For

      Combine two non-unital ring homomorphisms f : R →ₙ+* S, g : R →ₙ+* T into f.prod g : R →ₙ+* S × T given by (f.prod g) x = (f x, g x)

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        @[simp]
        theorem NonUnitalRingHom.prod_apply {R : Type u_3} {S : Type u_5} {T : Type u_7} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring T] (f : R →ₙ+* S) (g : R →ₙ+* T) (x : R) :
        (NonUnitalRingHom.prod f g) x = (f x, g x)
        def RingHom.fst (R : Type u_3) (S : Type u_5) [NonAssocSemiring R] [NonAssocSemiring S] :
        R × S →+* R

        Given semirings R, S, the natural projection homomorphism from R × S to R.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          def RingHom.snd (R : Type u_3) (S : Type u_5) [NonAssocSemiring R] [NonAssocSemiring S] :
          R × S →+* S

          Given semirings R, S, the natural projection homomorphism from R × S to S.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            @[simp]
            theorem RingHom.coe_fst {R : Type u_3} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] :
            (RingHom.fst R S) = Prod.fst
            @[simp]
            theorem RingHom.coe_snd {R : Type u_3} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] :
            (RingHom.snd R S) = Prod.snd
            def RingHom.prod {R : Type u_3} {S : Type u_5} {T : Type u_7} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring T] (f : R →+* S) (g : R →+* T) :
            R →+* S × T

            Combine two ring homomorphisms f : R →+* S, g : R →+* T into f.prod g : R →+* S × T given by (f.prod g) x = (f x, g x)

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              @[simp]
              theorem RingHom.prod_apply {R : Type u_3} {S : Type u_5} {T : Type u_7} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring T] (f : R →+* S) (g : R →+* T) (x : R) :
              (RingHom.prod f g) x = (f x, g x)
              @[simp]
              theorem RingHom.fst_comp_prod {R : Type u_3} {S : Type u_5} {T : Type u_7} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring T] (f : R →+* S) (g : R →+* T) :
              @[simp]
              theorem RingHom.snd_comp_prod {R : Type u_3} {S : Type u_5} {T : Type u_7} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring T] (f : R →+* S) (g : R →+* T) :
              def RingHom.prodMap {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] (f : R →+* R') (g : S →+* S') :
              R × S →+* R' × S'

              Prod.map as a RingHom.

              Equations
              Instances For
                theorem RingHom.prodMap_def {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] (f : R →+* R') (g : S →+* S') :
                @[simp]
                theorem RingHom.coe_prodMap {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] (f : R →+* R') (g : S →+* S') :
                (RingHom.prodMap f g) = Prod.map f g
                theorem RingHom.prod_comp_prodMap {R : Type u_3} {R' : Type u_4} {S : Type u_5} {S' : Type u_6} {T : Type u_7} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] [NonAssocSemiring T] (f : T →+* R) (g : T →+* S) (f' : R →+* R') (g' : S →+* S') :
                def RingEquiv.prodComm {R : Type u_3} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] :
                R × S ≃+* S × R

                Swapping components as an equivalence of (semi)rings.

                Equations
                • RingEquiv.prodComm = let __src := AddEquiv.prodComm; let __src_1 := MulEquiv.prodComm; { toEquiv := __src.toEquiv, map_mul' := , map_add' := }
                Instances For
                  @[simp]
                  theorem RingEquiv.coe_prodComm {R : Type u_3} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] :
                  RingEquiv.prodComm = Prod.swap
                  @[simp]
                  theorem RingEquiv.coe_prodComm_symm {R : Type u_3} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] :
                  (RingEquiv.symm RingEquiv.prodComm) = Prod.swap
                  @[simp]
                  theorem RingEquiv.fst_comp_coe_prodComm {R : Type u_3} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] :
                  RingHom.comp (RingHom.fst S R) RingEquiv.prodComm = RingHom.snd R S
                  @[simp]
                  theorem RingEquiv.snd_comp_coe_prodComm {R : Type u_3} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] :
                  RingHom.comp (RingHom.snd S R) RingEquiv.prodComm = RingHom.fst R S
                  @[simp]
                  theorem RingEquiv.prodProdProdComm_apply (R : Type u_3) (R' : Type u_4) (S : Type u_5) (S' : Type u_6) [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] (rrss : (R × R') × S × S') :
                  (RingEquiv.prodProdProdComm R R' S S') rrss = ((rrss.1.1, rrss.2.1), rrss.1.2, rrss.2.2)
                  def RingEquiv.prodProdProdComm (R : Type u_3) (R' : Type u_4) (S : Type u_5) (S' : Type u_6) [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring R'] [NonAssocSemiring S'] :
                  (R × R') × S × S' ≃+* (R × S) × R' × S'

                  Four-way commutativity of prod. The name matches mul_mul_mul_comm.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    @[simp]
                    @[simp]
                    theorem RingEquiv.prodZeroRing_apply (R : Type u_3) (S : Type u_5) [NonAssocSemiring R] [NonAssocSemiring S] [Subsingleton S] (x : R) :
                    (RingEquiv.prodZeroRing R S) x = (x, 0)
                    @[simp]
                    theorem RingEquiv.prodZeroRing_symm_apply (R : Type u_3) (S : Type u_5) [NonAssocSemiring R] [NonAssocSemiring S] [Subsingleton S] (self : R × S) :

                    A ring R is isomorphic to R × S when S is the zero ring

                    Equations
                    • RingEquiv.prodZeroRing R S = { toEquiv := { toFun := fun (x : R) => (x, 0), invFun := Prod.fst, left_inv := , right_inv := }, map_mul' := , map_add' := }
                    Instances For
                      @[simp]
                      theorem RingEquiv.zeroRingProd_symm_apply (R : Type u_3) (S : Type u_5) [NonAssocSemiring R] [NonAssocSemiring S] [Subsingleton S] (self : S × R) :
                      @[simp]
                      theorem RingEquiv.zeroRingProd_apply (R : Type u_3) (S : Type u_5) [NonAssocSemiring R] [NonAssocSemiring S] [Subsingleton S] (x : R) :
                      (RingEquiv.zeroRingProd R S) x = (0, x)

                      A ring R is isomorphic to S × R when S is the zero ring

                      Equations
                      • RingEquiv.zeroRingProd R S = { toEquiv := { toFun := fun (x : R) => (0, x), invFun := Prod.snd, left_inv := , right_inv := }, map_mul' := , map_add' := }
                      Instances For
                        theorem false_of_nontrivial_of_product_domain (R : Type u_9) (S : Type u_10) [Ring R] [Ring S] [IsDomain (R × S)] [Nontrivial R] [Nontrivial S] :

                        The product of two nontrivial rings is not a domain

                        Order #

                        instance instOrderedSemiringProd {α : Type u_1} {β : Type u_2} [OrderedSemiring α] [OrderedSemiring β] :
                        Equations
                        Equations
                        instance instOrderedRingProd {α : Type u_1} {β : Type u_2} [OrderedRing α] [OrderedRing β] :
                        OrderedRing (α × β)
                        Equations
                        instance instOrderedCommRingProd {α : Type u_1} {β : Type u_2} [OrderedCommRing α] [OrderedCommRing β] :
                        Equations