Documentation

Mathlib.Algebra.Ring.Hom.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 #

Notations #

Implementation notes #

Tags #

RingHom, SemiringHom

structure NonUnitalRingHom (α : Type u_5) (β : Type u_6) [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] extends MulHom :
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.

  • toFun : αβ
  • map_mul' : ∀ (x y : α), self.toFun (x * y) = self.toFun x * self.toFun y
  • map_zero' : self.toFun 0 = 0

    The proposition that the function preserves 0

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

    The proposition that the function preserves addition

Instances For

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

    Equations
    Instances For
      @[reducible]

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

      Equations
      • self.toAddMonoidHom = { toFun := self.toFun, map_zero' := , map_add' := }
      Instances For

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

          Instances

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

            Equations
            • f = let __src := f; let __src_1 := f; { toMulHom := __src, map_zero' := , map_add' := }
            Instances For
              instance instCoeTCNonUnitalRingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [FunLike F α β] [NonUnitalRingHomClass F α β] :
              CoeTC F (α →ₙ+* β)

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

              Equations
              • instCoeTCNonUnitalRingHom = { coe := NonUnitalRingHomClass.toNonUnitalRingHom }
              Equations
              • NonUnitalRingHom.instFunLike = { coe := fun (f : α →ₙ+* β) => f.toFun, coe_injective' := }
              @[simp]
              theorem NonUnitalRingHom.coe_toMulHom {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) :
              f.toMulHom = f
              @[simp]
              theorem NonUnitalRingHom.coe_mulHom_mk {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : αβ) (h₁ : ∀ (x y : α), f (x * y) = f x * f y) (h₂ : { toFun := f, map_mul' := h₁ }.toFun 0 = 0) (h₃ : ∀ (x y : α), { toFun := f, map_mul' := h₁ }.toFun (x + y) = { toFun := f, map_mul' := h₁ }.toFun x + { toFun := f, map_mul' := h₁ }.toFun y) :
              { 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} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) :
              f.toAddMonoidHom = f
              @[simp]
              theorem NonUnitalRingHom.coe_addMonoidHom_mk {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : αβ) (h₁ : ∀ (x y : α), f (x * y) = f x * f y) (h₂ : { toFun := f, map_mul' := h₁ }.toFun 0 = 0) (h₃ : ∀ (x y : α), { toFun := f, map_mul' := h₁ }.toFun (x + y) = { toFun := f, map_mul' := h₁ }.toFun x + { toFun := f, map_mul' := h₁ }.toFun y) :
              { toFun := f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ } = { toFun := f, map_zero' := h₂, map_add' := h₃ }
              def NonUnitalRingHom.copy {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) (f' : αβ) (h : f' = f) :
              α →ₙ+* β

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

              Equations
              • f.copy f' h = let __src := f.copy f' h; let __src_1 := f.toAddMonoidHom.copy f' h; { toMulHom := __src, map_zero' := , map_add' := }
              Instances For
                @[simp]
                theorem NonUnitalRingHom.coe_copy {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) (f' : αβ) (h : f' = f) :
                (f.copy f' h) = f'
                theorem NonUnitalRingHom.copy_eq {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) (f' : αβ) (h : f' = f) :
                f.copy f' h = f
                theorem NonUnitalRingHom.ext_iff {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] {f : α →ₙ+* β} {g : α →ₙ+* β} :
                f = g ∀ (x : α), f x = g x
                theorem NonUnitalRingHom.ext {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] ⦃f : α →ₙ+* β ⦃g : α →ₙ+* β :
                (∀ (x : α), f x = g x)f = g
                @[simp]
                theorem NonUnitalRingHom.mk_coe {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) (h₁ : ∀ (x y : α), f (x * y) = f x * f y) (h₂ : { toFun := f, map_mul' := h₁ }.toFun 0 = 0) (h₃ : ∀ (x y : α), { toFun := f, map_mul' := h₁ }.toFun (x + y) = { toFun := f, map_mul' := h₁ }.toFun x + { toFun := f, map_mul' := h₁ }.toFun y) :
                { toFun := f, map_mul' := h₁, map_zero' := h₂, map_add' := h₃ } = f

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

                Equations
                Instances For
                  Equations
                  • NonUnitalRingHom.instZero = { zero := { toFun := 0, map_mul' := , map_zero' := , map_add' := } }
                  Equations
                  • NonUnitalRingHom.instInhabited = { default := 0 }
                  @[simp]
                  @[simp]
                  theorem NonUnitalRingHom.zero_apply {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (x : α) :
                  0 x = 0
                  @[simp]
                  def NonUnitalRingHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β) :
                  α →ₙ+* γ

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

                  Equations
                  • g.comp f = let __src := g.comp f.toMulHom; let __src_1 := g.toAddMonoidHom.comp f.toAddMonoidHom; { toMulHom := __src, map_zero' := , map_add' := }
                  Instances For
                    theorem NonUnitalRingHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] {δ : Type u_5} :
                    ∀ {x : NonUnitalNonAssocSemiring δ} (f : α →ₙ+* β) (g : β →ₙ+* γ) (h : γ →ₙ+* δ), (h.comp g).comp f = h.comp (g.comp f)

                    Composition of non-unital ring homomorphisms is associative.

                    @[simp]
                    theorem NonUnitalRingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β) :
                    (g.comp f) = g f
                    @[simp]
                    theorem NonUnitalRingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β) (x : α) :
                    (g.comp f) x = g (f x)
                    @[simp]
                    theorem NonUnitalRingHom.coe_comp_addMonoidHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β) :
                    { toFun := g f, map_zero' := , map_add' := } = (↑g).comp f
                    @[simp]
                    theorem NonUnitalRingHom.coe_comp_mulHom {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β) :
                    { toFun := g f, map_mul' := } = (↑g).comp f
                    @[simp]
                    theorem NonUnitalRingHom.comp_zero {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) :
                    g.comp 0 = 0
                    @[simp]
                    theorem NonUnitalRingHom.comp_id {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) :
                    f.comp (NonUnitalRingHom.id α) = f
                    @[simp]
                    theorem NonUnitalRingHom.id_comp {α : Type u_2} {β : Type u_3} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] (f : α →ₙ+* β) :
                    (NonUnitalRingHom.id β).comp f = f
                    Equations
                    @[simp]
                    theorem NonUnitalRingHom.coe_one {α : Type u_2} [NonUnitalNonAssocSemiring α] :
                    1 = id
                    theorem NonUnitalRingHom.mul_def {α : Type u_2} [NonUnitalNonAssocSemiring α] (f : α →ₙ+* α) (g : α →ₙ+* α) :
                    f * g = f.comp g
                    @[simp]
                    theorem NonUnitalRingHom.coe_mul {α : Type u_2} [NonUnitalNonAssocSemiring α] (f : α →ₙ+* α) (g : α →ₙ+* α) :
                    (f * g) = f g
                    @[simp]
                    theorem NonUnitalRingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] {g₁ : β →ₙ+* γ} {g₂ : β →ₙ+* γ} {f : α →ₙ+* β} (hf : Function.Surjective f) :
                    g₁.comp f = g₂.comp f g₁ = g₂
                    @[simp]
                    theorem NonUnitalRingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} [NonUnitalNonAssocSemiring α] [NonUnitalNonAssocSemiring β] [NonUnitalNonAssocSemiring γ] {g : β →ₙ+* γ} {f₁ : α →ₙ+* β} {f₂ : α →ₙ+* β} (hg : Function.Injective g) :
                    g.comp f₁ = g.comp f₂ f₁ = f₂
                    structure RingHom (α : Type u_5) (β : Type u_6) [NonAssocSemiring α] [NonAssocSemiring β] extends MonoidHom :
                    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.

                    • toFun : αβ
                    • map_one' : (↑self).toFun 1 = 1
                    • map_mul' : ∀ (x y : α), (↑self).toFun (x * y) = (↑self).toFun x * (↑self).toFun y
                    • map_zero' : (↑self).toFun 0 = 0

                      The proposition that the function preserves 0

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

                      The proposition that the function preserves addition

                    Instances For

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

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

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

                        Equations
                        • self.toMonoidWithZeroHom = { toFun := (↑self).toFun, map_zero' := , map_one' := , map_mul' := }
                        Instances For
                          @[reducible]
                          abbrev RingHom.toAddMonoidHom {α : Type u_5} {β : Type u_6} [NonAssocSemiring α] [NonAssocSemiring β] (self : α →+* β) :
                          α →+ β

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

                          Equations
                          • self.toAddMonoidHom = { toFun := (↑self).toFun, map_zero' := , map_add' := }
                          Instances For
                            @[reducible]
                            abbrev RingHom.toNonUnitalRingHom {α : Type u_5} {β : Type u_6} [NonAssocSemiring α] [NonAssocSemiring β] (self : α →+* β) :
                            α →ₙ+* β

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

                            Equations
                            • self.toNonUnitalRingHom = { toFun := (↑self).toFun, map_mul' := , map_zero' := , map_add' := }
                            Instances For
                              class RingHomClass (F : Type u_5) (α : outParam (Type u_6)) (β : outParam (Type u_7)) [NonAssocSemiring α] [NonAssocSemiring β] [FunLike F α β] extends MonoidHomClass , AddMonoidHomClass :

                              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
                                  def RingHomClass.toRingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] :
                                  {x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → [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 α →+* β.

                                  Equations
                                  • f = let __src := f; let __src_1 := f; { toMonoidHom := __src, map_zero' := , map_add' := }
                                  Instances For
                                    instance instCoeTCRingHom {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] :
                                    {x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → [inst : RingHomClass F α β] → CoeTC F (α →+* β)

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

                                    Equations
                                    • instCoeTCRingHom = { coe := RingHomClass.toRingHom }
                                    @[instance 100]
                                    instance RingHomClass.toNonUnitalRingHomClass {F : Type u_1} {α : Type u_2} {β : Type u_3} [FunLike F α β] :
                                    ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} [inst : RingHomClass F α β], NonUnitalRingHomClass F α β
                                    Equations
                                    • =

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

                                    instance RingHom.instFunLike {α : Type u_2} {β : Type u_3} :
                                    {x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → FunLike (α →+* β) α β
                                    Equations
                                    • RingHom.instFunLike = { coe := fun (f : α →+* β) => (↑f).toFun, coe_injective' := }
                                    instance RingHom.instRingHomClass {α : Type u_2} {β : Type u_3} :
                                    ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β}, RingHomClass (α →+* β) α β
                                    Equations
                                    • =
                                    theorem RingHom.toFun_eq_coe {α : Type u_2} {β : Type u_3} :
                                    ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), (↑f).toFun = f
                                    @[simp]
                                    theorem RingHom.coe_mk {α : Type u_2} {β : Type u_3} :
                                    ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →* β) (h₁ : (↑f).toFun 0 = 0) (h₂ : ∀ (x_2 y : α), (↑f).toFun (x_2 + y) = (↑f).toFun x_2 + (↑f).toFun y), { toMonoidHom := f, map_zero' := h₁, map_add' := h₂ } = f
                                    @[simp]
                                    theorem RingHom.coe_coe {α : Type u_2} {β : Type u_3} :
                                    ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {F : Type u_5} [inst : FunLike F α β] [inst_1 : RingHomClass F α β] (f : F), f = f
                                    instance RingHom.coeToMonoidHom {α : Type u_2} {β : Type u_3} :
                                    {x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → Coe (α →+* β) (α →* β)
                                    Equations
                                    • RingHom.coeToMonoidHom = { coe := RingHom.toMonoidHom }
                                    @[simp]
                                    theorem RingHom.toMonoidHom_eq_coe {α : Type u_2} {β : Type u_3} :
                                    ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), f = f
                                    theorem RingHom.toMonoidWithZeroHom_eq_coe {α : Type u_2} {β : Type u_3} :
                                    ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), f.toMonoidWithZeroHom = f
                                    @[simp]
                                    theorem RingHom.coe_monoidHom_mk {α : Type u_2} {β : Type u_3} :
                                    ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →* β) (h₁ : (↑f).toFun 0 = 0) (h₂ : ∀ (x_2 y : α), (↑f).toFun (x_2 + y) = (↑f).toFun x_2 + (↑f).toFun y), { toMonoidHom := f, map_zero' := h₁, map_add' := h₂ } = f
                                    @[simp]
                                    theorem RingHom.toAddMonoidHom_eq_coe {α : Type u_2} {β : Type u_3} :
                                    ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), f.toAddMonoidHom = f
                                    @[simp]
                                    theorem RingHom.coe_addMonoidHom_mk {α : Type u_2} {β : Type u_3} :
                                    ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : αβ) (h₁ : f 1 = 1) (h₂ : ∀ (x_2 y : α), { toFun := f, map_one' := h₁ }.toFun (x_2 * y) = { toFun := f, map_one' := h₁ }.toFun x_2 * { toFun := f, map_one' := h₁ }.toFun y) (h₃ : (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0) (h₄ : ∀ (x_2 y : α), (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun (x_2 + y) = (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun x_2 + (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun y), { toFun := f, map_one' := h₁, map_mul' := h₂, map_zero' := h₃, map_add' := h₄ } = { toFun := f, map_zero' := h₃, map_add' := h₄ }
                                    def RingHom.copy {α : Type u_2} {β : Type u_3} :
                                    {x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → (f : α →+* β) → (f' : αβ) → f' = fα →+* β

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

                                    Equations
                                    • f.copy f' h = let __src := f.toMonoidWithZeroHom.copy f' h; let __src_1 := f.toAddMonoidHom.copy f' h; { toMonoidHom := __src, map_zero' := , map_add' := }
                                    Instances For
                                      @[simp]
                                      theorem RingHom.coe_copy {α : Type u_2} {β : Type u_3} :
                                      ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (f' : αβ) (h : f' = f), (f.copy f' h) = f'
                                      theorem RingHom.copy_eq {α : Type u_2} {β : Type u_3} :
                                      ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (f' : αβ) (h : f' = f), f.copy f' h = f
                                      theorem RingHom.congr_fun {α : Type u_2} {β : Type u_3} :
                                      ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {f g : α →+* β}, f = g∀ (x_2 : α), f x_2 = g x_2
                                      theorem RingHom.congr_arg {α : Type u_2} {β : Type u_3} :
                                      ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) {x_2 y : α}, x_2 = yf x_2 = f y
                                      theorem RingHom.coe_inj {α : Type u_2} {β : Type u_3} :
                                      ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} ⦃f g : α →+* β⦄, f = gf = g
                                      theorem RingHom.ext_iff {α : Type u_2} {β : Type u_3} :
                                      ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {f g : α →+* β}, f = g ∀ (x_2 : α), f x_2 = g x_2
                                      theorem RingHom.ext {α : Type u_2} {β : Type u_3} :
                                      ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} ⦃f g : α →+* β⦄, (∀ (x_2 : α), f x_2 = g x_2)f = g
                                      @[simp]
                                      theorem RingHom.mk_coe {α : Type u_2} {β : Type u_3} :
                                      ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) (h₁ : f 1 = 1) (h₂ : ∀ (x_2 y : α), { toFun := f, map_one' := h₁ }.toFun (x_2 * y) = { toFun := f, map_one' := h₁ }.toFun x_2 * { toFun := f, map_one' := h₁ }.toFun y) (h₃ : (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun 0 = 0) (h₄ : ∀ (x_2 y : α), (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun (x_2 + y) = (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun x_2 + (↑{ toFun := f, map_one' := h₁, map_mul' := h₂ }).toFun y), { 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 : NonAssocSemiring α} {x_1 : NonAssocSemiring β}, Function.Injective fun (f : α →+* β) => f
                                      theorem RingHom.coe_monoidHom_injective {α : Type u_2} {β : Type u_3} :
                                      ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β}, Function.Injective fun (f : α →+* β) => f
                                      theorem RingHom.map_zero {α : Type u_2} {β : Type u_3} :
                                      ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), f 0 = 0

                                      Ring homomorphisms map zero to zero.

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

                                      Ring homomorphisms map one to one.

                                      theorem RingHom.map_add {α : Type u_2} {β : Type u_3} :
                                      ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (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 : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (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 : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {F : Type u_5} [inst : FunLike F α β] [inst_1 : RingHomClass F α β] (f : F) (p : Prop) [inst_2 : Decidable p], 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 : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {F : Type u_5} [inst : FunLike F α β] [inst_1 : RingHomClass F α β] (f : F) (p : Prop) [inst_2 : Decidable p], 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 : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (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 : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (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 : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β) [inst : Nontrivial β], f 1 0

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

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

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

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

                                      Ring homomorphisms preserve additive inverse.

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

                                      Ring homomorphisms preserve subtraction.

                                      def RingHom.mk' {α : Type u_2} {β : Type u_3} [NonAssocSemiring α] [NonAssocRing β] (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.

                                      Equations
                                      • RingHom.mk' f map_add = let __src := AddMonoidHom.mk' (⇑f) map_add; { toFun := (↑__src).toFun, map_one' := , map_mul' := , map_zero' := , map_add' := }
                                      Instances For
                                        def RingHom.id (α : Type u_5) [NonAssocSemiring α] :
                                        α →+* α

                                        The identity ring homomorphism from a semiring to itself.

                                        Equations
                                        • RingHom.id α = { toFun := id, map_one' := , map_mul' := , map_zero' := , map_add' := }
                                        Instances For
                                          instance RingHom.instInhabited {α : Type u_2} :
                                          {x : NonAssocSemiring α} → Inhabited (α →+* α)
                                          Equations
                                          @[simp]
                                          theorem RingHom.id_apply {α : Type u_2} :
                                          ∀ {x : NonAssocSemiring α} (x_1 : α), (RingHom.id α) x_1 = x_1
                                          @[simp]
                                          theorem RingHom.coe_addMonoidHom_id {α : Type u_2} :
                                          ∀ {x : NonAssocSemiring α}, (RingHom.id α) = AddMonoidHom.id α
                                          @[simp]
                                          theorem RingHom.coe_monoidHom_id {α : Type u_2} :
                                          ∀ {x : NonAssocSemiring α}, (RingHom.id α) = MonoidHom.id α
                                          def RingHom.comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} :
                                          {x : NonAssocSemiring α} → {x_1 : NonAssocSemiring β} → {x_2 : NonAssocSemiring γ} → (β →+* γ)(α →+* β)α →+* γ

                                          Composition of ring homomorphisms is a ring homomorphism.

                                          Equations
                                          • g.comp f = let __src := g.toNonUnitalRingHom.comp f.toNonUnitalRingHom; { toFun := g f, map_one' := , map_mul' := , map_zero' := , map_add' := }
                                          Instances For
                                            theorem RingHom.comp_assoc {α : Type u_2} {β : Type u_3} {γ : Type u_4} :
                                            ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {x_2 : NonAssocSemiring γ} {δ : Type u_5} {x_3 : NonAssocSemiring δ} (f : α →+* β) (g : β →+* γ) (h : γ →+* δ), (h.comp g).comp f = h.comp (g.comp f)

                                            Composition of semiring homomorphisms is associative.

                                            @[simp]
                                            theorem RingHom.coe_comp {α : Type u_2} {β : Type u_3} {γ : Type u_4} :
                                            ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {x_2 : NonAssocSemiring γ} (hnp : β →+* γ) (hmn : α →+* β), (hnp.comp hmn) = hnp hmn
                                            theorem RingHom.comp_apply {α : Type u_2} {β : Type u_3} {γ : Type u_4} :
                                            ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {x_2 : NonAssocSemiring γ} (hnp : β →+* γ) (hmn : α →+* β) (x_3 : α), (hnp.comp hmn) x_3 = hnp (hmn x_3)
                                            @[simp]
                                            theorem RingHom.comp_id {α : Type u_2} {β : Type u_3} :
                                            ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), f.comp (RingHom.id α) = f
                                            @[simp]
                                            theorem RingHom.id_comp {α : Type u_2} {β : Type u_3} :
                                            ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), (RingHom.id β).comp f = f
                                            instance RingHom.instOne {α : Type u_2} :
                                            {x : NonAssocSemiring α} → One (α →+* α)
                                            Equations
                                            instance RingHom.instMul {α : Type u_2} :
                                            {x : NonAssocSemiring α} → Mul (α →+* α)
                                            Equations
                                            • RingHom.instMul = { mul := RingHom.comp }
                                            theorem RingHom.one_def {α : Type u_2} :
                                            ∀ {x : NonAssocSemiring α}, 1 = RingHom.id α
                                            theorem RingHom.mul_def {α : Type u_2} :
                                            ∀ {x : NonAssocSemiring α} (f g : α →+* α), f * g = f.comp g
                                            @[simp]
                                            theorem RingHom.coe_one {α : Type u_2} :
                                            ∀ {x : NonAssocSemiring α}, 1 = id
                                            @[simp]
                                            theorem RingHom.coe_mul {α : Type u_2} :
                                            ∀ {x : NonAssocSemiring α} (f g : α →+* α), (f * g) = f g
                                            instance RingHom.instMonoid {α : Type u_2} :
                                            {x : NonAssocSemiring α} → Monoid (α →+* α)
                                            Equations
                                            @[simp]
                                            theorem RingHom.coe_pow {α : Type u_2} :
                                            ∀ {x : NonAssocSemiring α} (f : α →+* α) (n : ), (f ^ n) = (⇑f)^[n]
                                            @[simp]
                                            theorem RingHom.cancel_right {α : Type u_2} {β : Type u_3} {γ : Type u_4} :
                                            ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {x_2 : NonAssocSemiring γ} {g₁ g₂ : β →+* γ} {f : α →+* β}, Function.Surjective f(g₁.comp f = g₂.comp f g₁ = g₂)
                                            @[simp]
                                            theorem RingHom.cancel_left {α : Type u_2} {β : Type u_3} {γ : Type u_4} :
                                            ∀ {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} {x_2 : NonAssocSemiring γ} {g : β →+* γ} {f₁ f₂ : α →+* β}, Function.Injective g(g.comp f₁ = g.comp f₂ f₁ = f₂)
                                            theorem RingHom.map_pow {α : Type u_2} {β : Type u_3} [Semiring α] [Semiring β] (f : α →+* β) (a : α) (n : ) :
                                            f (a ^ n) = f a ^ n
                                            def AddMonoidHom.mkRingHomOfMulSelfOfTwoNeZero {α : Type u_2} {β : Type u_3} [CommRing α] [IsDomain α] [CommRing β] (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.

                                            Equations
                                            • f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one = { toFun := (↑f).toFun, map_one' := h_one, map_mul' := , map_zero' := , map_add' := }
                                            Instances For
                                              @[simp]
                                              theorem AddMonoidHom.coe_fn_mkRingHomOfMulSelfOfTwoNeZero {α : Type u_2} {β : Type u_3} [CommRing α] [IsDomain α] [CommRing β] (f : β →+ α) (h : ∀ (x : β), f (x * x) = f x * f x) (h_two : 2 0) (h_one : f 1 = 1) :
                                              (f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one) = f
                                              theorem AddMonoidHom.coe_addMonoidHom_mkRingHomOfMulSelfOfTwoNeZero {α : Type u_2} {β : Type u_3} [CommRing α] [IsDomain α] [CommRing β] (f : β →+ α) (h : ∀ (x : β), f (x * x) = f x * f x) (h_two : 2 0) (h_one : f 1 = 1) :
                                              (f.mkRingHomOfMulSelfOfTwoNeZero h h_two h_one) = f