# Documentation

Mathlib.Algebra.Hom.Ring.Defs

# Homomorphisms of semirings and rings #

This file defines bundled homomorphisms of (non-unital) semirings and rings. As with monoid and groups, we use the same structure RingHom a β, a.k.a. α →+* β, for both types of homomorphisms.

## Main definitions #

• NonUnitalRingHom: Non-unital (semi)ring homomorphisms. Additive monoid homomorphism which preserve multiplication.
• RingHom: (Semi)ring homomorphisms. Monoid homomorphisms which are also additive monoid homomorphism.

## Notations #

• →ₙ+*: Non-unital (semi)ring homs
• →+*: (Semi)ring homs

## Implementation notes #

• There's a coercion from bundled homs to fun, and the canonical notation is to use the bundled hom as a function via this coercion.

• There is no SemiringHom -- the idea is that RingHom is used. The constructor for a RingHom between semirings needs a proof of map_zero, map_one and map_add as well as map_mul; a separate constructor RingHom.mk' will construct ring homs between rings from monoid homs given only a proof that addition is preserved.

## Tags #

RingHom, SemiringHom

structure NonUnitalRingHom (α : Type u_5) (β : Type u_6) extends :
Type (max u_5 u_6)

Bundled non-unital semiring homomorphisms α →ₙ+* β; use this for bundled non-unital ring homomorphisms too.

When possible, instead of parametrizing results over (f : α →ₙ+* β), you should parametrize over (F : Type*) [NonUnitalRingHomClass F α β] (f : F).

When you extend this structure, make sure to extend NonUnitalRingHomClass.

Instances For

α →ₙ+* β denotes the type of non-unital ring homomorphisms from α to β.

Instances For
@[reducible]
abbrev NonUnitalRingHom.toAddMonoidHom {α : Type u_5} {β : Type u_6} (self : α →ₙ+* β) :
α →+ β

Reinterpret a non-unital ring homomorphism f : α →ₙ+* β as an additive monoid homomorphism α →+ β. The simp-normal form is (f : α →+ β).

Instances For
class NonUnitalRingHomClass (F : Type u_5) (α : outParam (Type u_6)) (β : outParam (Type u_7)) extends :
Type (max (max u_5 u_6) u_7)
• coe : Fαβ
• coe_injective' : Function.Injective FunLike.coe
• map_mul : ∀ (f : F) (x y : α), f (x * y) = f x * f y
• map_add : ∀ (f : F) (x y : α), f (x + y) = f x + f y

The proposition that the function preserves addition

• map_zero : ∀ (f : F), f 0 = 0

The proposition that the function preserves 0

NonUnitalRingHomClass F α β states that F is a type of non-unital (semi)ring homomorphisms. You should extend this class when you extend NonUnitalRingHom.

Instances
def NonUnitalRingHomClass.toNonUnitalRingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [] (f : F) :
α →ₙ+* β

Turn an element of a type F satisfying NonUnitalRingHomClass F α β into an actual NonUnitalRingHom. This is declared as the default coercion from F to α →ₙ+* β.

Instances For
instance instCoeTCNonUnitalRingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [] :
CoeTC F (α →ₙ+* β)

Any type satisfying NonUnitalRingHomClass can be cast into NonUnitalRingHom via NonUnitalRingHomClass.toNonUnitalRingHom.

@[simp]
theorem NonUnitalRingHom.coe_toMulHom {α : Type u_2} {β : Type u_3} (f : α →ₙ+* β) :
f.toMulHom = f
@[simp]
theorem NonUnitalRingHom.coe_mulHom_mk {α : Type u_2} {β : Type u_3} (f : αβ) (h₁ : ∀ (x y : α), f (x * y) = f x * f y) (h₂ : MulHom.toFun { toFun := f, map_mul' := h₁ } 0 = 0) (h₃ : ∀ (x y : α), MulHom.toFun { toFun := f, map_mul' := h₁ } (x + y) = MulHom.toFun { toFun := f, map_mul' := h₁ } x + MulHom.toFun { toFun := f, map_mul' := h₁ } y) :
{ toMulHom := { toFun := f, map_mul' := h₁ }, map_zero' := h₂, map_add' := h₃ } = { toFun := f, map_mul' := h₁ }
theorem NonUnitalRingHom.coe_toAddMonoidHom {α : Type u_2} {β : Type u_3} (f : α →ₙ+* β) :
@[simp]
theorem NonUnitalRingHom.coe_addMonoidHom_mk {α : Type u_2} {β : Type u_3} (f : αβ) (h₁ : ∀ (x y : α), f (x * y) = f x * f y) (h₂ : MulHom.toFun { toFun := f, map_mul' := h₁ } 0 = 0) (h₃ : ∀ (x y : α), MulHom.toFun { toFun := f, map_mul' := h₁ } (x + y) = MulHom.toFun { toFun := f, map_mul' := h₁ } x + MulHom.toFun { toFun := f, map_mul' := h₁ } y) :
{ toMulHom := { toFun := f, map_mul' := h₁ }, map_zero' := h₂, map_add' := h₃ } = { toZeroHom := { toFun := f, map_zero' := h₂ }, map_add' := h₃ }
def NonUnitalRingHom.copy {α : Type u_2} {β : Type u_3} (f : α →ₙ+* β) (f' : αβ) (h : f' = f) :
α →ₙ+* β

Copy of a RingHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Instances For
@[simp]
theorem NonUnitalRingHom.coe_copy {α : Type u_2} {β : Type u_3} (f : α →ₙ+* β) (f' : αβ) (h : f' = f) :
↑() = f'
theorem NonUnitalRingHom.copy_eq {α : Type u_2} {β : Type u_3} (f : α →ₙ+* β) (f' : αβ) (h : f' = f) :
= f
theorem NonUnitalRingHom.ext {α : Type u_2} {β : Type u_3} ⦃f : α →ₙ+* β ⦃g : α →ₙ+* β :
(∀ (x : α), f x = g x) → f = g
theorem NonUnitalRingHom.ext_iff {α : Type u_2} {β : Type u_3} {f : α →ₙ+* β} {g : α →ₙ+* β} :
f = g ∀ (x : α), f x = g x
@[simp]
theorem NonUnitalRingHom.mk_coe {α : Type u_2} {β : Type u_3} (f : α →ₙ+* β) (h₁ : ∀ (x y : α), f (x * y) = f x * f y) (h₂ : MulHom.toFun { toFun := f, map_mul' := h₁ } 0 = 0) (h₃ : ∀ (x y : α), MulHom.toFun { toFun := f, map_mul' := h₁ } (x + y) = MulHom.toFun { toFun := f, map_mul' := h₁ } x + MulHom.toFun { toFun := f, map_mul' := h₁ } y) :
{ toMulHom := { toFun := f, map_mul' := h₁ }, map_zero' := h₂, map_add' := h₃ } = f
theorem NonUnitalRingHom.coe_mulHom_injective {α : Type u_2} {β : Type u_3} :
Function.Injective fun f => f
def NonUnitalRingHom.id (α : Type u_5) :
α →ₙ+* α

The identity non-unital ring homomorphism from a non-unital semiring to itself.

Instances For
@[simp]
theorem NonUnitalRingHom.coe_zero {α : Type u_2} {β : Type u_3} :
0 = 0
@[simp]
theorem NonUnitalRingHom.zero_apply {α : Type u_2} {β : Type u_3} (x : α) :
0 x = 0
@[simp]
theorem NonUnitalRingHom.id_apply {α : Type u_2} (x : α) :
↑() x = x
@[simp]
def NonUnitalRingHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} (g : β →ₙ+* γ) (f : α →ₙ+* β) :
α →ₙ+* γ

Composition of non-unital ring homomorphisms is a non-unital ring homomorphism.

Instances For
theorem NonUnitalRingHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} :
∀ {x : } (f : α →ₙ+* β) (g : β →ₙ+* γ) (h : γ →ₙ+* δ),

Composition of non-unital ring homomorphisms is associative.

@[simp]
theorem NonUnitalRingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} (g : β →ₙ+* γ) (f : α →ₙ+* β) :
↑() = g f
@[simp]
theorem NonUnitalRingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} (g : β →ₙ+* γ) (f : α →ₙ+* β) (x : α) :
↑() x = g (f x)
@[simp]
theorem NonUnitalRingHom.coe_comp_addMonoidHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} (g : β →ₙ+* γ) (f : α →ₙ+* β) :
{ toZeroHom := { toFun := g f, map_zero' := (_ : MulHom.toFun ().toMulHom 0 = 0) }, map_add' := (_ : ∀ (x y : α), MulHom.toFun ().toMulHom (x + y) = MulHom.toFun ().toMulHom x + MulHom.toFun ().toMulHom y) } =
@[simp]
theorem NonUnitalRingHom.coe_comp_mulHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} (g : β →ₙ+* γ) (f : α →ₙ+* β) :
{ toFun := g f, map_mul' := (_ : ∀ (x y : α), MulHom.toFun ().toMulHom (x * y) = MulHom.toFun ().toMulHom x * MulHom.toFun ().toMulHom y) } = MulHom.comp g f
@[simp]
theorem NonUnitalRingHom.comp_zero {α : Type u_2} {β : Type u_3} {γ : Type u_4} (g : β →ₙ+* γ) :
@[simp]
theorem NonUnitalRingHom.zero_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} (f : α →ₙ+* β) :
@[simp]
theorem NonUnitalRingHom.comp_id {α : Type u_2} {β : Type u_3} (f : α →ₙ+* β) :
@[simp]
theorem NonUnitalRingHom.id_comp {α : Type u_2} {β : Type u_3} (f : α →ₙ+* β) :
@[simp]
theorem NonUnitalRingHom.coe_one {α : Type u_2} :
1 = id
theorem NonUnitalRingHom.mul_def {α : Type u_2} (f : α →ₙ+* α) (g : α →ₙ+* α) :
f * g =
@[simp]
theorem NonUnitalRingHom.coe_mul {α : Type u_2} (f : α →ₙ+* α) (g : α →ₙ+* α) :
↑(f * g) = f g
@[simp]
theorem NonUnitalRingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} {g₁ : β →ₙ+* γ} {g₂ : β →ₙ+* γ} {f : α →ₙ+* β} (hf : ) :
g₁ = g₂
@[simp]
theorem NonUnitalRingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} {g : β →ₙ+* γ} {f₁ : α →ₙ+* β} {f₂ : α →ₙ+* β} (hg : ) :
f₁ = f₂
structure RingHom (α : Type u_5) (β : Type u_6) [] [] extends :
Type (max u_5 u_6)

Bundled semiring homomorphisms; use this for bundled ring homomorphisms too.

This extends from both MonoidHom and MonoidWithZeroHom in order to put the fields in a sensible order, even though MonoidWithZeroHom already extends MonoidHom.

Instances For

α →+* β denotes the type of ring homomorphisms from α to β.

Instances For
@[reducible]
abbrev RingHom.toMonoidWithZeroHom {α : Type u_5} {β : Type u_6} [] [] (self : α →+* β) :
α →*₀ β

Reinterpret a ring homomorphism f : α →+* β as a monoid with zero homomorphism α →*₀ β. The simp-normal form is (f : α →*₀ β).

Instances For
@[reducible]
abbrev RingHom.toAddMonoidHom {α : Type u_5} {β : Type u_6} [] [] (self : α →+* β) :
α →+ β

Reinterpret a ring homomorphism f : α →+* β as an additive monoid homomorphism α →+ β. The simp-normal form is (f : α →+ β).

Instances For
@[reducible]
abbrev RingHom.toNonUnitalRingHom {α : Type u_5} {β : Type u_6} [] [] (self : α →+* β) :
α →ₙ+* β

Reinterpret a ring homomorphism f : α →+* β as a non-unital ring homomorphism α →ₙ+* β. The simp-normal form is (f : α →ₙ+* β).

Instances For
class RingHomClass (F : Type u_5) (α : outParam (Type u_6)) (β : outParam (Type u_7)) [] [] extends :
Type (max (max u_5 u_6) u_7)
• coe : Fαβ
• coe_injective' : Function.Injective FunLike.coe
• map_mul : ∀ (f : F) (x y : α), f (x * y) = f x * f y
• map_one : ∀ (f : F), f 1 = 1
• map_add : ∀ (f : F) (x y : α), f (x + y) = f x + f y

The proposition that the function preserves addition

• map_zero : ∀ (f : F), f 0 = 0

The proposition that the function preserves 0

RingHomClass F α β states that F is a type of (semi)ring homomorphisms. You should extend this class when you extend RingHom.

This extends from both MonoidHomClass and MonoidWithZeroHomClass in order to put the fields in a sensible order, even though MonoidWithZeroHomClass already extends MonoidHomClass.

Instances
@[simp]
theorem map_bit1 {F : Type u_1} {α : Type u_2} {β : Type u_3} [] [] [RingHomClass F α β] (f : F) (a : α) :
f (bit1 a) = bit1 (f a)

Ring homomorphisms preserve bit1.

def RingHomClass.toRingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} :
{x : } → {x_1 : } → [inst : RingHomClass F α β] → Fα →+* β

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

Instances For
instance instCoeTCRingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} :
{x : } → {x_1 : } → [inst : RingHomClass F α β] → CoeTC F (α →+* β)

Any type satisfying RingHomClass can be cast into RingHom via RingHomClass.toRingHom.

instance RingHomClass.toNonUnitalRingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} :
{x : } → {x_1 : } → [inst : RingHomClass F α β] →

Throughout this section, some Semiring arguments are specified with {} instead of []. See note [implicit instance arguments].

instance RingHom.instRingHomClass {α : Type u_2} {β : Type u_3} :
{x : } → {x_1 : } → RingHomClass (α →+* β) α β
theorem RingHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } (f : α →+* β), f.toFun = f
@[simp]
theorem RingHom.coe_mk {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } (f : α →* β) (h₁ : OneHom.toFun (f) 0 = 0) (h₂ : ∀ (x_2 y : α), OneHom.toFun (f) (x_2 + y) = OneHom.toFun (f) x_2 + OneHom.toFun (f) y), { toMonoidHom := f, map_zero' := h₁, map_add' := h₂ } = f
@[simp]
theorem RingHom.coe_coe {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } {F : Type u_5} [inst : RingHomClass F α β] (f : F), f = f
instance RingHom.coeToMonoidHom {α : Type u_2} {β : Type u_3} :
{x : } → {x_1 : } → Coe (α →+* β) (α →* β)
@[simp]
theorem RingHom.toMonoidHom_eq_coe {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } (f : α →+* β), f = f
theorem RingHom.toMonoidWithZeroHom_eq_coe {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } (f : α →+* β), = f
@[simp]
theorem RingHom.coe_monoidHom_mk {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } (f : α →* β) (h₁ : OneHom.toFun (f) 0 = 0) (h₂ : ∀ (x_2 y : α), OneHom.toFun (f) (x_2 + y) = OneHom.toFun (f) x_2 + OneHom.toFun (f) y), { toMonoidHom := f, map_zero' := h₁, map_add' := h₂ } = f
@[simp]
theorem RingHom.toAddMonoidHom_eq_coe {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } (f : α →+* β),
@[simp]
theorem RingHom.coe_addMonoidHom_mk {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } (f : αβ) (h₁ : f 1 = 1) (h₂ : ∀ (x_2 y : α), OneHom.toFun { toFun := f, map_one' := h₁ } (x_2 * y) = OneHom.toFun { toFun := f, map_one' := h₁ } x_2 * OneHom.toFun { toFun := f, map_one' := h₁ } y) (h₃ : OneHom.toFun ({ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) 0 = 0) (h₄ : ∀ (x_2 y : α), OneHom.toFun ({ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) (x_2 + y) = OneHom.toFun ({ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) x_2 + OneHom.toFun ({ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) y), { toMonoidHom := { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ } = { toZeroHom := { toFun := f, map_zero' := h₃ }, map_add' := h₄ }
def RingHom.copy {α : Type u_2} {β : Type u_3} :
{x : } → {x_1 : } → (f : α →+* β) → (f' : αβ) → f' = fα →+* β

Copy of a RingHom with a new toFun equal to the old one. Useful to fix definitional equalities.

Instances For
@[simp]
theorem RingHom.coe_copy {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } (f : α →+* β) (f' : αβ) (h : f' = f), ↑(RingHom.copy f f' h) = f'
theorem RingHom.copy_eq {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } (f : α →+* β) (f' : αβ) (h : f' = f), RingHom.copy f f' h = f
theorem RingHom.congr_fun {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } {f g : α →+* β}, f = g∀ (x_2 : α), f x_2 = g x_2
theorem RingHom.congr_arg {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } (f : α →+* β) {x_2 y : α}, x_2 = yf x_2 = f y
theorem RingHom.coe_inj {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } ⦃f g : α →+* β⦄, f = gf = g
theorem RingHom.ext {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } ⦃f g : α →+* β⦄, (∀ (x_2 : α), f x_2 = g x_2) → f = g
theorem RingHom.ext_iff {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } {f g : α →+* β}, f = g ∀ (x_2 : α), f x_2 = g x_2
@[simp]
theorem RingHom.mk_coe {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } (f : α →+* β) (h₁ : f 1 = 1) (h₂ : ∀ (x_2 y : α), OneHom.toFun { toFun := f, map_one' := h₁ } (x_2 * y) = OneHom.toFun { toFun := f, map_one' := h₁ } x_2 * OneHom.toFun { toFun := f, map_one' := h₁ } y) (h₃ : OneHom.toFun ({ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) 0 = 0) (h₄ : ∀ (x_2 y : α), OneHom.toFun ({ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) (x_2 + y) = OneHom.toFun ({ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) x_2 + OneHom.toFun ({ toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }) y), { toMonoidHom := { toOneHom := { toFun := f, map_one' := h₁ }, map_mul' := h₂ }, map_zero' := h₃, map_add' := h₄ } = f
theorem RingHom.coe_addMonoidHom_injective {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : }, Function.Injective fun f => f
theorem RingHom.coe_monoidHom_injective {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : }, Function.Injective fun f => f
theorem RingHom.map_zero {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } (f : α →+* β), f 0 = 0

Ring homomorphisms map zero to zero.

theorem RingHom.map_one {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } (f : α →+* β), f 1 = 1

Ring homomorphisms map one to one.

theorem RingHom.map_add {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } (f : α →+* β) (a b : α), f (a + b) = f a + f b

Ring homomorphisms preserve addition.

theorem RingHom.map_mul {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } (f : α →+* β) (a b : α), f (a * b) = f a * f b

Ring homomorphisms preserve multiplication.

@[simp]
theorem RingHom.map_ite_zero_one {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } {F : Type u_5} [inst : RingHomClass F α β] (f : F) (p : Prop) [inst_1 : ], f (if p then 0 else 1) = if p then 0 else 1
@[simp]
theorem RingHom.map_ite_one_zero {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } {F : Type u_5} [inst : RingHomClass F α β] (f : F) (p : Prop) [inst_1 : ], f (if p then 1 else 0) = if p then 1 else 0
theorem RingHom.codomain_trivial_iff_map_one_eq_zero {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } (f : α →+* β), 0 = 1 f 1 = 0

f : α →+* β has a trivial codomain iff f 1 = 0.

theorem RingHom.codomain_trivial_iff_range_trivial {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } (f : α →+* β), 0 = 1 ∀ (x_2 : α), f x_2 = 0

f : α →+* β has a trivial codomain iff it has a trivial range.

theorem RingHom.map_one_ne_zero {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } (f : α →+* β) [inst : ], f 1 0

f : α →+* β doesn't map 1 to 0 if β is nontrivial

theorem RingHom.domain_nontrivial {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : }, (α →+* β) → ∀ [inst : ],

If there is a homomorphism f : α →+* β and β is nontrivial, then α is nontrivial.

theorem RingHom.codomain_trivial {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : }, (α →+* β) → ∀ [h : ],
theorem RingHom.map_neg {α : Type u_2} {β : Type u_3} [] [] (f : α →+* β) (x : α) :
f (-x) = -f x

Ring homomorphisms preserve additive inverse.

theorem RingHom.map_sub {α : Type u_2} {β : Type u_3} [] [] (f : α →+* β) (x : α) (y : α) :
f (x - y) = f x - f y

Ring homomorphisms preserve subtraction.

def RingHom.mk' {α : Type u_2} {β : Type u_3} [] [] (f : α →* β) (map_add : ∀ (a b : α), f (a + b) = f a + f b) :
α →+* β

Makes a ring homomorphism from a monoid homomorphism of rings which preserves addition.

Instances For
def RingHom.id (α : Type u_5) [] :
α →+* α

The identity ring homomorphism from a semiring to itself.

Instances For
instance RingHom.instInhabitedRingHom {α : Type u_2} :
{x : } → Inhabited (α →+* α)
@[simp]
theorem RingHom.id_apply {α : Type u_2} :
∀ {x : } (x_1 : α), ↑() x_1 = x_1
@[simp]
theorem RingHom.coe_addMonoidHom_id {α : Type u_2} :
∀ {x : }, ↑() =
@[simp]
theorem RingHom.coe_monoidHom_id {α : Type u_2} :
∀ {x : }, ↑() =
def RingHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} :
{x : } → {x_1 : } → {x_2 : } → (β →+* γ) → (α →+* β) → α →+* γ

Composition of ring homomorphisms is a ring homomorphism.

Instances For
theorem RingHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} :
∀ {x : } {x_1 : } {x_2 : } {δ : Type u_5} {x_3 : } (f : α →+* β) (g : β →+* γ) (h : γ →+* δ), RingHom.comp () f = RingHom.comp h ()

Composition of semiring homomorphisms is associative.

@[simp]
theorem RingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} :
∀ {x : } {x_1 : } {x_2 : } (hnp : β →+* γ) (hmn : α →+* β), ↑(RingHom.comp hnp hmn) = hnp hmn
theorem RingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} :
∀ {x : } {x_1 : } {x_2 : } (hnp : β →+* γ) (hmn : α →+* β) (x_3 : α), ↑(RingHom.comp hnp hmn) x_3 = hnp (hmn x_3)
@[simp]
theorem RingHom.comp_id {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } (f : α →+* β), = f
@[simp]
theorem RingHom.id_comp {α : Type u_2} {β : Type u_3} :
∀ {x : } {x_1 : } (f : α →+* β), = f
instance RingHom.instMonoidRingHom {α : Type u_2} :
{x : } → Monoid (α →+* α)
theorem RingHom.one_def {α : Type u_2} :
∀ {x : }, 1 =
theorem RingHom.mul_def {α : Type u_2} :
∀ {x : } (f g : α →+* α), f * g =
@[simp]
theorem RingHom.coe_one {α : Type u_2} :
∀ {x : }, 1 = id
@[simp]
theorem RingHom.coe_mul {α : Type u_2} :
∀ {x : } (f g : α →+* α), ↑(f * g) = f g
@[simp]
theorem RingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} :
∀ {x : } {x_1 : } {x_2 : } {g₁ g₂ : β →+* γ} {f : α →+* β}, → (RingHom.comp g₁ f = RingHom.comp g₂ f g₁ = g₂)
@[simp]
theorem RingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} :
∀ {x : } {x_1 : } {x_2 : } {g : β →+* γ} {f₁ f₂ : α →+* β}, → (RingHom.comp g f₁ = RingHom.comp g f₂ f₁ = f₂)
def AddMonoidHom.mkRingHomOfMulSelfOfTwoNeZero {α : Type u_2} {β : Type u_3} [] [] [] (f : β →+ α) (h : ∀ (x : β), f (x * x) = f x * f x) (h_two : 2 0) (h_one : f 1 = 1) :
β →+* α

Make a ring homomorphism from an additive group homomorphism from a commutative ring to an integral domain that commutes with self multiplication, assumes that two is nonzero and 1 is sent to 1.

Instances For
@[simp]
theorem AddMonoidHom.coe_fn_mkRingHomOfMulSelfOfTwoNeZero {α : Type u_2} {β : Type u_3} [] [] [] (f : β →+ α) (h : ∀ (x : β), f (x * x) = f x * f x) (h_two : 2 0) (h_one : f 1 = 1) :
theorem AddMonoidHom.coe_addMonoidHom_mkRingHomOfMulSelfOfTwoNeZero {α : Type u_2} {β : Type u_3} [] [] [] (f : β →+ α) (h : ∀ (x : β), f (x * x) = f x * f x) (h_two : 2 0) (h_one : f 1 = 1) :