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 #

infixl ` ≃+* `:25 := RingEquiv≃+* `:25 := RingEquiv

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

structure RingEquiv (R : Type u_1) (S : Type u_2) [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] extends Equiv :

Type (maxu_1u_2)

The proposition that the function preserves multiplication
map_mul' : ∀ (x y : R), Equiv.toFun toEquiv (x * y) = Equiv.toFun toEquiv x * Equiv.toFun toEquiv y
The proposition that the function preserves addition
map_add' : ∀ (x y : R), Equiv.toFun toEquiv (x + y) = Equiv.toFun toEquiv x + Equiv.toFun toEquiv y

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

Instances For

def «term_≃+*_» :

Lean.TrailingParserDescr

Notation for RingEquiv.

Equations

«term_≃+*_» = Lean.ParserDescr.trailingNode `term_≃+*_ 25 25 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ≃+* ") (Lean.ParserDescr.cat `term 26))

abbrev RingEquiv.toAddEquiv {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (self : R ≃+* S) :

R ≃+ S

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

Equations

RingEquiv.toAddEquiv self = { toEquiv := self.toEquiv, map_add' := (_ : ∀ (x y : R), Equiv.toFun self.toEquiv (x + y) = Equiv.toFun self.toEquiv x + Equiv.toFun self.toEquiv y) }

abbrev RingEquiv.toMulEquiv {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (self : R ≃+* S) :

R ≃* S

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

Equations

RingEquiv.toMulEquiv self = { toEquiv := self.toEquiv, map_mul' := (_ : ∀ (x y : R), Equiv.toFun self.toEquiv (x * y) = Equiv.toFun self.toEquiv x * Equiv.toFun self.toEquiv y) }

class RingEquivClass (F : Type u_1) (R : outParam (Type u_2)) (S : outParam (Type u_3)) [inst : Mul R] [inst : Add R] [inst : Mul S] [inst : Add S] extends MulEquivClass :

Type (max(maxu_1u_2)u_3)

By definition, a ring isomorphism preserves the additive structure.
map_add : ∀ (f : F) (a b : R), ↑f (a + b) = ↑f a + ↑f b

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

Instances

instance RingEquivClass.toAddEquivClass {F : Type u_1} {R : Type u_2} {S : Type u_3} :

{x : Mul R} → {x_1 : Add R} → {x_2 : Mul S} → {x_3 : Add S} → [h : RingEquivClass F R S] → AddEquivClass F R S

Equations

RingEquivClass.toAddEquivClass = AddEquivClass.mk (_ : ∀ (f : F) (a b : R), ↑f (a + b) = ↑f a + ↑f b)

instance RingEquivClass.toRingHomClass {F : Type u_1} {R : Type u_2} {S : Type u_3} :

{x : NonAssocSemiring R} → {x_1 : NonAssocSemiring S} → [h : RingEquivClass F R S] → RingHomClass F R S

Equations

RingEquivClass.toRingHomClass = RingHomClass.mk (_ : ∀ (f : F) (a b : R), ↑f (a + b) = ↑f a + ↑f b) (_ : ∀ (f : F), ↑f 0 = 0)

instance RingEquivClass.toNonUnitalRingHomClass {F : Type u_1} {R : Type u_2} {S : Type u_3} :

{x : NonUnitalNonAssocSemiring R} → {x_1 : NonUnitalNonAssocSemiring S} → [h : RingEquivClass F R S] → NonUnitalRingHomClass F R S

Equations

RingEquivClass.toNonUnitalRingHomClass = NonUnitalRingHomClass.mk (_ : ∀ (f : F) (a b : R), ↑f (a + b) = ↑f a + ↑f b) (_ : ∀ (f : F), ↑f 0 = 0)

def RingEquivClass.toRingEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst : Add α] [inst : Mul β] [inst : Add β] [inst : 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

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

instance instCoeTCRingEquiv {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst : Add α] [inst : Mul β] [inst : Add β] [inst : RingEquivClass F α β] :

CoeTC F (α ≃+* β)

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

Equations

instCoeTCRingEquiv = { coe := RingEquivClass.toRingEquiv }

instance RingEquiv.instRingEquivClassRingEquiv {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] :

RingEquivClass (R ≃+* S) R S

Equations

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

@[simp]

theorem RingEquiv.toEquiv_eq_coe {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (f : R ≃+* S) :

f.toEquiv = ↑f

@[simp]

theorem RingEquiv.coe_toEquiv {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (f : R ≃+* S) :

↑↑f = ↑f

theorem RingEquiv.map_mul {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : 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_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : 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_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : 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_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (e : R ≃ S) (h₃ : ∀ (x y : R), Equiv.toFun e (x * y) = Equiv.toFun e x * Equiv.toFun e y) (h₄ : ∀ (x y : R), Equiv.toFun e (x + y) = Equiv.toFun e x + Equiv.toFun e y) :

↑{ toEquiv := e, map_mul' := h₃, map_add' := h₄ } = ↑e

@[simp]

theorem RingEquiv.mk_coe {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (e : R ≃+* S) (e' : S → R) (h₁ : Function.LeftInverse e' ↑e) (h₂ : Function.RightInverse e' ↑e) (h₃ : ∀ (x y : R), Equiv.toFun { toFun := ↑e, invFun := e', left_inv := h₁, right_inv := h₂ } (x * y) = Equiv.toFun { toFun := ↑e, invFun := e', left_inv := h₁, right_inv := h₂ } x * Equiv.toFun { toFun := ↑e, invFun := e', left_inv := h₁, right_inv := h₂ } y) (h₄ : ∀ (x y : R), Equiv.toFun { toFun := ↑e, invFun := e', left_inv := h₁, right_inv := h₂ } (x + y) = Equiv.toFun { toFun := ↑e, invFun := e', left_inv := h₁, right_inv := h₂ } x + Equiv.toFun { toFun := ↑e, invFun := e', left_inv := h₁, right_inv := h₂ } 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_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] {f : R ≃+* S} {x : R} {x' : R} :

x = x' → ↑f x = ↑f x'

theorem RingEquiv.congr_fun {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] {f : R ≃+* S} {g : R ≃+* S} (h : f = g) (x : R) :

↑f x = ↑g x

theorem RingEquiv.ext_iff {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : 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_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (f : R ≃+* S) :

RingEquiv.toAddEquiv f = ↑f

@[simp]

theorem RingEquiv.toMulEquiv_eq_coe {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (f : R ≃+* S) :

RingEquiv.toMulEquiv f = ↑f

@[simp]

theorem RingEquiv.coe_toMulEquiv {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (f : R ≃+* S) :

↑↑f = ↑f

@[simp]

theorem RingEquiv.coe_toAddEquiv {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (f : R ≃+* S) :

↑↑f = ↑f

def RingEquiv.ringEquivOfUnique {M : Type u_1} {N : Type u_2} [inst : Unique M] [inst : Unique N] [inst : Add M] [inst : Mul M] [inst : Add N] [inst : Mul N] :

The RingEquiv between two semirings with a unique element.

Equations

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

instance RingEquiv.instUniqueRingEquiv {M : Type u_1} {N : Type u_2} [inst : Unique M] [inst : Unique N] [inst : Add M] [inst : Mul M] [inst : Add N] [inst : Mul N] :

Unique (M ≃+* N)

Equations

RingEquiv.instUniqueRingEquiv = { toInhabited := { default := RingEquiv.ringEquivOfUnique }, uniq := (_ : ∀ (x : M ≃+* N), x = default) }

def RingEquiv.refl (R : Type u_1) [inst : Mul R] [inst : Add R] :

The identity map is a ring isomorphism.

Equations

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

@[simp]

theorem RingEquiv.refl_apply (R : Type u_1) [inst : Mul R] [inst : Add R] (x : R) :

↑(RingEquiv.refl R) x = x

@[simp]

theorem RingEquiv.coe_addEquiv_refl (R : Type u_1) [inst : Mul R] [inst : Add R] :

↑(RingEquiv.refl R) = AddEquiv.refl R

@[simp]

theorem RingEquiv.coe_mulEquiv_refl (R : Type u_1) [inst : Mul R] [inst : Add R] :

↑(RingEquiv.refl R) = MulEquiv.refl R

instance RingEquiv.instInhabitedRingEquiv (R : Type u_1) [inst : Mul R] [inst : Add R] :

Inhabited (R ≃+* R)

Equations

RingEquiv.instInhabitedRingEquiv R = { default := RingEquiv.refl R }

def RingEquiv.symm {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (e : R ≃+* S) :

The inverse of a ring isomorphism is a ring isomorphism.

Equations

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

def RingEquiv.Simps.symm_apply {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (e : R ≃+* S) :

S → R

See Note [custom simps projection]

Equations

RingEquiv.Simps.symm_apply e = ↑(RingEquiv.symm e)

@[simp]

theorem RingEquiv.invFun_eq_symm {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (f : R ≃+* S) :

EquivLike.inv f = ↑(RingEquiv.symm f)

@[simp]

theorem RingEquiv.symm_symm {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (e : R ≃+* S) :

RingEquiv.symm (RingEquiv.symm e) = e

@[simp]

theorem RingEquiv.symm_refl {R : Type u_1} [inst : Mul R] [inst : Add R] :

RingEquiv.symm (RingEquiv.refl R) = RingEquiv.refl R

@[simp]

theorem RingEquiv.coe_toEquiv_symm {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (e : R ≃+* S) :

↑(RingEquiv.symm e) = Equiv.symm ↑e

theorem RingEquiv.symm_bijective {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] :

Function.Bijective RingEquiv.symm

@[simp]

theorem RingEquiv.mk_coe' {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (e : R ≃+* S) (f : S → R) (h₁ : Function.LeftInverse (↑e) f) (h₂ : Function.RightInverse (↑e) f) (h₃ : ∀ (x y : S), Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } (x * y) = Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } x * Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } y) (h₄ : ∀ (x y : S), Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } (x + y) = Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } x + Equiv.toFun { toFun := f, invFun := ↑e, left_inv := h₁, right_inv := h₂ } 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_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (f : R → S) (g : S → R) (h₁ : Function.LeftInverse g f) (h₂ : Function.RightInverse g f) (h₃ : ∀ (x y : R), Equiv.toFun { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂ } (x * y) = Equiv.toFun { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂ } x * Equiv.toFun { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂ } y) (h₄ : ∀ (x y : R), Equiv.toFun { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂ } (x + y) = Equiv.toFun { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂ } x + Equiv.toFun { toFun := f, invFun := g, left_inv := h₁, right_inv := h₂ } 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 := (_ : Function.LeftInverse src.toEquiv.invFun src.toEquiv.toFun), right_inv := (_ : Function.RightInverse src.toEquiv.invFun src.toEquiv.toFun) }, map_mul' := (_ : ∀ (x y : S), Equiv.toFun src.toEquiv (x * y) = Equiv.toFun src.toEquiv x * Equiv.toFun src.toEquiv y), map_add' := (_ : ∀ (x y : S), Equiv.toFun src.toEquiv (x + y) = Equiv.toFun src.toEquiv x + Equiv.toFun src.toEquiv y) }

def RingEquiv.trans {R : Type u_1} {S : Type u_2} {S' : Type u_3} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] [inst : Mul S'] [inst : 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.

theorem RingEquiv.trans_apply {R : Type u_1} {S : Type u_2} {S' : Type u_3} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] [inst : Mul S'] [inst : 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_1} {S : Type u_2} {S' : Type u_3} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] [inst : Mul S'] [inst : Add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :

↑(RingEquiv.trans e₁ e₂) = ↑e₂ ∘ ↑e₁

@[simp]

theorem RingEquiv.symm_trans_apply {R : Type u_1} {S : Type u_2} {S' : Type u_3} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] [inst : Mul S'] [inst : Add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') (a : S') :

↑(RingEquiv.symm (RingEquiv.trans e₁ e₂)) a = ↑(RingEquiv.symm e₁) (↑(RingEquiv.symm e₂) a)

theorem RingEquiv.symm_trans {R : Type u_1} {S : Type u_2} {S' : Type u_3} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] [inst : Mul S'] [inst : Add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :

RingEquiv.symm (RingEquiv.trans e₁ e₂) = RingEquiv.trans (RingEquiv.symm e₂) (RingEquiv.symm e₁)

theorem RingEquiv.bijective {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (e : R ≃+* S) :

Function.Bijective ↑e

theorem RingEquiv.injective {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (e : R ≃+* S) :

Function.Injective ↑e

theorem RingEquiv.surjective {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (e : R ≃+* S) :

Function.Surjective ↑e

@[simp]

theorem RingEquiv.apply_symm_apply {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (e : R ≃+* S) (x : S) :

↑e (↑(RingEquiv.symm e) x) = x

@[simp]

theorem RingEquiv.symm_apply_apply {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (e : R ≃+* S) (x : R) :

↑(RingEquiv.symm e) (↑e x) = x

theorem RingEquiv.image_eq_preimage {R : Type u_1} {S : Type u_2} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] (e : R ≃+* S) (s : Set R) :

↑e '' s = ↑(RingEquiv.symm e) ⁻¹' s

@[simp]

theorem RingEquiv.coe_mulEquiv_trans {R : Type u_1} {S : Type u_2} {S' : Type u_3} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] [inst : Mul S'] [inst : 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_1} {S : Type u_2} {S' : Type u_3} [inst : Mul R] [inst : Mul S] [inst : Add R] [inst : Add S] [inst : Mul S'] [inst : Add S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :

↑(RingEquiv.trans e₁ e₂) = AddEquiv.trans ↑e₁ ↑e₂

@[simp]

theorem RingEquiv.op_apply_symm_apply_unop {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Mul α] [inst : Add β] [inst : Mul β] (f : α ≃+* β) :

∀ (a : βᵐᵒᵖ), (↑(RingEquiv.symm (↑RingEquiv.op f)) a).unop = ↑(AddEquiv.symm ↑f) a.unop

@[simp]

theorem RingEquiv.op_apply_apply_unop {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Mul α] [inst : Add β] [inst : Mul β] (f : α ≃+* β) :

∀ (a : αᵐᵒᵖ), (↑(↑RingEquiv.op f) a).unop = ↑f a.unop

@[simp]

theorem RingEquiv.op_symm_apply_apply {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Mul α] [inst : Add β] [inst : Mul β] (f : αᵐᵒᵖ ≃+* βᵐᵒᵖ) :

∀ (a : α), ↑(↑(Equiv.symm RingEquiv.op) f) a = (↑f { unop := a }).unop

@[simp]

theorem RingEquiv.op_symm_apply_symm_apply {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Mul α] [inst : Add β] [inst : Mul β] (f : αᵐᵒᵖ ≃+* βᵐᵒᵖ) :

∀ (a : β), ↑(RingEquiv.symm (↑(Equiv.symm RingEquiv.op) f)) a = (↑(AddEquiv.symm ↑f) { unop := a }).unop

def RingEquiv.op {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Mul α] [inst : Add β] [inst : 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.

def RingEquiv.unop {α : Type u_1} {β : Type u_2} [inst : Add α] [inst : Mul α] [inst : Add β] [inst : Mul β] :

αᵐᵒᵖ ≃+* βᵐᵒᵖ ≃ (α ≃+* β)

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

Equations

RingEquiv.unop = Equiv.symm RingEquiv.op

def RingEquiv.toOpposite (R : Type u_1) [inst : NonUnitalCommSemiring R] :

R ≃+* Rᵐᵒᵖ

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

Equations

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

@[simp]

theorem RingEquiv.toOpposite_apply (R : Type u_1) [inst : NonUnitalCommSemiring R] (r : R) :

↑(RingEquiv.toOpposite R) r = { unop := r }

@[simp]

theorem RingEquiv.toOpposite_symm_apply (R : Type u_1) [inst : NonUnitalCommSemiring R] (r : Rᵐᵒᵖ) :

↑(RingEquiv.symm (RingEquiv.toOpposite R)) r = r.unop

theorem RingEquiv.map_zero {R : Type u_2} {S : Type u_1} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] (f : R ≃+* S) :

↑f 0 = 0

A ring isomorphism sends zero to zero.

theorem RingEquiv.map_eq_zero_iff {R : Type u_2} {S : Type u_1} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] (f : R ≃+* S) {x : R} :

↑f x = 0 ↔ x = 0

theorem RingEquiv.map_ne_zero_iff {R : Type u_2} {S : Type u_1} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] (f : R ≃+* S) {x : R} :

↑f x ≠ 0 ↔ x ≠ 0

noncomputable def RingEquiv.ofBijective {F : Type u_1} {R : Type u_2} {S : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] [inst : NonUnitalRingHomClass F R S] (f : F) (hf : Function.Bijective ↑f) :

Produce a ring isomorphism from a bijective ring homomorphism.

Equations

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

@[simp]

theorem RingEquiv.coe_ofBijective {F : Type u_1} {R : Type u_2} {S : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] [inst : 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_2} {S : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] [inst : NonUnitalRingHomClass F R S] (f : F) (hf : Function.Bijective ↑f) (x : R) :

↑(RingEquiv.ofBijective f hf) x = ↑f x

@[simp]

theorem RingEquiv.piCongrRight_apply {ι : Type u_1} {R : ι → Type u_2} {S : ι → Type u_3} [inst : (i : ι) → NonUnitalNonAssocSemiring (R i)] [inst : (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_1} {R : ι → Type u_2} {S : ι → Type u_3} [inst : (i : ι) → NonUnitalNonAssocSemiring (R i)] [inst : (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)∀ j, (R j ≃+* S j)≃+* S j) generates a ring isomorphisms between ∀ j, R j∀ j, R j and ∀ j, S j∀ 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.

@[simp]

theorem RingEquiv.piCongrRight_refl {ι : Type u_1} {R : ι → Type u_2} [inst : (i : ι) → NonUnitalNonAssocSemiring (R i)] :

(RingEquiv.piCongrRight fun i => RingEquiv.refl (R i)) = RingEquiv.refl ((i : ι) → R i)

@[simp]

theorem RingEquiv.piCongrRight_symm {ι : Type u_1} {R : ι → Type u_2} {S : ι → Type u_3} [inst : (i : ι) → NonUnitalNonAssocSemiring (R i)] [inst : (i : ι) → NonUnitalNonAssocSemiring (S i)] (e : (i : ι) → R i ≃+* S i) :

RingEquiv.symm (RingEquiv.piCongrRight e) = RingEquiv.piCongrRight fun i => RingEquiv.symm (e i)

@[simp]

theorem RingEquiv.piCongrRight_trans {ι : Type u_1} {R : ι → Type u_2} {S : ι → Type u_3} {T : ι → Type u_4} [inst : (i : ι) → NonUnitalNonAssocSemiring (R i)] [inst : (i : ι) → NonUnitalNonAssocSemiring (S i)] [inst : (i : ι) → NonUnitalNonAssocSemiring (T i)] (e : (i : ι) → R i ≃+* S i) (f : (i : ι) → S i ≃+* T i) :

RingEquiv.trans (RingEquiv.piCongrRight e) (RingEquiv.piCongrRight f) = RingEquiv.piCongrRight fun i => RingEquiv.trans (e i) (f i)

theorem RingEquiv.map_one {R : Type u_2} {S : Type u_1} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R ≃+* S) :

↑f 1 = 1

A ring isomorphism sends one to one.

theorem RingEquiv.map_eq_one_iff {R : Type u_2} {S : Type u_1} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R ≃+* S) {x : R} :

↑f x = 1 ↔ x = 1

theorem RingEquiv.map_ne_one_iff {R : Type u_2} {S : Type u_1} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R ≃+* S) {x : R} :

↑f x ≠ 1 ↔ x ≠ 1

theorem RingEquiv.coe_monoidHom_refl {R : Type u_1} [inst : NonAssocSemiring R] :

↑(RingEquiv.refl R) = MonoidHom.id R

@[simp]

theorem RingEquiv.coe_addMonoidHom_refl {R : Type u_1} [inst : NonAssocSemiring R] :

↑(RingEquiv.refl R) = AddMonoidHom.id R

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

@[simp]

theorem RingEquiv.coe_ringHom_refl {R : Type u_1} [inst : NonAssocSemiring R] :

↑(RingEquiv.refl R) = RingHom.id R

@[simp]

theorem RingEquiv.coe_monoidHom_trans {R : Type u_2} {S : Type u_3} {S' : Type u_1} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : 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_2} {S : Type u_3} {S' : Type u_1} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : 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_2} {S : Type u_3} {S' : Type u_1} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : NonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :

↑(RingEquiv.trans e₁ e₂) = RingHom.comp ↑e₂ ↑e₁

@[simp]

theorem RingEquiv.comp_symm {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (e : R ≃+* S) :

RingHom.comp ↑e ↑(RingEquiv.symm e) = RingHom.id S

@[simp]

theorem RingEquiv.symm_comp {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (e : R ≃+* S) :

RingHom.comp ↑(RingEquiv.symm e) ↑e = RingHom.id R

theorem RingEquiv.map_neg {R : Type u_2} {S : Type u_1} [inst : NonUnitalNonAssocRing R] [inst : NonUnitalNonAssocRing S] (f : R ≃+* S) (x : R) :

↑f (-x) = -↑f x

theorem RingEquiv.map_sub {R : Type u_2} {S : Type u_1} [inst : NonUnitalNonAssocRing R] [inst : NonUnitalNonAssocRing S] (f : R ≃+* S) (x : R) (y : R) :

↑f (x - y) = ↑f x - ↑f y

theorem RingEquiv.map_neg_one {R : Type u_2} {S : Type u_1} [inst : NonAssocRing R] [inst : NonAssocRing S] (f : R ≃+* S) :

↑f (-1) = -1

def RingEquiv.toNonUnitalRingHom {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] (e : R ≃+* S) :

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

Equations

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

theorem RingEquiv.toNonUnitalRingHom_injective {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] :

Function.Injective RingEquiv.toNonUnitalRingHom

instance RingEquiv.instCoeToNonUnitalRingHom {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] :

Coe (R ≃+* S) (R →ₙ+* S)

Equations

RingEquiv.instCoeToNonUnitalRingHom = { coe := RingEquiv.toNonUnitalRingHom }

theorem RingEquiv.toNonUnitalRingHom_eq_coe {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] (f : R ≃+* S) :

RingEquiv.toNonUnitalRingHom f = ↑f

@[simp]

theorem RingEquiv.coe_toNonUnitalRingHom {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] (f : R ≃+* S) :

↑↑f = ↑f

theorem RingEquiv.coe_nonUnitalRingHom_inj_iff {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] (f : R ≃+* S) (g : R ≃+* S) :

f = g ↔ ↑f = ↑g

@[simp]

theorem RingEquiv.toNonUnitalRingHom_refl {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] :

RingEquiv.toNonUnitalRingHom (RingEquiv.refl R) = NonUnitalRingHom.id R

@[simp]

theorem RingEquiv.toNonUnitalRingHom_apply_symm_toNonUnitalRingHom_apply {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] (e : R ≃+* S) (y : S) :

↑(RingEquiv.toNonUnitalRingHom e) (↑(RingEquiv.toNonUnitalRingHom (RingEquiv.symm e)) y) = y

@[simp]

theorem RingEquiv.symm_toNonUnitalRingHom_apply_toNonUnitalRingHom_apply {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] (e : R ≃+* S) (x : R) :

↑(RingEquiv.toNonUnitalRingHom (RingEquiv.symm e)) (↑(RingEquiv.toNonUnitalRingHom e) x) = x

@[simp]

theorem RingEquiv.toNonUnitalRingHom_trans {R : Type u_1} {S : Type u_2} {S' : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] [inst : NonUnitalNonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :

RingEquiv.toNonUnitalRingHom (RingEquiv.trans e₁ e₂) = NonUnitalRingHom.comp (RingEquiv.toNonUnitalRingHom e₂) (RingEquiv.toNonUnitalRingHom e₁)

@[simp]

theorem RingEquiv.toNonUnitalRingHomm_comp_symm_toNonUnitalRingHom {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] (e : R ≃+* S) :

NonUnitalRingHom.comp (RingEquiv.toNonUnitalRingHom e) (RingEquiv.toNonUnitalRingHom (RingEquiv.symm e)) = NonUnitalRingHom.id S

@[simp]

theorem RingEquiv.symm_toNonUnitalRingHom_comp_toNonUnitalRingHom {R : Type u_1} {S : Type u_2} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] (e : R ≃+* S) :

NonUnitalRingHom.comp (RingEquiv.toNonUnitalRingHom (RingEquiv.symm e)) (RingEquiv.toNonUnitalRingHom e) = NonUnitalRingHom.id R

def RingEquiv.toRingHom {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (e : R ≃+* S) :

Reinterpret a ring equivalence as a ring homomorphism.

Equations

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

theorem RingEquiv.toRingHom_injective {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] :

Function.Injective RingEquiv.toRingHom

instance RingEquiv.instCoeToRingHom {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] :

Coe (R ≃+* S) (R →+* S)

Equations

RingEquiv.instCoeToRingHom = { coe := RingEquiv.toRingHom }

theorem RingEquiv.toRingHom_eq_coe {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R ≃+* S) :

RingEquiv.toRingHom f = ↑f

@[simp]

theorem RingEquiv.coe_toRingHom {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R ≃+* S) :

↑↑f = ↑f

theorem RingEquiv.coe_ringHom_inj_iff {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R ≃+* S) (g : R ≃+* S) :

f = g ↔ ↑f = ↑g

@[simp]

theorem RingEquiv.toNonUnitalRingHom_commutes {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R ≃+* S) :

↑↑f = ↑f

The two paths coercion can take to a NonUnitalRingEquiv are equivalent

@[inline]

abbrev RingEquiv.toMonoidHom {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (e : R ≃+* S) :

R →* S

Reinterpret a ring equivalence as a monoid homomorphism.

Equations

RingEquiv.toMonoidHom e = ↑(RingEquiv.toRingHom e)

@[inline]

abbrev RingEquiv.toAddMonoidHom {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (e : R ≃+* S) :

R →+ S

Reinterpret a ring equivalence as an AddMonoid homomorphism.

Equations

RingEquiv.toAddMonoidHom e = RingHom.toAddMonoidHom (RingEquiv.toRingHom e)

theorem RingEquiv.toAddMonoidMom_commutes {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R ≃+* S) :

RingHom.toAddMonoidHom ↑f = AddEquiv.toAddMonoidHom ↑f

The two paths coercion can take to an AddMonoidHom are equivalent

theorem RingEquiv.toMonoidHom_commutes {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R ≃+* S) :

↑↑f = MulEquiv.toMonoidHom ↑f

The two paths coercion can take to an MonoidHom are equivalent

theorem RingEquiv.toEquiv_commutes {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (f : R ≃+* S) :

(↑f).toEquiv = (↑f).toEquiv

The two paths coercion can take to an Equiv are equivalent

@[simp]

theorem RingEquiv.toRingHom_refl {R : Type u_1} [inst : NonAssocSemiring R] :

RingEquiv.toRingHom (RingEquiv.refl R) = RingHom.id R

@[simp]

theorem RingEquiv.toMonoidHom_refl {R : Type u_1} [inst : NonAssocSemiring R] :

RingEquiv.toMonoidHom (RingEquiv.refl R) = MonoidHom.id R

@[simp]

theorem RingEquiv.toAddMonoidHom_refl {R : Type u_1} [inst : NonAssocSemiring R] :

RingEquiv.toAddMonoidHom (RingEquiv.refl R) = AddMonoidHom.id R

@[simp]

theorem RingEquiv.toRingHom_apply_symm_toRingHom_apply {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (e : R ≃+* S) (y : S) :

↑(RingEquiv.toRingHom e) (↑(RingEquiv.toRingHom (RingEquiv.symm e)) y) = y

@[simp]

theorem RingEquiv.symm_toRingHom_apply_toRingHom_apply {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (e : R ≃+* S) (x : R) :

↑(RingEquiv.toRingHom (RingEquiv.symm e)) (↑(RingEquiv.toRingHom e) x) = x

@[simp]

theorem RingEquiv.toRingHom_trans {R : Type u_1} {S : Type u_2} {S' : Type u_3} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : NonAssocSemiring S'] (e₁ : R ≃+* S) (e₂ : S ≃+* S') :

RingEquiv.toRingHom (RingEquiv.trans e₁ e₂) = RingHom.comp (RingEquiv.toRingHom e₂) (RingEquiv.toRingHom e₁)

@[simp]

theorem RingEquiv.toRingHom_comp_symm_toRingHom {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (e : R ≃+* S) :

RingHom.comp (RingEquiv.toRingHom e) (RingEquiv.toRingHom (RingEquiv.symm e)) = RingHom.id S

@[simp]

theorem RingEquiv.symm_toRingHom_comp_toRingHom {R : Type u_1} {S : Type u_2} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] (e : R ≃+* S) :

RingHom.comp (RingEquiv.toRingHom (RingEquiv.symm e)) (RingEquiv.toRingHom e) = RingHom.id R

@[simp]

theorem RingEquiv.ofHomInv'_symm_apply {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] [inst : NonUnitalRingHomClass F R S] [inst : 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_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] [inst : NonUnitalRingHomClass F R S] [inst : 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_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NonUnitalNonAssocSemiring R] [inst : NonUnitalNonAssocSemiring S] [inst : NonUnitalRingHomClass F R S] [inst : 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) :

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

Equations

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

@[simp]

theorem RingEquiv.ofHomInv_symm_apply {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : RingHomClass F R S] [inst : 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

@[simp]

theorem RingEquiv.ofHomInv_apply {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : RingHomClass F R S] [inst : 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

def RingEquiv.ofHomInv {R : Type u_1} {S : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NonAssocSemiring R] [inst : NonAssocSemiring S] [inst : RingHomClass F R S] [inst : 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) :

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

Equations

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

theorem RingEquiv.map_pow {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst : Semiring S] (f : R ≃+* S) (a : R) (n : ℕ) :

↑f (a ^ n) = ↑f a ^ n

def MulEquiv.toRingEquiv {R : Type u_1} {S : Type u_2} {F : Type u_3} [inst : Add R] [inst : Add S] [inst : Mul R] [inst : Mul S] [inst : MulEquivClass F R S] (f : F) (H : ∀ (x y : R), ↑f (x + y) = ↑f x + ↑f y) :

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

Equations

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

def AddEquiv.toRingEquiv {R : Type u_1} {S : Type u_2} {F : Type u_3} [inst : Add R] [inst : Add S] [inst : Mul R] [inst : Mul S] [inst : AddEquivClass F R S] (f : F) (H : ∀ (x y : R), ↑f (x * y) = ↑f x * ↑f y) :

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

Equations

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

@[simp]

theorem RingEquiv.self_trans_symm {R : Type u_1} {S : Type u_2} [inst : Add R] [inst : Add S] [inst : Mul R] [inst : Mul S] (e : R ≃+* S) :

RingEquiv.trans e (RingEquiv.symm e) = RingEquiv.refl R

@[simp]

theorem RingEquiv.symm_trans_self {R : Type u_1} {S : Type u_2} [inst : Add R] [inst : Add S] [inst : Mul R] [inst : Mul S] (e : R ≃+* S) :

RingEquiv.trans (RingEquiv.symm e) e = RingEquiv.refl S

theorem RingEquiv.noZeroDivisors {A : Type u_1} (B : Type u_2) [inst : Ring A] [inst : Ring B] [inst : 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.

theorem RingEquiv.isDomain {A : Type u_1} (B : Type u_2) [inst : Ring A] [inst : Ring B] [inst : IsDomain B] (e : A ≃+* B) :

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