map_bit1
theorem map_bit1 :
∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : NonAssocSemiring α]
[inst_2 : NonAssocSemiring β] [inst_3 : RingHomClass F α β] (f : F) (a : α), f (bit1 a) = bit1 (f a)
The theorem `map_bit1` states that for any types `F`, `α`, and `β`, if `F` has an structure of function from `α` to `β` (as expressed by `FunLike F α β`), `α` and `β` have structures of non-associative semirings, and `F` has an structure of ring homomorphism from `α` to `β` (as expressed by `RingHomClass F α β`), then for any function `f : F` and any element `a : α`, applying `f` to `bit1 a` (where `bit1` is a function that maps an element `a` to `bit0 a + 1`, essentially representing the operation of multiplying by 2 and then adding 1) is the same as applying `f` to `a` and then applying `bit1` to the result. In other words, ring homomorphisms preserve the `bit1` operation.
More concisely: For any function `F : α -> β` with ring homomorphism structure between non-associative semirings `α` and `β`, `F (bit1 a) = bit1 (F a)` for all `a : α`, where `bit1` is the operation of adding 1 after multiplying by 2.
|
RingHom.codomain_trivial_iff_map_one_eq_zero
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
This theorem states that for a ring homomorphism `f` from a non-associative semiring `α` to another non-associative semiring `β`, the codomain of `f` is trivial (i.e., consists of a single element) if and only if the mapping of the unit element `1` under `f` is the zero element. In other words, it provides a condition to check if a ring homomorphism has a trivial codomain; this occurs precisely when the image of the unit element is zero.
More concisely: A ring homomorphism from a non-associative semiring to another non-associative semiring has a trivial codomain if and only if the image of its unit element is the zero element.
|
NonUnitalRingHom.map_add'
theorem NonUnitalRingHom.map_add' :
∀ {α : Type u_5} {β : Type u_6} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
(self : α →ₙ+* β) (x y : α), self.toFun (x + y) = self.toFun x + self.toFun y
This theorem, `NonUnitalRingHom.map_add'`, states that for all types `α` and `β`, which are non-unital and non-associative semirings, a given function `self` (which is a non-unital ring homomorphism from `α` to `β`) preserves addition. In other words, applying this function `self` to the sum of any two elements `x` and `y` in `α` will yield the same result as summing the outputs of applying the function to `x` and `y` individually. Mathematically, this can be expressed as `self(x + y) = self(x) + self(y)`.
More concisely: For any non-unital and non-associative semirings α and β, a non-unital ring homomorphism from α to β preserves addition: self(x + y) = self(x) + self(y).
|
RingHom.id_comp
theorem RingHom.id_comp :
∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β),
(RingHom.id β).comp f = f
The theorem `RingHom.id_comp` states that for any two types `α` and `β` which are non-associative semirings, and any ring homomorphism `f` from `α` to `β`, the composition of `f` with the identity ring homomorphism on `β` is equal to `f`. In other words, composing any ring homomorphism with the identity function on the codomain does not change the original homomorphism. This property is one of the defining features of identity functions in the context of ring theory.
More concisely: For any non-associative semirings `α` and `β`, and any ring homomorphism `f` from `α` to `β`, `f ∘ id_β = f`, where `id_β` is the identity ring homomorphism on `β`.
|
RingHom.ext
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
This theorem, `RingHom.ext`, states that for any two ring homomorphisms `f` and `g` from a non-associative semiring `α` to another non-associative semiring `β`, if `f` and `g` are equal for every element in semiring `α`, then `f` and `g` are indeed the same function. In other words, two ring homomorphisms are identical if they map each element of the domain semiring to the same element in the codomain semiring.
More concisely: If two ring homomorphisms between non-associative semirings map every element to the same image, then they are equal as functions.
|
RingHom.coe_addMonoidHom_injective
theorem RingHom.coe_addMonoidHom_injective :
∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β},
Function.Injective fun f => ↑f
The theorem `RingHom.coe_addMonoidHom_injective` states that for any two non-associative semirings `α` and `β`, the function that maps a ring homomorphism to its underlying additive monoid homomorphism is injective. In other words, if two ring homomorphisms from `α` to `β` are equivalent as additive monoid homomorphisms, then they were the same ring homomorphism to begin with. This means that the additive structure of a ring homomorphism uniquely determines it.
More concisely: Given any two ring homomorphisms between non-associative semirings, if they have the same underlying additive monoid homomorphisms, then they are equal as ring homomorphisms.
|
NonUnitalRingHom.comp_assoc
theorem NonUnitalRingHom.comp_assoc :
∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : NonUnitalNonAssocSemiring α]
[inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] {δ : Type u_5}
{x : NonUnitalNonAssocSemiring δ} (f : α →ₙ+* β) (g : β →ₙ+* γ) (h : γ →ₙ+* δ),
(h.comp g).comp f = h.comp (g.comp f)
This theorem states that for any three non-unital non-associative semirings α, β, γ, and another non-unital non-associative semiring δ, the composition of non-unital ring homomorphisms is associative. In other words, given any three homomorphisms `f` from α to β, `g` from β to γ, and `h` from γ to δ, the composition of `h` and `g` first, and then `f` is equal to the composition of `h` and the composition of `g` and `f`. This is written symbolically as `(h.comp g).comp f = h.comp (g.comp f)`.
More concisely: For any three non-unital non-associative semirings α, β, γ, and given any three homomorphisms f : α -> β, g : β -> γ, and h : γ -> δ, the associativity of composition holds: (h.comp g).comp f = h.comp (g.comp f).
|
RingHom.map_one
theorem RingHom.map_one :
∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), f 1 = 1 := by
sorry
This theorem states that for any ring homomorphism `f` from a non-associative semiring `α` to another non-associative semiring `β`, the image of 1 under `f` is 1. In other words, a ring homomorphism always maps the multiplicative identity of the source ring (1 in `α`) to the multiplicative identity of the target ring (1 in `β`).
More concisely: For any ring homomorphism `f` between non-associative semirings, `f 1 = 1`.
|
RingHom.congr_fun
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
This theorem, `RingHom.congr_fun`, states that for any two ring homomorphisms `f` and `g` from a non-associative semiring `α` to another non-associative semiring `β`, if `f` and `g` are equal, then the results of applying `f` and `g` to any element `x_2` from the semiring `α` are also equal. In other words, if two ring homomorphisms are the same, then they map any given element to the same element in the target semiring.
More concisely: If two ring homomorphisms from a semiring to another semiring are equal, then they map any element to the same image.
|
RingHom.ext_iff
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
This theorem states a property of ring homomorphisms between two non-associative semirings. Specifically, it says that for any two ring homomorphisms `f` and `g` from a non-associative semiring `α` to another non-associative semiring `β`, `f` and `g` are equal if and only if they produce the same output for every input from `α`. In other words, two ring homomorphisms are identical if they behave in the same way for all elements of the domain semiring.
More concisely: Two ring homomorphisms between non-associative semirings are equal if and only if they map every element in the domain to the same image.
|
RingHom.domain_nontrivial
theorem RingHom.domain_nontrivial :
∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β},
(α →+* β) → ∀ [inst : Nontrivial β], Nontrivial α
This theorem states that if there exists a ring homomorphism, denoted by `f`, from a type `α` to a type `β` and `β` is nontrivial (i.e., it contains at least two distinct elements), then `α` must also be nontrivial. In other words, you cannot have a homomorphism from a trivial ring to a nontrivial one. Here, `α` and `β` are types with a Non-Associative Semiring structure, which is a mathematical structure that includes operations like addition and multiplication but does not require the multiplication to be associative.
More concisely: If `α` is a Non-Associative Semiring and there exists a homomorphism from `α` to a nontrivial `β` (Non-Associative Semiring), then `α` is also nontrivial.
|
RingHom.map_zero
theorem RingHom.map_zero :
∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β), f 0 = 0 := by
sorry
This theorem states that for any ring homomorphism `f` from a non-associative semiring `α` to another non-associative semiring `β`, the mapping of the element zero from `α` through `f` will always result in the zero element of `β`. In other words, ring homomorphisms preserve the zero element across different non-associative semirings.
More concisely: For any ring homomorphism between non-associative semirings, the image of the zero element is the zero element.
|
RingHom.map_mul
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
The theorem `RingHom.map_mul` states that for any two types `α` and `β` with their respective non-associative semirings `x` and `x_1`, and given a ring homomorphism `f` from `α` to `β` and two elements `a` and `b` of type `α`, the application of `f` on the product of `a` and `b` (i.e., `f (a * b)`) is equal to the product of `f a` and `f b`. This means that the multiplication operation is preserved under the ring homomorphism `f`.
More concisely: Given ring homomorphisms `f : α → β` between semirings `x` and `x_1`, and elements `a` and `b` from `α`, we have `f (a * b) = f a * f b`.
|
RingHom.map_sub
theorem RingHom.map_sub :
∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocRing α] [inst_1 : NonAssocRing β] (f : α →+* β) (x y : α),
f (x - y) = f x - f y
This theorem states that ring homomorphisms preserve the operation of subtraction. Specifically, for any two types, `α` and `β`, that form non-associative rings, any ring homomorphism `f : α →+* β` maps the subtraction of any two elements in `α` to the subtraction of their images in `β`. In other words, for all `x` and `y` in `α`, applying the homomorphism to `x - y` results in `f(x) - f(y)` in `β`.
More concisely: For any non-associative ring homomorphism `f : α →+* β`, `f(x - y) = f(x) - f(y)` for all `x, y ∈ α`.
|
RingHom.comp_assoc
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)
The theorem `RingHom.comp_assoc` states that the composition of semiring homomorphisms is associative. In other words, for any three semiring homomorphisms `f`, `g`, and `h` (where `f` is a function from a nonassociative semiring `α` to a nonassociative semiring `β`, `g` is a function from `β` to `γ`, and `h` is a function from `γ` to `δ`), composing `h` and `g` first and then composing the result with `f` is the same as first composing `g` and `f` and then composing `h` with the result. This is a fundamental property of function composition and is essential in many areas of mathematics and computer science.
More concisely: For any semiring homomorphisms $f:\alpha \to \beta$, $g:\beta \to \gamma$, and $h:\gamma \to \delta$, $h \circ g \circ f = g \circ f \circ h$.
|
RingHom.comp_apply
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)
The theorem `RingHom.comp_apply` states that for any three types `α`, `β`, and `γ` which are all non-associative semirings, and for any two ring homomorphisms (one from `α` to `β` and the other from `β` to `γ`), the composition of these two homomorphisms applied to an element of `α` is equal to applying the second homomorphism to the result of applying the first homomorphism to the element. In other words, if we have two function `hmn : α → β` and `hnp : β → γ` and an element `x_3 : α`, then applying the composed homomorphism `(RingHom.comp hnp hmn)` to `x_3` is the same as first applying `hmn` to `x_3` and then applying `hnp` to the result. This is a formalization of the usual property of function composition in the context of ring homomorphisms.
More concisely: For any non-associative semirings α, β, and γ, and ring homomorphisms hmn : α → β and hnp : β → γ, (hnp ∘ hmn)(x) = hnp(hmn(x)) for all x ∈ α.
|
RingHom.map_one_ne_zero
theorem RingHom.map_one_ne_zero :
∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β)
[inst : Nontrivial β], f 1 ≠ 0
This theorem states that for any ring homomorphism `f` from a type `α` to another type `β` (both of which are non-associative semirings), if `β` is nontrivial (i.e., it has at least two distinct elements), then `f` does not map the multiplicative identity `1` of `α` to the additive identity `0` of `β`. In other words, `f(1)` is not equal to `0` when `β` is nontrivial.
More concisely: If `α` and `β` are non-associative semirings, `f` is a ring homomorphism from `α` to `β`, and `β` is nontrivial, then `f(1) ≠ 0`.
|
RingHom.map_neg
theorem RingHom.map_neg :
∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocRing α] [inst_1 : NonAssocRing β] (f : α →+* β) (x : α),
f (-x) = -f x
The theorem `RingHom.map_neg` states that for any two types `α` and `β`, if they are both non-associative rings (indicated by `NonAssocRing α` and `NonAssocRing β`), then for a ring homomorphism `f` from `α` to `β` and any element `x` of `α`, the ring homomorphism of the additive inverse of `x` (-x) is equal to the additive inverse of the ring homomorphism of `x` (-f x). In simpler terms, ring homomorphisms preserve the property of additive inverses.
More concisely: For any non-associative rings α and β and ring homomorphism f : α → β, we have -(f(x)) = f(-x) for all x ∈ α.
|
RingHom.map_zero'
theorem RingHom.map_zero' :
∀ {α : Type u_5} {β : Type u_6} [inst : NonAssocSemiring α] [inst_1 : NonAssocSemiring β] (self : α →+* β),
self.toFun 0 = 0
This theorem, `RingHom.map_zero'`, declares that for any two non-associative semirings, denoted by α and β, any ring homomorphism from α to β preserves the element 0. In other words, the ring homomorphism maps 0 in α to 0 in β.
More concisely: Given any non-associative semirings α and β and a ring homomorphism f from α to β, f maps the additive identity 0 of α to the additive identity 0 of β.
|
RingHom.coe_inj
theorem RingHom.coe_inj :
∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} ⦃f g : α →+* β⦄,
⇑f = ⇑g → f = g
This theorem, `RingHom.coe_inj`, asserts that for any two ring homomorphisms `f` and `g` from a non-associative semiring `α` to another non-associative semiring `β`, if the function application of `f` and `g` (denoted by `⇑f` and `⇑g` respectively) are equal, then `f` and `g` themselves are equal. This theorem essentially states that ring homomorphisms are injective with respect to their function application.
More concisely: If two ring homomorphisms between non-associative semirings have equal function applications, then they are equal.
|
RingHom.map_add'
theorem RingHom.map_add' :
∀ {α : Type u_5} {β : Type u_6} [inst : NonAssocSemiring α] [inst_1 : NonAssocSemiring β] (self : α →+* β)
(x y : α), self.toFun (x + y) = self.toFun x + self.toFun y
This theorem states that for any two types `α` and `β`, both with `NonAssocSemiring` structures, and any ring homomorphism from `α` to `β`, the ring homomorphism preserves addition. In other words, for any two elements `x` and `y` of type `α`, applying the ring homomorphism to their sum (`x + y`) is equivalent to applying the ring homomorphism to each element individually and then adding the results.
In terms of mathematical notation, for any ring homomorphism `f : α → β`, this theorem asserts the equality `f(x + y) = f(x) + f(y)`.
More concisely: For any ring homomorphisms between two types with `NonAssocSemiring` structures, the homomorphism preserves addition, that is, `f(x + y) = f(x) + f(y)` for all `x` and `y` in the first type.
|
RingHom.map_add
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
This theorem, named `RingHom.map_add`, states that for any two types `α` and `β` which are non-associative semirings, and for any ring homomorphism `f` from `α` to `β`, the homomorphism preserves the addition operation. More formally, for any two elements `a` and `b` of `α`, the image of their sum under `f` is equal to the sum of their individual images under `f`. In mathematical terms, for all `a, b` in `α`, `f(a + b) = f(a) + f(b)`. This property is one of the defining characteristics of a ring homomorphism.
More concisely: Given any ring homomorphism `f` between non-associative semirings `α` and `β`, `f(a + b) = f(a) + f(b)` for all `a, b` in `α`.
|
NonUnitalRingHom.ext
theorem NonUnitalRingHom.ext :
∀ {α : Type u_2} {β : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
⦃f g : α →ₙ+* β⦄, (∀ (x : α), f x = g x) → f = g
This theorem, `NonUnitalRingHom.ext`, states that for any types `α` and `β` that are NonUnitalNonAssocSemirings, if we have two non-unital ring homomorphisms `f` and `g` from `α` to `β`, and for every element `x` in `α` the application of `f` and `g` to `x` are equal, then the homomorphisms `f` and `g` themselves are equal. In short, two non-unital ring homomorphisms are equal if they produce the same result for every input from the domain.
More concisely: If `α` and `β` are NonUnitalNonAssocSemirings, and `f` and `g` are non-unital ring homomorphisms from `α` to `β` such that `f x = g x` for all `x` in `α`, then `f = g`.
|
RingHom.coe_comp
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
The theorem `RingHom.coe_comp` states that for any three non-associative semirings (which are types `α`, `β`, and `γ`), and for any given two ring homomorphisms - one from `β` to `γ` (`hnp`), and another from `α` to `β` (`hmn`), the composition of these two ring homomorphisms (obtained using `RingHom.comp`) coincides with the composition of the corresponding functions (`⇑hnp ∘ ⇑hmn`). In other words, the composition of ring homomorphisms is equivalent to the composition of their underlying functions.
More concisely: For any three semirings `α`, `β`, and `γ`, and given ring homomorphisms `hmn: α → β` and `hnp: β → γ`, `RingHom.comp hnp hmn = hnp ∘ hmn`.
|
RingHom.codomain_trivial_iff_range_trivial
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
The theorem `RingHom.codomain_trivial_iff_range_trivial` states that for all non-associative semirings `α` and `β`, and for any ring homomorphism `f` from `α` to `β`, the codomain `β` is trivial (i.e., it contains only one element, such that 0 equals 1) if and only if the range of `f` is also trivial (i.e., for every element `x` in `α`, the image under `f` is 0).
More concisely: A ring homomorphism from a non-associative semiring to a trivial ring is trivial if and only if its image of every element is zero.
|
RingHom.id_apply
theorem RingHom.id_apply : ∀ {α : Type u_2} {x : NonAssocSemiring α} (x_1 : α), (RingHom.id α) x_1 = x_1
The theorem `RingHom.id_apply` states that for any type `α` that forms a non-associative semiring and any element `x_1` of `α`, applying the identity ring homomorphism `RingHom.id α` to `x_1` results in `x_1` itself. In other words, the identity ring homomorphism does not change the value of an element in the semiring.
More concisely: For any semiring `α` and its identity homomorphism `RingHom.id α`, `RingHom.id α x_1 = x_1` for all `x_1 ∈ α`.
|
RingHom.coe_monoidHom_injective
theorem RingHom.coe_monoidHom_injective :
∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β},
Function.Injective fun f => ↑f
The theorem `RingHom.coe_monoidHom_injective` states that for any two types `α` and `β` (where `α` and `β` are non-associative semirings), the function that transforms a ring homomorphism into a monoid homomorphism (denoted as `f => ↑f`) is injective. This means that if two ring homomorphisms are mapped to the same monoid homomorphism, then they were originally the same ring homomorphism.
More concisely: If two ring homomorphisms between non-associative semirings result in the same monoid homomorphism, then they are equal as functions.
|
NonUnitalRingHom.ext_iff
theorem NonUnitalRingHom.ext_iff :
∀ {α : Type u_2} {β : Type u_3} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
{f g : α →ₙ+* β}, f = g ↔ ∀ (x : α), f x = g x
This theorem states that for any two non-unital ring homomorphisms `f` and `g` from a type `α` to a type `β`, where both `α` and `β` are non-unital, non-associative semirings, `f` is equal to `g` if and only if `f` and `g` map every element `x` in `α` to the same element in `β`. In other words, two such ring homomorphisms are equal if they behave the same way on every element of `α`.
More concisely: Two non-unital ring homomorphisms from a non-unital, non-associative semiring `α` to a non-unital semiring `β` are equal if and only if they map every element of `α` to the same image in `β`.
|
NonUnitalRingHom.map_zero'
theorem NonUnitalRingHom.map_zero' :
∀ {α : Type u_5} {β : Type u_6} [inst : NonUnitalNonAssocSemiring α] [inst_1 : NonUnitalNonAssocSemiring β]
(self : α →ₙ+* β), self.toFun 0 = 0
This theorem states that for any two types `α` and `β`, which are non-unital, non-associative semirings, any function `self` that is a non-unital ring homomorphism from `α` to `β` will map the element `0` in `α` to the element `0` in `β`. In other words, zero is preserved under the application of the function `self`.
More concisely: For any non-unital, non-associative semirings `α` and `β`, and any non-unital ring homomorphism `self` from `α` to `β`, `self (0α) = 0β`.
|
RingHom.comp_id
theorem RingHom.comp_id :
∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β),
f.comp (RingHom.id α) = f
This theorem states that for all types `α` and `β` with structures of non-associative semirings, and for any ring homomorphism `f` from `α` to `β`, the composition of `f` with the identity ring homomorphism on `α` is equal to `f`. This is essentially the mathematical principle that applying identity does not change the function.
More concisely: For any non-associative semirings `α` and `β`, and ring homomorphism `f` from `α` to `β`, the identity ring homomorphism on `α` and `f` commute, i.e., the composition of the identity homomorphism and `f` equals `f`.
|