Documentation

Mathlib.Algebra.Ring.Equiv

(Semi)ring equivs #

In this file we define an extension of Equiv called RingEquiv, which is a datatype representing an isomorphism of Semirings, Rings, DivisionRings, or Fields.

Notations #

The extended equiv have coercions to functions, and the coercion is the canonical notation when treating the isomorphism as maps.

Implementation notes #

The fields for RingEquiv now avoid the unbundled isMulHom and isAddHom, as these are deprecated.

Definition of multiplication in the groups of automorphisms agrees with function composition, multiplication in Equiv.Perm, and multiplication in CategoryTheory.End, not with CategoryTheory.CategoryStruct.comp.

Tags #

Equiv, MulEquiv, AddEquiv, RingEquiv, MulAut, AddAut, RingAut

@[simp]
theorem NonUnitalRingHom.inverse_apply {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (g : SR) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
∀ (a : S), (NonUnitalRingHom.inverse f g h₁ h₂) a = g a
def NonUnitalRingHom.inverse {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R →ₙ+* S) (g : SR) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :

makes a NonUnitalRingHom from the bijective inverse of a NonUnitalRingHom

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem RingHom.inverse_apply {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (g : SR) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
    ∀ (a : S), (RingHom.inverse f g h₁ h₂) a = g a
    def RingHom.inverse {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (g : SR) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) :
    S →+* R

    makes a RingHom from the bijective inverse of a RingHom

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      structure RingEquiv (R : Type u_7) (S : Type u_8) [Mul R] [Mul S] [Add R] [Add S] extends Equiv :
      Type (max u_7 u_8)

      An equivalence between two (non-unital non-associative semi)rings that preserves the algebraic structure.

      • toFun : RS
      • invFun : SR
      • left_inv : Function.LeftInverse self.invFun self.toFun
      • right_inv : Function.RightInverse self.invFun self.toFun
      • map_mul' : ∀ (x y : R), self.toFun (x * y) = self.toFun x * self.toFun y

        The proposition that the function preserves multiplication

      • map_add' : ∀ (x y : R), self.toFun (x + y) = self.toFun x + self.toFun y

        The proposition that the function preserves addition

      Instances For
        @[reducible]
        abbrev RingEquiv.toAddEquiv {R : Type u_7} {S : Type u_8} [Mul R] [Mul S] [Add R] [Add S] (self : R ≃+* S) :
        R ≃+ S

        The equivalence of additive monoids underlying an equivalence of (semi)rings.

        Equations
        Instances For
          @[reducible]
          abbrev RingEquiv.toMulEquiv {R : Type u_7} {S : Type u_8} [Mul R] [Mul S] [Add R] [Add S] (self : R ≃+* S) :
          R ≃* S

          The equivalence of multiplicative monoids underlying an equivalence of (semi)rings.

          Equations
          Instances For
            class RingEquivClass (F : Type u_7) (R : Type u_8) (S : Type u_9) [Mul R] [Add R] [Mul S] [Add S] [EquivLike F R S] extends MulEquivClass :

            RingEquivClass F R S states that F is a type of ring structure preserving equivalences. You should extend this class when you extend RingEquiv.

            • map_mul : ∀ (f : F) (a b : R), f (a * b) = f a * f b
            • map_add : ∀ (f : F) (a b : R), f (a + b) = f a + f b

              By definition, a ring isomorphism preserves the additive structure.

            Instances
              instance RingEquivClass.toAddEquivClass {F : Type u_1} {R : Type u_4} {S : Type u_5} [EquivLike F R S] [Mul R] [Add R] [Mul S] [Add S] [h : RingEquivClass F R S] :
              Equations
              • =
              instance RingEquivClass.toRingHomClass {F : Type u_1} {R : Type u_4} {S : Type u_5} [EquivLike F R S] [NonAssocSemiring R] [NonAssocSemiring S] [h : RingEquivClass F R S] :
              Equations
              • =
              def RingEquivClass.toRingEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [Mul β] [Add β] [EquivLike F α β] [RingEquivClass F α β] (f : F) :
              α ≃+* β

              Turn an element of a type F satisfying RingEquivClass F α β into an actual RingEquiv. This is declared as the default coercion from F to α ≃+* β.

              Equations
              • f = let __src := f; let __src_1 := f; { toEquiv := __src.toEquiv, map_mul' := , map_add' := }
              Instances For
                instance instCoeTCRingEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [Mul α] [Add α] [Mul β] [Add β] [EquivLike F α β] [RingEquivClass F α β] :
                CoeTC F (α ≃+* β)

                Any type satisfying RingEquivClass can be cast into RingEquiv via RingEquivClass.toRingEquiv.

                Equations
                • instCoeTCRingEquiv = { coe := RingEquivClass.toRingEquiv }
                instance RingEquiv.instEquivLikeRingEquiv {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] :
                EquivLike (R ≃+* S) R S
                Equations
                • RingEquiv.instEquivLikeRingEquiv = { coe := fun (f : R ≃+* S) => f.toFun, inv := fun (f : R ≃+* S) => f.invFun, left_inv := , right_inv := , coe_injective' := }
                Equations
                • =
                @[simp]
                theorem RingEquiv.toEquiv_eq_coe {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (f : R ≃+* S) :
                f.toEquiv = f
                @[simp]
                theorem RingEquiv.coe_toEquiv {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (f : R ≃+* S) :
                f = f
                theorem RingEquiv.map_mul {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (e : R ≃+* S) (x : R) (y : R) :
                e (x * y) = e x * e y

                A ring isomorphism preserves multiplication.

                theorem RingEquiv.map_add {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (e : R ≃+* S) (x : R) (y : R) :
                e (x + y) = e x + e y

                A ring isomorphism preserves addition.

                theorem RingEquiv.ext {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] {f : R ≃+* S} {g : R ≃+* S} (h : ∀ (x : R), f x = g x) :
                f = g

                Two ring isomorphisms agree if they are defined by the same underlying function.

                @[simp]
                theorem RingEquiv.coe_mk {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (e : R S) (h₃ : ∀ (x y : R), e.toFun (x * y) = e.toFun x * e.toFun y) (h₄ : ∀ (x y : R), e.toFun (x + y) = e.toFun x + e.toFun y) :
                { toEquiv := e, map_mul' := h₃, map_add' := h₄ } = e
                @[simp]
                theorem RingEquiv.mk_coe {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (e : R ≃+* S) (e' : SR) (h₁ : Function.LeftInverse e' e) (h₂ : Function.RightInverse e' e) (h₃ : ∀ (x y : R), { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y) (h₄ : ∀ (x y : R), { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }.toFun y) :
                { toEquiv := { toFun := e, invFun := e', left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ } = e
                theorem RingEquiv.congr_arg {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] {f : R ≃+* S} {x : R} {x' : R} :
                x = x'f x = f x'
                theorem RingEquiv.congr_fun {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] {f : R ≃+* S} {g : R ≃+* S} (h : f = g) (x : R) :
                f x = g x
                theorem RingEquiv.ext_iff {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] {f : R ≃+* S} {g : R ≃+* S} :
                f = g ∀ (x : R), f x = g x
                @[simp]
                theorem RingEquiv.toAddEquiv_eq_coe {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (f : R ≃+* S) :
                @[simp]
                theorem RingEquiv.toMulEquiv_eq_coe {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (f : R ≃+* S) :
                @[simp]
                theorem RingEquiv.coe_toMulEquiv {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (f : R ≃+* S) :
                f = f
                @[simp]
                theorem RingEquiv.coe_toAddEquiv {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (f : R ≃+* S) :
                f = f
                def RingEquiv.ringEquivOfUnique {M : Type u_7} {N : Type u_8} [Unique M] [Unique N] [Add M] [Mul M] [Add N] [Mul N] :
                M ≃+* N

                The RingEquiv between two semirings with a unique element.

                Equations
                • RingEquiv.ringEquivOfUnique = let __src := AddEquiv.addEquivOfUnique; let __src_1 := MulEquiv.mulEquivOfUnique; { toEquiv := __src.toEquiv, map_mul' := , map_add' := }
                Instances For
                  instance RingEquiv.instUniqueRingEquiv {M : Type u_7} {N : Type u_8} [Unique M] [Unique N] [Add M] [Mul M] [Add N] [Mul N] :
                  Equations
                  • RingEquiv.instUniqueRingEquiv = { toInhabited := { default := RingEquiv.ringEquivOfUnique }, uniq := }
                  def RingEquiv.refl (R : Type u_4) [Mul R] [Add R] :
                  R ≃+* R

                  The identity map is a ring isomorphism.

                  Equations
                  Instances For
                    @[simp]
                    theorem RingEquiv.refl_apply (R : Type u_4) [Mul R] [Add R] (x : R) :
                    @[simp]
                    @[simp]
                    def RingEquiv.symm {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (e : R ≃+* S) :
                    S ≃+* R

                    The inverse of a ring isomorphism is a ring isomorphism.

                    Equations
                    Instances For
                      def RingEquiv.Simps.symm_apply {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (e : R ≃+* S) :
                      SR

                      See Note [custom simps projection]

                      Equations
                      Instances For
                        @[simp]
                        theorem RingEquiv.invFun_eq_symm {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (f : R ≃+* S) :
                        @[simp]
                        theorem RingEquiv.symm_symm {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (e : R ≃+* S) :
                        @[simp]
                        theorem RingEquiv.coe_toEquiv_symm {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (e : R ≃+* S) :
                        (RingEquiv.symm e) = (e).symm
                        theorem RingEquiv.symm_bijective {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] :
                        Function.Bijective RingEquiv.symm
                        @[simp]
                        theorem RingEquiv.mk_coe' {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (e : R ≃+* S) (f : SR) (h₁ : Function.LeftInverse (e) f) (h₂ : Function.RightInverse (e) f) (h₃ : ∀ (x y : S), { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun y) (h₄ : ∀ (x y : S), { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }.toFun y) :
                        { toEquiv := { toFun := f, invFun := e, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ } = RingEquiv.symm e
                        @[simp]
                        theorem RingEquiv.symm_mk {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (f : RS) (g : SR) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) (h₃ : ∀ (x y : R), { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂ }.toFun (x * y) = { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂ }.toFun x * { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂ }.toFun y) (h₄ : ∀ (x y : R), { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂ }.toFun (x + y) = { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂ }.toFun x + { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂ }.toFun y) :
                        RingEquiv.symm { toEquiv := { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ } = let __src := RingEquiv.symm { toEquiv := { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂ }, map_mul' := h₃, map_add' := h₄ }; { toEquiv := { toFun := g, invFun := f, left_inv := , right_inv := }, map_mul' := , map_add' := }
                        def RingEquiv.trans {R : Type u_4} {S : Type u_5} {S' : Type u_6} [Mul R] [Mul S] [Add R] [Add S] [Mul S'] [Add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
                        R ≃+* S'

                        Transitivity of RingEquiv.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          theorem RingEquiv.trans_apply {R : Type u_4} {S : Type u_5} {S' : Type u_6} [Mul R] [Mul S] [Add R] [Add S] [Mul S'] [Add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') (a : R) :
                          (RingEquiv.trans e₁ e₂) a = e₂ (e₁ a)
                          @[simp]
                          theorem RingEquiv.coe_trans {R : Type u_4} {S : Type u_5} {S' : Type u_6} [Mul R] [Mul S] [Add R] [Add S] [Mul S'] [Add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
                          (RingEquiv.trans e₁ e₂) = e₂ e₁
                          @[simp]
                          theorem RingEquiv.symm_trans_apply {R : Type u_4} {S : Type u_5} {S' : Type u_6} [Mul R] [Mul S] [Add R] [Add S] [Mul S'] [Add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') (a : S') :
                          theorem RingEquiv.symm_trans {R : Type u_4} {S : Type u_5} {S' : Type u_6} [Mul R] [Mul S] [Add R] [Add S] [Mul S'] [Add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
                          theorem RingEquiv.bijective {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (e : R ≃+* S) :
                          theorem RingEquiv.injective {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (e : R ≃+* S) :
                          theorem RingEquiv.surjective {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (e : R ≃+* S) :
                          @[simp]
                          theorem RingEquiv.apply_symm_apply {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (e : R ≃+* S) (x : S) :
                          e ((RingEquiv.symm e) x) = x
                          @[simp]
                          theorem RingEquiv.symm_apply_apply {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (e : R ≃+* S) (x : R) :
                          (RingEquiv.symm e) (e x) = x
                          theorem RingEquiv.image_eq_preimage {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (e : R ≃+* S) (s : Set R) :
                          e '' s = (RingEquiv.symm e) ⁻¹' s
                          @[simp]
                          theorem RingEquiv.coe_mulEquiv_trans {R : Type u_4} {S : Type u_5} {S' : Type u_6} [Mul R] [Mul S] [Add R] [Add S] [Mul S'] [Add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
                          (RingEquiv.trans e₁ e₂) = MulEquiv.trans e₁ e₂
                          @[simp]
                          theorem RingEquiv.coe_addEquiv_trans {R : Type u_4} {S : Type u_5} {S' : Type u_6} [Mul R] [Mul S] [Add R] [Add S] [Mul S'] [Add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
                          (RingEquiv.trans e₁ e₂) = AddEquiv.trans e₁ e₂
                          @[simp]
                          theorem RingEquiv.op_apply_symm_apply {α : Type u_7} {β : Type u_8} [Add α] [Mul α] [Add β] [Mul β] (f : α ≃+* β) :
                          ∀ (a : βᵐᵒᵖ), (RingEquiv.symm (RingEquiv.op f)) a = MulOpposite.op ((AddEquiv.symm f) (MulOpposite.unop a))
                          @[simp]
                          theorem RingEquiv.op_symm_apply_apply {α : Type u_7} {β : Type u_8} [Add α] [Mul α] [Add β] [Mul β] (f : αᵐᵒᵖ ≃+* βᵐᵒᵖ) :
                          ∀ (a : α), (RingEquiv.op.symm f) a = MulOpposite.unop (f (MulOpposite.op a))
                          @[simp]
                          theorem RingEquiv.op_apply_apply {α : Type u_7} {β : Type u_8} [Add α] [Mul α] [Add β] [Mul β] (f : α ≃+* β) :
                          ∀ (a : αᵐᵒᵖ), (RingEquiv.op f) a = MulOpposite.op (f (MulOpposite.unop a))
                          @[simp]
                          theorem RingEquiv.op_symm_apply_symm_apply {α : Type u_7} {β : Type u_8} [Add α] [Mul α] [Add β] [Mul β] (f : αᵐᵒᵖ ≃+* βᵐᵒᵖ) :
                          ∀ (a : β), (RingEquiv.symm (RingEquiv.op.symm f)) a = MulOpposite.unop ((AddEquiv.symm f) (MulOpposite.op a))
                          def RingEquiv.op {α : Type u_7} {β : Type u_8} [Add α] [Mul α] [Add β] [Mul β] :

                          A ring iso α ≃+* β can equivalently be viewed as a ring iso αᵐᵒᵖ ≃+* βᵐᵒᵖ.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            def RingEquiv.unop {α : Type u_7} {β : Type u_8} [Add α] [Mul α] [Add β] [Mul β] :

                            The 'unopposite' of a ring iso αᵐᵒᵖ ≃+* βᵐᵒᵖ. Inverse to RingEquiv.op.

                            Equations
                            • RingEquiv.unop = RingEquiv.op.symm
                            Instances For
                              @[simp]
                              theorem RingEquiv.opOp_apply (R : Type u_7) [Add R] [Mul R] :

                              A ring is isomorphic to the opposite of its opposite.

                              Equations
                              Instances For

                                A non-unital commutative ring is isomorphic to its opposite.

                                Equations
                                • RingEquiv.toOpposite R = let __src := MulOpposite.opEquiv; { toEquiv := __src, map_mul' := , map_add' := }
                                Instances For
                                  theorem RingEquiv.map_zero {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R ≃+* S) :
                                  f 0 = 0

                                  A ring isomorphism sends zero to zero.

                                  theorem RingEquiv.map_eq_zero_iff {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R ≃+* S) {x : R} :
                                  f x = 0 x = 0
                                  theorem RingEquiv.map_ne_zero_iff {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R ≃+* S) {x : R} :
                                  f x 0 x 0
                                  noncomputable def RingEquiv.ofBijective {F : Type u_1} {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [FunLike F R S] [NonUnitalRingHomClass F R S] (f : F) (hf : Function.Bijective f) :
                                  R ≃+* S

                                  Produce a ring isomorphism from a bijective ring homomorphism.

                                  Equations
                                  Instances For
                                    @[simp]
                                    theorem RingEquiv.coe_ofBijective {F : Type u_1} {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [FunLike F R S] [NonUnitalRingHomClass F R S] (f : F) (hf : Function.Bijective f) :
                                    (RingEquiv.ofBijective f hf) = f
                                    theorem RingEquiv.ofBijective_apply {F : Type u_1} {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [FunLike F R S] [NonUnitalRingHomClass F R S] (f : F) (hf : Function.Bijective f) (x : R) :
                                    @[simp]
                                    theorem RingEquiv.piCongrRight_apply {ι : Type u_7} {R : ιType u_8} {S : ιType u_9} [(i : ι) → NonUnitalNonAssocSemiring (R i)] [(i : ι) → NonUnitalNonAssocSemiring (S i)] (e : (i : ι) → R i ≃+* S i) (x : (i : ι) → R i) (j : ι) :
                                    (RingEquiv.piCongrRight e) x j = (e j) (x j)
                                    def RingEquiv.piCongrRight {ι : Type u_7} {R : ιType u_8} {S : ιType u_9} [(i : ι) → NonUnitalNonAssocSemiring (R i)] [(i : ι) → NonUnitalNonAssocSemiring (S i)] (e : (i : ι) → R i ≃+* S i) :
                                    ((i : ι) → R i) ≃+* ((i : ι) → S i)

                                    A family of ring isomorphisms ∀ j, (R j ≃+* S j) generates a ring isomorphisms between ∀ j, R j and ∀ j, S j.

                                    This is the RingEquiv version of Equiv.piCongrRight, and the dependent version of RingEquiv.arrowCongr.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For
                                      @[simp]
                                      theorem RingEquiv.piCongrRight_refl {ι : Type u_7} {R : ιType u_8} [(i : ι) → NonUnitalNonAssocSemiring (R i)] :
                                      (RingEquiv.piCongrRight fun (i : ι) => RingEquiv.refl (R i)) = RingEquiv.refl ((i : ι) → R i)
                                      @[simp]
                                      theorem RingEquiv.piCongrRight_symm {ι : Type u_7} {R : ιType u_8} {S : ιType u_9} [(i : ι) → NonUnitalNonAssocSemiring (R i)] [(i : ι) → NonUnitalNonAssocSemiring (S i)] (e : (i : ι) → R i ≃+* S i) :
                                      @[simp]
                                      theorem RingEquiv.piCongrRight_trans {ι : Type u_7} {R : ιType u_8} {S : ιType u_9} {T : ιType u_10} [(i : ι) → NonUnitalNonAssocSemiring (R i)] [(i : ι) → NonUnitalNonAssocSemiring (S i)] [(i : ι) → NonUnitalNonAssocSemiring (T i)] (e : (i : ι) → R i ≃+* S i) (f : (i : ι) → S i ≃+* T i) :
                                      theorem RingEquiv.map_one {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (f : R ≃+* S) :
                                      f 1 = 1

                                      A ring isomorphism sends one to one.

                                      theorem RingEquiv.map_eq_one_iff {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (f : R ≃+* S) {x : R} :
                                      f x = 1 x = 1
                                      theorem RingEquiv.map_ne_one_iff {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (f : R ≃+* S) {x : R} :
                                      f x 1 x 1

                                      RingEquiv.coe_mulEquiv_refl and RingEquiv.coe_addEquiv_refl are proved above in higher generality

                                      @[simp]
                                      theorem RingEquiv.coe_monoidHom_trans {R : Type u_4} {S : Type u_5} {S' : Type u_6} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
                                      (RingEquiv.trans e₁ e₂) = MonoidHom.comp e₂ e₁
                                      @[simp]
                                      theorem RingEquiv.coe_addMonoidHom_trans {R : Type u_4} {S : Type u_5} {S' : Type u_6} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
                                      (RingEquiv.trans e₁ e₂) = AddMonoidHom.comp e₂ e₁

                                      RingEquiv.coe_mulEquiv_trans and RingEquiv.coe_addEquiv_trans are proved above in higher generality

                                      @[simp]
                                      theorem RingEquiv.coe_ringHom_trans {R : Type u_4} {S : Type u_5} {S' : Type u_6} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
                                      (RingEquiv.trans e₁ e₂) = RingHom.comp e₂ e₁
                                      @[simp]
                                      theorem RingEquiv.comp_symm {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (e : R ≃+* S) :
                                      @[simp]
                                      theorem RingEquiv.symm_comp {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (e : R ≃+* S) :
                                      theorem RingEquiv.map_neg {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R ≃+* S) (x : R) :
                                      f (-x) = -f x
                                      theorem RingEquiv.map_sub {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocRing R] [NonUnitalNonAssocRing S] (f : R ≃+* S) (x : R) (y : R) :
                                      f (x - y) = f x - f y
                                      theorem RingEquiv.map_neg_one {R : Type u_4} {S : Type u_5} [NonAssocRing R] [NonAssocRing S] (f : R ≃+* S) :
                                      f (-1) = -1
                                      theorem RingEquiv.map_eq_neg_one_iff {R : Type u_4} {S : Type u_5} [NonAssocRing R] [NonAssocRing S] (f : R ≃+* S) {x : R} :
                                      f x = -1 x = -1

                                      Reinterpret a ring equivalence as a non-unital ring homomorphism.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For
                                        @[simp]
                                        theorem RingEquiv.coe_toNonUnitalRingHom {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R ≃+* S) :
                                        f = f
                                        theorem RingEquiv.coe_nonUnitalRingHom_inj_iff {R : Type u_7} {S : Type u_8} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R ≃+* S) (g : R ≃+* S) :
                                        f = g f = g
                                        def RingEquiv.toRingHom {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (e : R ≃+* S) :
                                        R →+* S

                                        Reinterpret a ring equivalence as a ring homomorphism.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          theorem RingEquiv.toRingHom_injective {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] :
                                          Function.Injective RingEquiv.toRingHom
                                          @[simp]
                                          theorem RingEquiv.toRingHom_eq_coe {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (f : R ≃+* S) :
                                          @[simp]
                                          theorem RingEquiv.coe_toRingHom {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (f : R ≃+* S) :
                                          f = f
                                          theorem RingEquiv.coe_ringHom_inj_iff {R : Type u_7} {S : Type u_8} [NonAssocSemiring R] [NonAssocSemiring S] (f : R ≃+* S) (g : R ≃+* S) :
                                          f = g f = g
                                          @[simp]
                                          theorem RingEquiv.toNonUnitalRingHom_commutes {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (f : R ≃+* S) :
                                          f = f

                                          The two paths coercion can take to a NonUnitalRingEquiv are equivalent

                                          @[inline, reducible]
                                          abbrev RingEquiv.toMonoidHom {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (e : R ≃+* S) :
                                          R →* S

                                          Reinterpret a ring equivalence as a monoid homomorphism.

                                          Equations
                                          Instances For
                                            @[inline, reducible]
                                            abbrev RingEquiv.toAddMonoidHom {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (e : R ≃+* S) :
                                            R →+ S

                                            Reinterpret a ring equivalence as an AddMonoid homomorphism.

                                            Equations
                                            Instances For

                                              The two paths coercion can take to an AddMonoidHom are equivalent

                                              theorem RingEquiv.toMonoidHom_commutes {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (f : R ≃+* S) :
                                              f = MulEquiv.toMonoidHom f

                                              The two paths coercion can take to a MonoidHom are equivalent

                                              theorem RingEquiv.toEquiv_commutes {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (f : R ≃+* S) :
                                              (f).toEquiv = (f).toEquiv

                                              The two paths coercion can take to an Equiv are equivalent

                                              @[simp]
                                              theorem RingEquiv.toRingHom_trans {R : Type u_4} {S : Type u_5} {S' : Type u_6} [NonAssocSemiring R] [NonAssocSemiring S] [NonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
                                              @[simp]
                                              theorem RingEquiv.ofHomInv'_symm_apply {R : Type u_7} {S : Type u_8} {F : Type u_9} {G : Type u_10} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [FunLike F R S] [FunLike G S R] [NonUnitalRingHomClass F R S] [NonUnitalRingHomClass G S R] (hom : F) (inv : G) (hom_inv_id : NonUnitalRingHom.comp inv hom = NonUnitalRingHom.id R) (inv_hom_id : NonUnitalRingHom.comp hom inv = NonUnitalRingHom.id S) (a : S) :
                                              (RingEquiv.symm (RingEquiv.ofHomInv' hom inv hom_inv_id inv_hom_id)) a = inv a
                                              @[simp]
                                              theorem RingEquiv.ofHomInv'_apply {R : Type u_7} {S : Type u_8} {F : Type u_9} {G : Type u_10} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [FunLike F R S] [FunLike G S R] [NonUnitalRingHomClass F R S] [NonUnitalRingHomClass G S R] (hom : F) (inv : G) (hom_inv_id : NonUnitalRingHom.comp inv hom = NonUnitalRingHom.id R) (inv_hom_id : NonUnitalRingHom.comp hom inv = NonUnitalRingHom.id S) (a : R) :
                                              (RingEquiv.ofHomInv' hom inv hom_inv_id inv_hom_id) a = hom a
                                              def RingEquiv.ofHomInv' {R : Type u_7} {S : Type u_8} {F : Type u_9} {G : Type u_10} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [FunLike F R S] [FunLike G S R] [NonUnitalRingHomClass F R S] [NonUnitalRingHomClass G S R] (hom : F) (inv : G) (hom_inv_id : NonUnitalRingHom.comp inv hom = NonUnitalRingHom.id R) (inv_hom_id : NonUnitalRingHom.comp hom inv = NonUnitalRingHom.id S) :
                                              R ≃+* S

                                              Construct an equivalence of rings from homomorphisms in both directions, which are inverses.

                                              Equations
                                              • RingEquiv.ofHomInv' hom inv hom_inv_id inv_hom_id = { toEquiv := { toFun := hom, invFun := inv, left_inv := , right_inv := }, map_mul' := , map_add' := }
                                              Instances For
                                                @[simp]
                                                theorem RingEquiv.ofHomInv_apply {R : Type u_7} {S : Type u_8} {F : Type u_9} {G : Type u_10} [NonAssocSemiring R] [NonAssocSemiring S] [FunLike F R S] [FunLike G S R] [RingHomClass F R S] [RingHomClass G S R] (hom : F) (inv : G) (hom_inv_id : RingHom.comp inv hom = RingHom.id R) (inv_hom_id : RingHom.comp hom inv = RingHom.id S) (a : R) :
                                                (RingEquiv.ofHomInv hom inv hom_inv_id inv_hom_id) a = hom a
                                                @[simp]
                                                theorem RingEquiv.ofHomInv_symm_apply {R : Type u_7} {S : Type u_8} {F : Type u_9} {G : Type u_10} [NonAssocSemiring R] [NonAssocSemiring S] [FunLike F R S] [FunLike G S R] [RingHomClass F R S] [RingHomClass G S R] (hom : F) (inv : G) (hom_inv_id : RingHom.comp inv hom = RingHom.id R) (inv_hom_id : RingHom.comp hom inv = RingHom.id S) (a : S) :
                                                (RingEquiv.symm (RingEquiv.ofHomInv hom inv hom_inv_id inv_hom_id)) a = inv a
                                                def RingEquiv.ofHomInv {R : Type u_7} {S : Type u_8} {F : Type u_9} {G : Type u_10} [NonAssocSemiring R] [NonAssocSemiring S] [FunLike F R S] [FunLike G S R] [RingHomClass F R S] [RingHomClass G S R] (hom : F) (inv : G) (hom_inv_id : RingHom.comp inv hom = RingHom.id R) (inv_hom_id : RingHom.comp hom inv = RingHom.id S) :
                                                R ≃+* S

                                                Construct an equivalence of rings from unital homomorphisms in both directions, which are inverses.

                                                Equations
                                                • RingEquiv.ofHomInv hom inv hom_inv_id inv_hom_id = { toEquiv := { toFun := hom, invFun := inv, left_inv := , right_inv := }, map_mul' := , map_add' := }
                                                Instances For
                                                  theorem RingEquiv.map_pow {R : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] (f : R ≃+* S) (a : R) (n : ) :
                                                  f (a ^ n) = f a ^ n
                                                  theorem RingEquiv.isUnit_iff {R : Type u_4} {S : Type u_5} [Semiring R] [Semiring S] (f : R ≃+* S) {a : R} :
                                                  IsUnit (f a) IsUnit a
                                                  def MulEquiv.toRingEquiv {R : Type u_7} {S : Type u_8} {F : Type u_9} [Add R] [Add S] [Mul R] [Mul S] [EquivLike F R S] [MulEquivClass F R S] (f : F) (H : ∀ (x y : R), f (x + y) = f x + f y) :
                                                  R ≃+* S

                                                  Gives a RingEquiv from an element of a MulEquivClass preserving addition.

                                                  Equations
                                                  • MulEquiv.toRingEquiv f H = let __src := (f).toEquiv; let __src_1 := f; let __src_2 := AddEquiv.mk' (f).toEquiv H; { toEquiv := __src, map_mul' := , map_add' := }
                                                  Instances For
                                                    def AddEquiv.toRingEquiv {R : Type u_7} {S : Type u_8} {F : Type u_9} [Add R] [Add S] [Mul R] [Mul S] [EquivLike F R S] [AddEquivClass F R S] (f : F) (H : ∀ (x y : R), f (x * y) = f x * f y) :
                                                    R ≃+* S

                                                    Gives a RingEquiv from an element of an AddEquivClass preserving addition.

                                                    Equations
                                                    • AddEquiv.toRingEquiv f H = let __src := (f).toEquiv; let __src_1 := f; let __src_2 := MulEquiv.mk' (f).toEquiv H; { toEquiv := __src, map_mul' := , map_add' := }
                                                    Instances For
                                                      @[simp]
                                                      theorem RingEquiv.self_trans_symm {R : Type u_4} {S : Type u_5} [Add R] [Add S] [Mul R] [Mul S] (e : R ≃+* S) :
                                                      @[simp]
                                                      theorem RingEquiv.symm_trans_self {R : Type u_4} {S : Type u_5} [Add R] [Add S] [Mul R] [Mul S] (e : R ≃+* S) :
                                                      theorem MulEquiv.noZeroDivisors {A : Type u_7} (B : Type u_8) [MulZeroClass A] [MulZeroClass B] [NoZeroDivisors B] (e : A ≃* B) :

                                                      If two rings are isomorphic, and the second doesn't have zero divisors, then so does the first.

                                                      theorem MulEquiv.isDomain {A : Type u_7} (B : Type u_8) [Semiring A] [Semiring B] [IsDomain B] (e : A ≃* B) :

                                                      If two rings are isomorphic, and the second is a domain, then so is the first.

                                                      theorem MulEquiv.isField {A : Type u_7} (B : Type u_8) [Semiring A] [Semiring B] (hB : IsField B) (e : A ≃* B) :