# mathlib3documentation

algebra.ring.equiv

# (Semi)ring equivs #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

In this file we define extension of `equiv` called `ring_equiv`, which is a datatype representing an isomorphism of `semiring`s, `ring`s, `division_ring`s, or `field`s. We also introduce the corresponding group of automorphisms `ring_aut`.

## Notations #

• `infix ` ≃+* `:25 := ring_equiv`

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 `ring_equiv` now avoid the unbundled `is_mul_hom` and `is_add_hom`, as these are deprecated.

Definition of multiplication in the groups of automorphisms agrees with function composition, multiplication in `equiv.perm`, and multiplication in `category_theory.End`, not with `category_theory.comp`.

## Tags #

structure ring_equiv (R : Type u_7) (S : Type u_8) [has_mul R] [has_add R] [has_mul S] [has_add S] :
Type (max u_7 u_8)

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

Instances for `ring_equiv`
def ring_equiv.to_mul_equiv {R : Type u_7} {S : Type u_8} [has_mul R] [has_add R] [has_mul S] [has_add S] (self : R ≃+* S) :
R ≃* S

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

def ring_equiv.to_add_equiv {R : Type u_7} {S : Type u_8} [has_mul R] [has_add R] [has_mul S] [has_add S] (self : R ≃+* S) :
R ≃+ S

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

def ring_equiv.to_equiv {R : Type u_7} {S : Type u_8} [has_mul R] [has_add R] [has_mul S] [has_add S] (self : R ≃+* S) :
R S

The "plain" equivalence of types underlying an equivalence of (semi)rings.

@[class]
structure ring_equiv_class (F : Type u_7) (R : out_param (Type u_8)) (S : out_param (Type u_9)) [has_mul R] [has_add R] [has_mul S] [has_add S] :
Type (max u_7 u_8 u_9)

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

Instances of this typeclass
Instances of other typeclasses for `ring_equiv_class`
• ring_equiv_class.has_sizeof_inst
@[instance]
def ring_equiv_class.to_mul_equiv_class (F : Type u_7) (R : out_param (Type u_8)) (S : out_param (Type u_9)) [has_mul R] [has_add R] [has_mul S] [has_add S] [self : S] :
S
@[protected, instance]
def ring_equiv_class.to_add_equiv_class (F : Type u_1) (R : Type u_2) (S : Type u_3) [has_mul R] [has_add R] [has_mul S] [has_add S] [h : S] :
S
Equations
@[protected, instance]
def ring_equiv_class.to_ring_hom_class (F : Type u_1) (R : Type u_2) (S : Type u_3) [h : S] :
S
Equations
@[protected, instance]
def ring_equiv_class.to_non_unital_ring_hom_class (F : Type u_1) (R : Type u_2) (S : Type u_3) [h : S] :
Equations
@[protected, instance]
def ring_equiv.has_coe_t {F : Type u_1} {α : Type u_2} {β : Type u_3} [has_mul α] [has_add α] [has_mul β] [has_add β] [ β] :
≃+* β)
Equations
@[protected, instance]
def ring_equiv.ring_equiv_class {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] :
Equations
@[protected, instance]
def ring_equiv.has_coe_to_fun {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] :
has_coe_to_fun (R ≃+* S) (λ (_x : R ≃+* S), R S)
Equations
@[simp]
theorem ring_equiv.to_equiv_eq_coe {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (f : R ≃+* S) :
@[simp]
theorem ring_equiv.to_fun_eq_coe {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (f : R ≃+* S) :
@[simp]
theorem ring_equiv.coe_to_equiv {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (f : R ≃+* S) :
@[protected]
theorem ring_equiv.map_mul {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) (x y : R) :
e (x * y) = e x * e y

A ring isomorphism preserves multiplication.

@[protected]
theorem ring_equiv.map_add {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) (x y : R) :
e (x + y) = e x + e y

@[ext]
theorem ring_equiv.ext {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] {f 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 ring_equiv.coe_mk {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R S) (e' : S R) (h₁ : e) (h₂ : e) (h₃ : (x y : R), e (x * y) = e x * e y) (h₄ : (x y : R), e (x + y) = e x + e y) :
{to_fun := e, inv_fun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄} = e
@[simp]
theorem ring_equiv.mk_coe {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) (e' : S R) (h₁ : e) (h₂ : e) (h₃ : (x y : R), e (x * y) = e x * e y) (h₄ : (x y : R), e (x + y) = e x + e y) :
{to_fun := e, inv_fun := e', left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄} = e
@[protected]
theorem ring_equiv.congr_arg {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] {f : R ≃+* S} {x x' : R} :
x = x' f x = f x'
@[protected]
theorem ring_equiv.congr_fun {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] {f g : R ≃+* S} (h : f = g) (x : R) :
f x = g x
@[protected]
theorem ring_equiv.ext_iff {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] {f g : R ≃+* S} :
f = g (x : R), f x = g x
@[simp]
theorem ring_equiv.to_add_equiv_eq_coe {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (f : R ≃+* S) :
@[simp]
theorem ring_equiv.to_mul_equiv_eq_coe {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (f : R ≃+* S) :
@[simp, norm_cast]
theorem ring_equiv.coe_to_mul_equiv {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (f : R ≃+* S) :
@[simp, norm_cast]
theorem ring_equiv.coe_to_add_equiv {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (f : R ≃+* S) :
def ring_equiv.ring_equiv_of_unique {M : Type u_1} {N : Type u_2} [unique M] [unique N] [has_add M] [has_mul M] [has_add N] [has_mul N] :
M ≃+* N

The `ring_equiv` between two semirings with a unique element.

Equations
@[protected, instance]
def ring_equiv.unique {M : Type u_1} {N : Type u_2} [unique M] [unique N] [has_add M] [has_mul M] [has_add N] [has_mul N] :
Equations
@[protected, refl]
def ring_equiv.refl (R : Type u_4) [has_mul R] [has_add R] :
R ≃+* R

The identity map is a ring isomorphism.

Equations
@[simp]
theorem ring_equiv.refl_apply (R : Type u_4) [has_mul R] [has_add R] (x : R) :
x = x
@[simp]
@[simp]
theorem ring_equiv.coe_mul_equiv_refl (R : Type u_4) [has_mul R] [has_add R] :
@[protected, instance]
def ring_equiv.inhabited (R : Type u_4) [has_mul R] [has_add R] :
Equations
@[protected, symm]
def ring_equiv.symm {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) :
S ≃+* R

The inverse of a ring isomorphism is a ring isomorphism.

Equations
def ring_equiv.simps.symm_apply {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) :
S R
Equations
@[simp]
theorem ring_equiv.inv_fun_eq_symm {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (f : R ≃+* S) :
@[simp]
theorem ring_equiv.symm_symm {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) :
e.symm.symm = e
@[simp]
theorem ring_equiv.coe_to_equiv_symm {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) :
theorem ring_equiv.symm_bijective {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] :
@[simp]
theorem ring_equiv.mk_coe' {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) (f : S R) (h₁ : f) (h₂ : f) (h₃ : (x y : S), f (x * y) = f x * f y) (h₄ : (x y : S), f (x + y) = f x + f y) :
{to_fun := f, inv_fun := e, left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄} = e.symm
@[simp]
theorem ring_equiv.symm_mk {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (f : R S) (g : S R) (h₁ : f) (h₂ : f) (h₃ : (x y : R), f (x * y) = f x * f y) (h₄ : (x y : R), f (x + y) = f x + f y) :
{to_fun := f, inv_fun := g, left_inv := h₁, right_inv := h₂, map_mul' := h₃, map_add' := h₄}.symm = {to_fun := g, inv_fun := f, left_inv := _, right_inv := _, map_mul' := _, map_add' := _}
@[protected, trans]
def ring_equiv.trans {R : Type u_4} {S : Type u_5} {S' : Type u_6} [has_mul R] [has_add R] [has_mul S] [has_add S] [has_mul S'] [has_add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
R ≃+* S'

Transitivity of `ring_equiv`.

Equations
theorem ring_equiv.trans_apply {R : Type u_4} {S : Type u_5} {S' : Type u_6} [has_mul R] [has_add R] [has_mul S] [has_add S] [has_mul S'] [has_add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') (a : R) :
(e₁.trans e₂) a = e₂ (e₁ a)
@[simp]
theorem ring_equiv.coe_trans {R : Type u_4} {S : Type u_5} {S' : Type u_6} [has_mul R] [has_add R] [has_mul S] [has_add S] [has_mul S'] [has_add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
(e₁.trans e₂) = e₂ e₁
@[simp]
theorem ring_equiv.symm_trans_apply {R : Type u_4} {S : Type u_5} {S' : Type u_6} [has_mul R] [has_add R] [has_mul S] [has_add S] [has_mul S'] [has_add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') (a : S') :
((e₁.trans e₂).symm) a = (e₁.symm) ((e₂.symm) a)
theorem ring_equiv.symm_trans {R : Type u_4} {S : Type u_5} {S' : Type u_6} [has_mul R] [has_add R] [has_mul S] [has_add S] [has_mul S'] [has_add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
(e₁.trans e₂).symm = e₂.symm.trans e₁.symm
@[protected]
theorem ring_equiv.bijective {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) :
@[protected]
theorem ring_equiv.injective {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) :
@[protected]
theorem ring_equiv.surjective {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) :
@[simp]
theorem ring_equiv.apply_symm_apply {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) (x : S) :
e ((e.symm) x) = x
@[simp]
theorem ring_equiv.symm_apply_apply {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) (x : R) :
(e.symm) (e x) = x
theorem ring_equiv.image_eq_preimage {R : Type u_4} {S : Type u_5} [has_mul R] [has_add R] [has_mul S] [has_add S] (e : R ≃+* S) (s : set R) :
e '' s = (e.symm) ⁻¹' s
@[simp]
theorem ring_equiv.coe_mul_equiv_trans {R : Type u_4} {S : Type u_5} {S' : Type u_6} [has_mul R] [has_add R] [has_mul S] [has_add S] [has_mul S'] [has_add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
(e₁.trans e₂) = e₁.trans e₂
@[simp]
theorem ring_equiv.coe_add_equiv_trans {R : Type u_4} {S : Type u_5} {S' : Type u_6} [has_mul R] [has_add R] [has_mul S] [has_add S] [has_mul S'] [has_add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
(e₁.trans e₂) = e₁.trans e₂
@[simp]
theorem ring_equiv.op_symm_apply_symm_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_mul α] [has_add β] [has_mul β] (f : αᵐᵒᵖ ≃+* βᵐᵒᵖ) (ᾰ : β) :
(((ring_equiv.op.symm) f).symm) =
@[simp]
theorem ring_equiv.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_mul α] [has_add β] [has_mul β] (f : αᵐᵒᵖ ≃+* βᵐᵒᵖ) (ᾰ : α) :
((ring_equiv.op.symm) f) =
@[simp]
theorem ring_equiv.op_apply_symm_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_mul α] [has_add β] [has_mul β] (f : α ≃+* β) (ᾰ : βᵐᵒᵖ) :
@[protected]
def ring_equiv.op {α : Type u_1} {β : Type u_2} [has_add α] [has_mul α] [has_add β] [has_mul β] :

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

Equations
@[simp]
theorem ring_equiv.op_apply_apply {α : Type u_1} {β : Type u_2} [has_add α] [has_mul α] [has_add β] [has_mul β] (f : α ≃+* β) (ᾰ : αᵐᵒᵖ) :
=
@[protected, simp]
def ring_equiv.unop {α : Type u_1} {β : Type u_2} [has_add α] [has_mul α] [has_add β] [has_mul β] :
≃+* β)

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

Equations

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

Equations
@[simp]
theorem ring_equiv.to_opposite_apply (R : Type u_4) (r : R) :
@[simp]
theorem ring_equiv.to_opposite_symm_apply (R : Type u_4) (r : Rᵐᵒᵖ) :
@[protected]
theorem ring_equiv.map_zero {R : Type u_4} {S : Type u_5} (f : R ≃+* S) :
f 0 = 0

A ring isomorphism sends zero to zero.

@[protected]
theorem ring_equiv.map_eq_zero_iff {R : Type u_4} {S : Type u_5} (f : R ≃+* S) {x : R} :
f x = 0 x = 0
theorem ring_equiv.map_ne_zero_iff {R : Type u_4} {S : Type u_5} (f : R ≃+* S) {x : R} :
f x 0 x 0
noncomputable def ring_equiv.of_bijective {F : Type u_1} {R : Type u_4} {S : Type u_5} [ S] (f : F) (hf : function.bijective f) :
R ≃+* S

Produce a ring isomorphism from a bijective ring homomorphism.

Equations
@[simp]
theorem ring_equiv.coe_of_bijective {F : Type u_1} {R : Type u_4} {S : Type u_5} [ S] (f : F) (hf : function.bijective f) :
hf) = f
theorem ring_equiv.of_bijective_apply {F : Type u_1} {R : Type u_4} {S : Type u_5} [ S] (f : F) (hf : function.bijective f) (x : R) :
hf) x = f x
@[simp]
theorem ring_equiv.Pi_congr_right_apply {ι : Type u_1} {R : ι Type u_2} {S : ι Type u_3} [Π (i : ι), ] [Π (i : ι), ] (e : Π (i : ι), R i ≃+* S i) (x : Π (i : ι), R i) (j : ι) :
j = (e j) (x j)
def ring_equiv.Pi_congr_right {ι : Type u_1} {R : ι Type u_2} {S : ι Type u_3} [Π (i : ι), ] [Π (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 `ring_equiv` version of `equiv.Pi_congr_right`, and the dependent version of `ring_equiv.arrow_congr`.

Equations
@[simp]
theorem ring_equiv.Pi_congr_right_refl {ι : Type u_1} {R : ι Type u_2} [Π (i : ι), ] :
ring_equiv.Pi_congr_right (λ (i : ι), ring_equiv.refl (R i)) = ring_equiv.refl (Π (i : ι), R i)
@[simp]
theorem ring_equiv.Pi_congr_right_symm {ι : Type u_1} {R : ι Type u_2} {S : ι Type u_3} [Π (i : ι), ] [Π (i : ι), ] (e : Π (i : ι), R i ≃+* S i) :
= ring_equiv.Pi_congr_right (λ (i : ι), (e i).symm)
@[simp]
theorem ring_equiv.Pi_congr_right_trans {ι : Type u_1} {R : ι Type u_2} {S : ι Type u_3} {T : ι Type u_4} [Π (i : ι), ] [Π (i : ι), ] [Π (i : ι), ] (e : Π (i : ι), R i ≃+* S i) (f : Π (i : ι), S i ≃+* T i) :
= ring_equiv.Pi_congr_right (λ (i : ι), (e i).trans (f i))
@[protected]
theorem ring_equiv.map_one {R : Type u_4} {S : Type u_5} (f : R ≃+* S) :
f 1 = 1

A ring isomorphism sends one to one.

@[protected]
theorem ring_equiv.map_eq_one_iff {R : Type u_4} {S : Type u_5} (f : R ≃+* S) {x : R} :
f x = 1 x = 1
theorem ring_equiv.map_ne_one_iff {R : Type u_4} {S : Type u_5} (f : R ≃+* S) {x : R} :
f x 1 x 1
@[simp]

`ring_equiv.coe_mul_equiv_refl` and `ring_equiv.coe_add_equiv_refl` are proved above in higher generality

@[simp]
@[simp]
theorem ring_equiv.coe_monoid_hom_trans {R : Type u_4} {S : Type u_5} {S' : Type u_6} (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
(e₁.trans e₂) = e₂.comp e₁
@[simp]
theorem ring_equiv.coe_add_monoid_hom_trans {R : Type u_4} {S : Type u_5} {S' : Type u_6} (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
(e₁.trans e₂) = e₂.comp e₁

`ring_equiv.coe_mul_equiv_trans` and `ring_equiv.coe_add_equiv_trans` are proved above in higher generality

@[simp]
theorem ring_equiv.coe_ring_hom_trans {R : Type u_4} {S : Type u_5} {S' : Type u_6} (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
(e₁.trans e₂) = e₂.comp e₁
@[simp]
theorem ring_equiv.comp_symm {R : Type u_4} {S : Type u_5} (e : R ≃+* S) :
@[simp]
theorem ring_equiv.symm_comp {R : Type u_4} {S : Type u_5} (e : R ≃+* S) :
@[protected]
theorem ring_equiv.map_neg {R : Type u_4} {S : Type u_5} (f : R ≃+* S) (x : R) :
f (-x) = -f x
@[protected]
theorem ring_equiv.map_sub {R : Type u_4} {S : Type u_5} (f : R ≃+* S) (x y : R) :
f (x - y) = f x - f y
@[simp]
theorem ring_equiv.map_neg_one {R : Type u_4} {S : Type u_5} (f : R ≃+* S) :
f (-1) = -1
theorem ring_equiv.map_eq_neg_one_iff {R : Type u_4} {S : Type u_5} (f : R ≃+* S) {x : R} :
f x = -1 x = -1
def ring_equiv.to_non_unital_ring_hom {R : Type u_4} {S : Type u_5} (e : R ≃+* S) :

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

Equations
@[protected, instance]
def ring_equiv.has_coe_to_non_unital_ring_hom {R : Type u_4} {S : Type u_5}  :
has_coe (R ≃+* S) (R →ₙ+* S)
Equations
theorem ring_equiv.to_non_unital_ring_hom_eq_coe {R : Type u_4} {S : Type u_5} (f : R ≃+* S) :
@[simp, norm_cast]
theorem ring_equiv.coe_to_non_unital_ring_hom {R : Type u_4} {S : Type u_5} (f : R ≃+* S) :
theorem ring_equiv.coe_non_unital_ring_hom_inj_iff {R : Type u_1} {S : Type u_2} (f g : R ≃+* S) :
f = g f = g
@[simp]
@[simp]
theorem ring_equiv.to_non_unital_ring_hom_trans {R : Type u_4} {S : Type u_5} {S' : Type u_6} (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
def ring_equiv.to_ring_hom {R : Type u_4} {S : Type u_5} (e : R ≃+* S) :
R →+* S

Reinterpret a ring equivalence as a ring homomorphism.

Equations
theorem ring_equiv.to_ring_hom_injective {R : Type u_4} {S : Type u_5}  :
@[protected, instance]
def ring_equiv.has_coe_to_ring_hom {R : Type u_4} {S : Type u_5}  :
has_coe (R ≃+* S) (R →+* S)
Equations
theorem ring_equiv.to_ring_hom_eq_coe {R : Type u_4} {S : Type u_5} (f : R ≃+* S) :
@[simp, norm_cast]
theorem ring_equiv.coe_to_ring_hom {R : Type u_4} {S : Type u_5} (f : R ≃+* S) :
theorem ring_equiv.coe_ring_hom_inj_iff {R : Type u_1} {S : Type u_2} (f g : R ≃+* S) :
f = g f = g
@[simp, norm_cast]
theorem ring_equiv.to_non_unital_ring_hom_commutes {R : Type u_4} {S : Type u_5} (f : R ≃+* S) :

The two paths coercion can take to a `non_unital_ring_hom` are equivalent

@[reducible]
def ring_equiv.to_monoid_hom {R : Type u_4} {S : Type u_5} (e : R ≃+* S) :
R →* S

Reinterpret a ring equivalence as a monoid homomorphism.

@[reducible]
def ring_equiv.to_add_monoid_hom {R : Type u_4} {S : Type u_5} (e : R ≃+* S) :
R →+ S

Reinterpret a ring equivalence as an `add_monoid` homomorphism.

theorem ring_equiv.to_add_monoid_hom_commutes {R : Type u_4} {S : Type u_5} (f : R ≃+* S) :

The two paths coercion can take to an `add_monoid_hom` are equivalent

theorem ring_equiv.to_monoid_hom_commutes {R : Type u_4} {S : Type u_5} (f : R ≃+* S) :

The two paths coercion can take to an `monoid_hom` are equivalent

theorem ring_equiv.to_equiv_commutes {R : Type u_4} {S : Type u_5} (f : R ≃+* S) :

The two paths coercion can take to an `equiv` are equivalent

@[simp]
theorem ring_equiv.to_ring_hom_refl {R : Type u_4}  :
@[simp]
theorem ring_equiv.to_monoid_hom_refl {R : Type u_4}  :
@[simp]
theorem ring_equiv.to_add_monoid_hom_refl {R : Type u_4}  :
@[simp]
theorem ring_equiv.to_ring_hom_apply_symm_to_ring_hom_apply {R : Type u_4} {S : Type u_5} (e : R ≃+* S) (y : S) :
@[simp]
theorem ring_equiv.symm_to_ring_hom_apply_to_ring_hom_apply {R : Type u_4} {S : Type u_5} (e : R ≃+* S) (x : R) :
@[simp]
theorem ring_equiv.to_ring_hom_trans {R : Type u_4} {S : Type u_5} {S' : Type u_6} (e₁ : R ≃+* S) (e₂ : S ≃+* S') :
@[simp]
theorem ring_equiv.to_ring_hom_comp_symm_to_ring_hom {R : Type u_4} {S : Type u_5} (e : R ≃+* S) :
@[simp]
theorem ring_equiv.symm_to_ring_hom_comp_to_ring_hom {R : Type u_4} {S : Type u_5} (e : R ≃+* S) :
def ring_equiv.of_hom_inv' {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [ S] [ R] (hom : F) (inv : G) (hom_inv_id : inv.comp hom = ) (inv_hom_id : hom.comp inv = ) :
R ≃+* S

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

Equations
@[simp]
theorem ring_equiv.of_hom_inv'_apply {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [ S] [ R] (hom : F) (inv : G) (hom_inv_id : inv.comp hom = ) (inv_hom_id : hom.comp inv = ) (a : R) :
inv hom_inv_id inv_hom_id) a = hom a
@[simp]
theorem ring_equiv.of_hom_inv'_symm_apply {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [ S] [ R] (hom : F) (inv : G) (hom_inv_id : inv.comp hom = ) (inv_hom_id : hom.comp inv = ) (a : S) :
inv hom_inv_id inv_hom_id).symm) a = inv a
@[simp]
theorem ring_equiv.of_hom_inv_symm_apply {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [ S] [ R] (hom : F) (inv : G) (hom_inv_id : inv.comp hom = ) (inv_hom_id : hom.comp inv = ) (a : S) :
inv hom_inv_id inv_hom_id).symm) a = inv a
def ring_equiv.of_hom_inv {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [ S] [ R] (hom : F) (inv : G) (hom_inv_id : inv.comp hom = ) (inv_hom_id : hom.comp inv = ) :
R ≃+* S

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

Equations
@[simp]
theorem ring_equiv.of_hom_inv_apply {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [ S] [ R] (hom : F) (inv : G) (hom_inv_id : inv.comp hom = ) (inv_hom_id : hom.comp inv = ) (a : R) :
inv hom_inv_id inv_hom_id) a = hom a
@[protected]
theorem ring_equiv.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
def mul_equiv.to_ring_equiv {R : Type u_1} {S : Type u_2} {F : Type u_3} [has_add R] [has_add S] [has_mul R] [has_mul S] [ S] (f : F) (H : (x y : R), f (x + y) = f x + f y) :
R ≃+* S

Gives a `ring_equiv` from an element of a `mul_equiv_class` preserving addition.

Equations
def add_equiv.to_ring_equiv {R : Type u_1} {S : Type u_2} {F : Type u_3} [has_add R] [has_add S] [has_mul R] [has_mul S] [ S] (f : F) (H : (x y : R), f (x * y) = f x * f y) :
R ≃+* S

Gives a `ring_equiv` from an element of an `add_equiv_class` preserving addition.

Equations
@[simp]
theorem ring_equiv.self_trans_symm {R : Type u_4} {S : Type u_5} [has_add R] [has_add S] [has_mul R] [has_mul S] (e : R ≃+* S) :
e.trans e.symm =
@[simp]
theorem ring_equiv.symm_trans_self {R : Type u_4} {S : Type u_5} [has_add R] [has_add S] [has_mul R] [has_mul S] (e : R ≃+* S) :
e.symm.trans e =
@[protected]
theorem ring_equiv.no_zero_divisors {A : Type u_1} (B : Type u_2) [ring A] [ring B] (e : A ≃+* B) :

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

@[protected]
theorem ring_equiv.is_domain {A : Type u_1} (B : Type u_2) [ring A] [ring B] [is_domain B] (e : A ≃+* B) :

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