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

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

makes a NonUnitalRingHom from the bijective inverse of a NonUnitalRingHom

Equations
  • f.inverse g h₁ h₂ = { toFun := g, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
source
@[simp]
theorem RingHom.inverse_apply {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (g : S → R) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) :
∀ (a : S), (f.inverse g h₁ h₂) a = g a
source
def RingHom.inverse {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (g : S → R) (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f) :
S →+* R

makes a RingHom from the bijective inverse of a RingHom

Equations
  • f.inverse g h₁ h₂ = { toFun := g, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
source
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 : R → S
  • invFun : S → R
  • 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

source
def «term_≃+*_» :
Lean.TrailingParserDescr

Notation for RingEquiv.

Equations
source
@[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
  • self.toAddEquiv = { toEquiv := self.toEquiv, map_add' := ⋯ }
source
@[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
  • self.toMulEquiv = { toEquiv := self.toEquiv, map_mul' := ⋯ }
source
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 :
Prop

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
    source
    theorem RingEquivClass.map_add {F : Type u_7} {R : Type u_8} {S : Type u_9} :
    ∀ {inst : Mul R} {inst_1 : Add R} {inst_2 : Mul S} {inst_3 : Add S} {inst_4 : EquivLike F R S} [self : RingEquivClass F R S] (f : F) (a b : R), f (a + b) = f a + f b

    By definition, a ring isomorphism preserves the additive structure.

    source
    @[instance 100]
    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] :
    AddEquivClass F R S
    Equations
    • ⋯ = ⋯
    source
    @[instance 100]
    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] :
    RingHomClass F R S
    Equations
    • ⋯ = ⋯
    source
    @[instance 100]
    instance RingEquivClass.toNonUnitalRingHomClass {F : Type u_1} {R : Type u_4} {S : Type u_5} [EquivLike F R S] [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [h : RingEquivClass F R S] :
    NonUnitalRingHomClass F R S
    Equations
    • ⋯ = ⋯
    source
    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 = { toEquiv := (↑f).toEquiv, map_mul' := ⋯, map_add' := ⋯ }
    source
    instance instCoeTCRingEquivOfRingEquivClass {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
    • instCoeTCRingEquivOfRingEquivClass = { coe := RingEquivClass.toRingEquiv }
    source
    instance RingEquiv.instEquivLike {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] :
    EquivLike (R ≃+* S) R S
    Equations
    • RingEquiv.instEquivLike = { coe := fun (f : R ≃+* S) => f.toFun, inv := fun (f : R ≃+* S) => f.invFun, left_inv := ⋯, right_inv := ⋯, coe_injective' := ⋯ }
    source
    instance RingEquiv.instRingEquivClass {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] :
    RingEquivClass (R ≃+* S) R S
    Equations
    • ⋯ = ⋯
    source
    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
    source
    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.

    source
    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'
    source
    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
    source
    @[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
    source
    @[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' : S → R) (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) :
    { toFun := ⇑e, invFun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ } = e
    source
    @[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
    source
    @[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
    source
    @[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) :
    f.toAddEquiv = ↑f
    source
    @[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) :
    f.toMulEquiv = ↑f
    source
    @[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
    source
    @[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
    source
    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.

    source
    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.

    source
    theorem RingEquiv.bijective {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (e : R ≃+* S) :
    Function.Bijective ⇑e
    source
    theorem RingEquiv.injective {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (e : R ≃+* S) :
    Function.Injective ⇑e
    source
    theorem RingEquiv.surjective {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (e : R ≃+* S) :
    Function.Surjective ⇑e
    source
    def RingEquiv.refl (R : Type u_4) [Mul R] [Add R] :
    R ≃+* R

    The identity map is a ring isomorphism.

    Equations
    source
    instance RingEquiv.instInhabited (R : Type u_4) [Mul R] [Add R] :
    Inhabited (R ≃+* R)
    Equations
    source
    @[simp]
    theorem RingEquiv.refl_apply (R : Type u_4) [Mul R] [Add R] (x : R) :
    (RingEquiv.refl R) x = x
    source
    @[simp]
    theorem RingEquiv.coe_addEquiv_refl (R : Type u_4) [Mul R] [Add R] :
    ↑(RingEquiv.refl R) = AddEquiv.refl R
    source
    @[simp]
    theorem RingEquiv.coe_mulEquiv_refl (R : Type u_4) [Mul R] [Add R] :
    ↑(RingEquiv.refl R) = MulEquiv.refl R
    source
    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
    • e.symm = { toEquiv := e.toMulEquiv.symm.toEquiv, map_mul' := ⋯, map_add' := ⋯ }
    source
    @[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) :
    EquivLike.inv f = ⇑f.symm
    source
    @[simp]
    theorem RingEquiv.symm_symm {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (e : R ≃+* S) :
    e.symm.symm = e
    source
    theorem RingEquiv.symm_bijective {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] :
    Function.Bijective RingEquiv.symm
    source
    @[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 : S → R) (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) :
    { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ } = e.symm
    source
    def RingEquiv.symm_mk.aux {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (f : R → S) (g : S → R) (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) :
    S ≃+* R

    Auxiliary definition to avoid looping in dsimp with RingEquiv.symm_mk.

    Equations
    • RingEquiv.symm_mk.aux f g h₁ h₂ h₃ h₄ = { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.symm
    source
    @[simp]
    theorem RingEquiv.symm_mk {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (f : R → S) (g : S → R) (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) :
    { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄ }.symm = let __src := RingEquiv.symm_mk.aux f g h₁ h₂ h₃ h₄; { toFun := g, invFun := f, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
    source
    @[simp]
    theorem RingEquiv.symm_refl {R : Type u_4} [Mul R] [Add R] :
    (RingEquiv.refl R).symm = RingEquiv.refl R
    source
    @[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) :
    ↑e.symm = (↑e).symm
    source
    @[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 (e.symm x) = x
    source
    @[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) :
    e.symm (e x) = x
    source
    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 = ⇑e.symm ⁻¹' s
    source
    def RingEquiv.Simps.symm_apply {R : Type u_4} {S : Type u_5} [Mul R] [Mul S] [Add R] [Add S] (e : R ≃+* S) :
    S → R

    See Note [custom simps projection]

    Equations
    source
    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
    • e₁.trans e₂ = { toEquiv := (e₁.toMulEquiv.trans e₂.toMulEquiv).toEquiv, map_mul' := ⋯, map_add' := ⋯ }
    source
    @[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') :
    ⇑(e₁.trans e₂) = ⇑e₂ ∘ ⇑e₁
    source
    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) :
    (e₁.trans e₂) a = e₂ (e₁ a)
    source
    @[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') :
    (e₁.trans e₂).symm a = e₁.symm (e₂.symm a)
    source
    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') :
    (e₁.trans e₂).symm = e₂.symm.trans e₁.symm
    source
    @[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') :
    ↑(e₁.trans e₂) = (↑e₁).trans ↑e₂
    source
    @[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') :
    ↑(e₁.trans e₂) = (↑e₁).trans ↑e₂
    source
    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 = { toEquiv := AddEquiv.addEquivOfUnique.toEquiv, map_mul' := ⋯, map_add' := ⋯ }
    source
    instance RingEquiv.instUnique {M : Type u_7} {N : Type u_8} [Unique M] [Unique N] [Add M] [Mul M] [Add N] [Mul N] :
    Unique (M ≃+* N)
    Equations
    • RingEquiv.instUnique = { default := RingEquiv.ringEquivOfUnique, uniq := ⋯ }
    source
    @[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))
    source
    @[simp]
    theorem RingEquiv.op_symm_apply_symm_apply {α : Type u_7} {β : Type u_8} [Add α] [Mul α] [Add β] [Mul β] (f : αᵐᵒᵖ ≃+* βᵐᵒᵖ) :
    ∀ (a : β), (RingEquiv.op.symm f).symm a = MulOpposite.unop ((↑f).symm (MulOpposite.op a))
    source
    @[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))
    source
    @[simp]
    theorem RingEquiv.op_apply_symm_apply {α : Type u_7} {β : Type u_8} [Add α] [Mul α] [Add β] [Mul β] (f : α ≃+* β) :
    ∀ (a : βᵐᵒᵖ), (RingEquiv.op f).symm a = MulOpposite.op ((↑f).symm (MulOpposite.unop a))
    source
    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.
    source
    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
    source
    @[simp]
    theorem RingEquiv.opOp_apply (R : Type u_7) [Add R] [Mul R] :
    ∀ (a : R), (RingEquiv.opOp R) a = MulOpposite.op (MulOpposite.op a)
    source
    @[simp]
    theorem RingEquiv.opOp_symm_apply (R : Type u_7) [Add R] [Mul R] :
    ∀ (a : Rᵐᵒᵖᵐᵒᵖ), (RingEquiv.opOp R).symm a = MulOpposite.unop (MulOpposite.unop a)
    source
    def RingEquiv.opOp (R : Type u_7) [Add R] [Mul R] :
    R ≃+* Rᵐᵒᵖᵐᵒᵖ

    A ring is isomorphic to the opposite of its opposite.

    Equations
    source
    def RingEquiv.toOpposite (R : Type u_4) [NonUnitalCommSemiring R] :
    R ≃+* Rᵐᵒᵖ

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

    Equations
    source
    @[simp]
    theorem RingEquiv.toOpposite_apply (R : Type u_4) [NonUnitalCommSemiring R] (r : R) :
    (RingEquiv.toOpposite R) r = MulOpposite.op r
    source
    @[simp]
    theorem RingEquiv.toOpposite_symm_apply (R : Type u_4) [NonUnitalCommSemiring R] (r : Rᵐᵒᵖ) :
    (RingEquiv.toOpposite R).symm r = MulOpposite.unop r
    source
    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.

    source
    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
    source
    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
    source
    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
    source
    @[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
    source
    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) :
    (RingEquiv.ofBijective f hf) x = f x
    source
    @[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)
    source
    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.
    source
    @[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)
    source
    @[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) :
    (RingEquiv.piCongrRight e).symm = RingEquiv.piCongrRight fun (i : ι) => (e i).symm
    source
    @[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) :
    (RingEquiv.piCongrRight e).trans (RingEquiv.piCongrRight f) = RingEquiv.piCongrRight fun (i : ι) => (e i).trans (f i)
    source
    @[simp]
    theorem RingEquiv.piCongrLeft'_symm_apply {ι : Type u_7} {ι' : Type u_8} (R : ι → Type u_9) (e : ι ≃ ι') [(i : ι) → NonUnitalNonAssocSemiring (R i)] (f : (b : ι') → R (e.symm b)) (x : ι) :
    (RingEquiv.piCongrLeft' R e).symm f x = ⋯ ▸ f (e x)
    source
    @[simp]
    theorem RingEquiv.piCongrLeft'_apply {ι : Type u_7} {ι' : Type u_8} (R : ι → Type u_9) (e : ι ≃ ι') [(i : ι) → NonUnitalNonAssocSemiring (R i)] (f : (a : ι) → R a) (x : ι') :
    (RingEquiv.piCongrLeft' R e) f x = f (e.symm x)
    source
    def RingEquiv.piCongrLeft' {ι : Type u_7} {ι' : Type u_8} (R : ι → Type u_9) (e : ι ≃ ι') [(i : ι) → NonUnitalNonAssocSemiring (R i)] :
    ((i : ι) → R i) ≃+* ((i : ι') → R (e.symm i))

    Transport dependent functions through an equivalence of the base space.

    This is Equiv.piCongrLeft' as a RingEquiv.

    Equations
    source
    @[simp]
    theorem RingEquiv.piCongrLeft'_symm {α : Type u_2} {β : Type u_3} {R : Type u_7} [NonUnitalNonAssocSemiring R] (e : α ≃ β) :
    (RingEquiv.piCongrLeft' (fun (x : α) => R) e).symm = RingEquiv.piCongrLeft' (fun (i : β) => R) e.symm
    source
    @[simp]
    theorem RingEquiv.piCongrLeft_symm_apply {ι : Type u_7} {ι' : Type u_8} (S : ι' → Type u_9) (e : ι ≃ ι') [(i : ι') → NonUnitalNonAssocSemiring (S i)] :
    ∀ (a : (i : ι') → S i) (i : ι), (RingEquiv.piCongrLeft S e).symm a i = (RingEquiv.piCongrLeft' S e.symm) a i
    source
    @[simp]
    theorem RingEquiv.piCongrLeft_apply {ι : Type u_7} {ι' : Type u_8} (S : ι' → Type u_9) (e : ι ≃ ι') [(i : ι') → NonUnitalNonAssocSemiring (S i)] :
    ∀ (a : (i : ι) → S (e.symm.symm i)) (i : ι'), (RingEquiv.piCongrLeft S e) a i = (↑(RingEquiv.piCongrLeft' S e.symm)).symm a i
    source
    def RingEquiv.piCongrLeft {ι : Type u_7} {ι' : Type u_8} (S : ι' → Type u_9) (e : ι ≃ ι') [(i : ι') → NonUnitalNonAssocSemiring (S i)] :
    ((i : ι) → S (e i)) ≃+* ((i : ι') → S i)

    Transport dependent functions through an equivalence of the base space.

    This is Equiv.piCongrLeft as a RingEquiv.

    Equations
    source
    @[simp]
    theorem RingEquiv.piEquivPiSubtypeProd_apply {ι : Type u_7} (p : ι → Prop) [DecidablePred p] (Y : ι → Type u_8) [(i : ι) → NonUnitalNonAssocSemiring (Y i)] (f : (i : ι) → Y i) :
    (RingEquiv.piEquivPiSubtypeProd p Y) f = (fun (x : { x : ι // p x }) => f ↑x, fun (x : { x : ι // ¬p x }) => f ↑x)
    source
    @[simp]
    theorem RingEquiv.piEquivPiSubtypeProd_symm_apply {ι : Type u_7} (p : ι → Prop) [DecidablePred p] (Y : ι → Type u_8) [(i : ι) → NonUnitalNonAssocSemiring (Y i)] (f : ((i : { x : ι // p x }) → Y ↑i) × ((i : { x : ι // ¬p x }) → Y ↑i)) (x : ι) :
    (RingEquiv.piEquivPiSubtypeProd p Y).symm f x = if h : p x then f.1 ⟨x, h⟩ else f.2 ⟨x, h⟩
    source
    def RingEquiv.piEquivPiSubtypeProd {ι : Type u_7} (p : ι → Prop) [DecidablePred p] (Y : ι → Type u_8) [(i : ι) → NonUnitalNonAssocSemiring (Y i)] :
    ((i : ι) → Y i) ≃+* ((i : { x : ι // p x }) → Y ↑i) × ((i : { x : ι // ¬p x }) → Y ↑i)

    Splits the indices of ring ∀ (i : ι), Y i along the predicate p. This is Equiv.piEquivPiSubtypeProd as a RingEquiv.

    Equations
    source
    @[simp]
    theorem RingEquiv.prodCongr_apply {R : Type u_7} {R' : Type u_8} {S : Type u_9} {S' : Type u_10} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring S'] (f : R ≃+* R') (g : S ≃+* S') :
    ∀ (a : R × S), (f.prodCongr g) a = Prod.map (⇑f) (⇑g) a
    source
    @[simp]
    theorem RingEquiv.prodCongr_symm_apply {R : Type u_7} {R' : Type u_8} {S : Type u_9} {S' : Type u_10} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring S'] (f : R ≃+* R') (g : S ≃+* S') :
    ∀ (a : R' × S'), (f.prodCongr g).symm a = Prod.map (⇑(↑f).symm) (⇑(↑g).symm) a
    source
    def RingEquiv.prodCongr {R : Type u_7} {R' : Type u_8} {S : Type u_9} {S' : Type u_10} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring S'] (f : R ≃+* R') (g : S ≃+* S') :
    R × S ≃+* R' × S'

    Product of ring equivalences. This is Equiv.prodCongr as a RingEquiv.

    Equations
    • f.prodCongr g = { toEquiv := (↑f).prodCongr ↑g, map_mul' := ⋯, map_add' := ⋯ }
    source
    @[simp]
    theorem RingEquiv.coe_prodCongr {R : Type u_7} {R' : Type u_8} {S : Type u_9} {S' : Type u_10} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring R'] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring S'] (f : R ≃+* R') (g : S ≃+* S') :
    ⇑(f.prodCongr g) = Prod.map ⇑f ⇑g
    source
    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.

    source
    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
    source
    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
    source
    theorem RingEquiv.coe_monoidHom_refl {R : Type u_4} [NonAssocSemiring R] :
    ↑(RingEquiv.refl R) = MonoidHom.id R
    source
    @[simp]
    theorem RingEquiv.coe_addMonoidHom_refl {R : Type u_4} [NonAssocSemiring R] :
    ↑(RingEquiv.refl R) = AddMonoidHom.id R

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

    source
    @[simp]
    theorem RingEquiv.coe_ringHom_refl {R : Type u_4} [NonAssocSemiring R] :
    ↑(RingEquiv.refl R) = RingHom.id R
    source
    @[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') :
    ↑(e₁.trans e₂) = (↑e₂).comp ↑e₁
    source
    @[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') :
    ↑(e₁.trans e₂) = (↑e₂).comp ↑e₁

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

    source
    @[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') :
    ↑(e₁.trans e₂) = (↑e₂).comp ↑e₁
    source
    @[simp]
    theorem RingEquiv.comp_symm {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (e : R ≃+* S) :
    (↑e).comp ↑e.symm = RingHom.id S
    source
    @[simp]
    theorem RingEquiv.symm_comp {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (e : R ≃+* S) :
    (↑e.symm).comp ↑e = RingHom.id R
    source
    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
    source
    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
    source
    @[simp]
    theorem RingEquiv.map_neg_one {R : Type u_4} {S : Type u_5} [NonAssocRing R] [NonAssocRing S] (f : R ≃+* S) :
    f (-1) = -1
    source
    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
    source
    def RingEquiv.toNonUnitalRingHom {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (e : R ≃+* S) :
    R →ₙ+* S

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

    Equations
    • e.toNonUnitalRingHom = { toMulHom := e.toMulEquiv.toMulHom, map_zero' := ⋯, map_add' := ⋯ }
    source
    theorem RingEquiv.toNonUnitalRingHom_injective {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] :
    Function.Injective RingEquiv.toNonUnitalRingHom
    source
    theorem RingEquiv.toNonUnitalRingHom_eq_coe {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R ≃+* S) :
    f.toNonUnitalRingHom = ↑f
    source
    @[simp]
    theorem RingEquiv.coe_toNonUnitalRingHom {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (f : R ≃+* S) :
    ⇑↑f = ⇑f
    source
    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
    source
    @[simp]
    theorem RingEquiv.toNonUnitalRingHom_refl {R : Type u_4} [NonUnitalNonAssocSemiring R] :
    (RingEquiv.refl R).toNonUnitalRingHom = NonUnitalRingHom.id R
    source
    @[simp]
    theorem RingEquiv.toNonUnitalRingHom_apply_symm_toNonUnitalRingHom_apply {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (e : R ≃+* S) (y : S) :
    e.toNonUnitalRingHom (e.symm.toNonUnitalRingHom y) = y
    source
    @[simp]
    theorem RingEquiv.symm_toNonUnitalRingHom_apply_toNonUnitalRingHom_apply {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (e : R ≃+* S) (x : R) :
    e.symm.toNonUnitalRingHom (e.toNonUnitalRingHom x) = x
    source
    @[simp]
    theorem RingEquiv.toNonUnitalRingHom_trans {R : Type u_4} {S : Type u_5} {S' : Type u_6} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] [NonUnitalNonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
    (e₁.trans e₂).toNonUnitalRingHom = e₂.toNonUnitalRingHom.comp e₁.toNonUnitalRingHom
    source
    @[simp]
    theorem RingEquiv.toNonUnitalRingHomm_comp_symm_toNonUnitalRingHom {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (e : R ≃+* S) :
    e.toNonUnitalRingHom.comp e.symm.toNonUnitalRingHom = NonUnitalRingHom.id S
    source
    @[simp]
    theorem RingEquiv.symm_toNonUnitalRingHom_comp_toNonUnitalRingHom {R : Type u_4} {S : Type u_5} [NonUnitalNonAssocSemiring R] [NonUnitalNonAssocSemiring S] (e : R ≃+* S) :
    e.symm.toNonUnitalRingHom.comp e.toNonUnitalRingHom = NonUnitalRingHom.id R
    source
    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
    • e.toRingHom = { toMonoidHom := e.toMulEquiv.toMonoidHom, map_zero' := ⋯, map_add' := ⋯ }
    source
    theorem RingEquiv.toRingHom_injective {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] :
    Function.Injective RingEquiv.toRingHom
    source
    @[simp]
    theorem RingEquiv.toRingHom_eq_coe {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (f : R ≃+* S) :
    f.toRingHom = ↑f
    source
    @[simp]
    theorem RingEquiv.coe_toRingHom {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (f : R ≃+* S) :
    ⇑↑f = ⇑f
    source
    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
    source
    @[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

    source
    @[reducible, inline]
    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
    • e.toMonoidHom = ↑e.toRingHom
    source
    @[reducible, inline]
    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
    • e.toAddMonoidHom = e.toRingHom.toAddMonoidHom
    source
    theorem RingEquiv.toAddMonoidMom_commutes {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (f : R ≃+* S) :
    (↑f).toAddMonoidHom = (↑f).toAddMonoidHom

    The two paths coercion can take to an AddMonoidHom are equivalent

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

    The two paths coercion can take to a MonoidHom are equivalent

    source
    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

    source
    @[simp]
    theorem RingEquiv.toRingHom_refl {R : Type u_4} [NonAssocSemiring R] :
    (RingEquiv.refl R).toRingHom = RingHom.id R
    source
    @[simp]
    theorem RingEquiv.toMonoidHom_refl {R : Type u_4} [NonAssocSemiring R] :
    (RingEquiv.refl R).toMonoidHom = MonoidHom.id R
    source
    @[simp]
    theorem RingEquiv.toAddMonoidHom_refl {R : Type u_4} [NonAssocSemiring R] :
    (RingEquiv.refl R).toAddMonoidHom = AddMonoidHom.id R
    source
    theorem RingEquiv.toRingHom_apply_symm_toRingHom_apply {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (e : R ≃+* S) (y : S) :
    e.toRingHom (e.symm.toRingHom y) = y
    source
    theorem RingEquiv.symm_toRingHom_apply_toRingHom_apply {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (e : R ≃+* S) (x : R) :
    e.symm.toRingHom (e.toRingHom x) = x
    source
    @[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') :
    (e₁.trans e₂).toRingHom = e₂.toRingHom.comp e₁.toRingHom
    source
    theorem RingEquiv.toRingHom_comp_symm_toRingHom {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (e : R ≃+* S) :
    e.toRingHom.comp e.symm.toRingHom = RingHom.id S
    source
    theorem RingEquiv.symm_toRingHom_comp_toRingHom {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (e : R ≃+* S) :
    e.symm.toRingHom.comp e.toRingHom = RingHom.id R
    source
    @[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 : (↑inv).comp ↑hom = NonUnitalRingHom.id R) (inv_hom_id : (↑hom).comp ↑inv = NonUnitalRingHom.id S) (a : S) :
    (RingEquiv.ofHomInv' hom inv hom_inv_id inv_hom_id).symm a = inv a
    source
    @[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 : (↑inv).comp ↑hom = NonUnitalRingHom.id R) (inv_hom_id : (↑hom).comp ↑inv = NonUnitalRingHom.id S) (a : R) :
    (RingEquiv.ofHomInv' hom inv hom_inv_id inv_hom_id) a = hom a
    source
    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 : (↑inv).comp ↑hom = NonUnitalRingHom.id R) (inv_hom_id : (↑hom).comp ↑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 = { toFun := ⇑hom, invFun := ⇑inv, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
    source
    @[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 : (↑inv).comp ↑hom = RingHom.id R) (inv_hom_id : (↑hom).comp ↑inv = RingHom.id S) (a : S) :
    (RingEquiv.ofHomInv hom inv hom_inv_id inv_hom_id).symm a = inv a
    source
    @[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 : (↑inv).comp ↑hom = RingHom.id R) (inv_hom_id : (↑hom).comp ↑inv = RingHom.id S) (a : R) :
    (RingEquiv.ofHomInv hom inv hom_inv_id inv_hom_id) a = hom a
    source
    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 : (↑inv).comp ↑hom = RingHom.id R) (inv_hom_id : (↑hom).comp ↑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 = { toFun := ⇑hom, invFun := ⇑inv, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
    source
    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
    source
    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
    source
    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
    source
    @[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) :
    e.trans e.symm = RingEquiv.refl R
    source
    @[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) :
    e.symm.trans e = RingEquiv.refl S
    source
    @[simp]
    theorem RingEquiv.ofRingHom_symm_apply {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (g : S →+* R) (h₁ : f.comp g = RingHom.id S) (h₂ : g.comp f = RingHom.id R) (a : S) :
    (RingEquiv.ofRingHom f g h₁ h₂).symm a = g a
    source
    @[simp]
    theorem RingEquiv.ofRingHom_apply {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (g : S →+* R) (h₁ : f.comp g = RingHom.id S) (h₂ : g.comp f = RingHom.id R) (a : R) :
    (RingEquiv.ofRingHom f g h₁ h₂) a = f a
    source
    def RingEquiv.ofRingHom {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (g : S →+* R) (h₁ : f.comp g = RingHom.id S) (h₂ : g.comp f = RingHom.id R) :
    R ≃+* S

    If a ring homomorphism has an inverse, it is a ring isomorphism.

    Equations
    • RingEquiv.ofRingHom f g h₁ h₂ = { toFun := ⇑f, invFun := ⇑g, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯, map_add' := ⋯ }
    source
    theorem RingEquiv.coe_ringHom_ofRingHom {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (g : S →+* R) (h₁ : f.comp g = RingHom.id S) (h₂ : g.comp f = RingHom.id R) :
    ↑(RingEquiv.ofRingHom f g h₁ h₂) = f
    source
    @[simp]
    theorem RingEquiv.ofRingHom_coe_ringHom {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (f : R ≃+* S) (g : S →+* R) (h₁ : (↑f).comp g = RingHom.id S) (h₂ : g.comp ↑f = RingHom.id R) :
    RingEquiv.ofRingHom (↑f) g h₁ h₂ = f
    source
    theorem RingEquiv.ofRingHom_symm {R : Type u_4} {S : Type u_5} [NonAssocSemiring R] [NonAssocSemiring S] (f : R →+* S) (g : S →+* R) (h₁ : f.comp g = RingHom.id S) (h₂ : g.comp f = RingHom.id R) :
    (RingEquiv.ofRingHom f g h₁ h₂).symm = RingEquiv.ofRingHom g f h₂ h₁
    source
    theorem MulEquiv.noZeroDivisors {A : Type u_7} (B : Type u_8) [MulZeroClass A] [MulZeroClass B] [NoZeroDivisors B] (e : A ≃* B) :
    NoZeroDivisors A

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

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

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