IsRingHom.map_one
theorem IsRingHom.map_one :
∀ {α : Type u} {β : Type v} [inst : Ring α] [inst_1 : Ring β] {f : α → β}, IsRingHom f → f 1 = 1
This theorem states that for any two rings, denoted by Greek letters α and β, and for any function `f` from α to β that is a ring homomorphism, then `f` preserves the multiplicative identity. In other words, if we apply `f` to the number 1 in the first ring (α), it will map to the number 1 in the second ring (β).
More concisely: For any ring homomorphism `f` from ring α to ring β, `f(1α) = 1β`.
|
IsSemiringHom.to_isMonoidHom
theorem IsSemiringHom.to_isMonoidHom :
∀ {α : Type u} {β : Type v} [inst : Semiring α] [inst_1 : Semiring β] {f : α → β},
IsSemiringHom f → IsMonoidHom f
This theorem states that under the condition that the types 'α' and 'β' are semirings, for any function 'f' mapping from 'α' to 'β', if 'f' is a semiring homomorphism then 'f' is also a monoid homomorphism. In other words, every semiring homomorphism is also a monoid homomorphism in the context of semirings.
More concisely: If 'f' is a semiring homomorphism from semiring 'α' to semiring 'β', then 'f' is a monoid homomorphism from 'α' to 'β'.
|
IsSemiringHom.id
theorem IsSemiringHom.id : ∀ {α : Type u} [inst : Semiring α], IsSemiringHom id
This theorem states that the identity map is a semiring homomorphism for any semiring. In other words, if you have a semiring structure on some type, `α`, then the identity function, which maps every element of `α` to itself, preserves the operations of the semiring (addition and multiplication). This means that applying the identity map won't disrupt the algebraic properties that make your type a semiring.
More concisely: The identity function is a semiring homomorphism for any semiring.
|
IsSemiringHom.map_one
theorem IsSemiringHom.map_one :
∀ {α : Type u} {β : Type v} [inst : Semiring α] [inst_1 : Semiring β] {f : α → β}, IsSemiringHom f → f 1 = 1 := by
sorry
This theorem states that for any two semirings `α` and `β`, and any function `f` from `α` to `β`, if `f` is a semiring homomorphism, then `f` preserves the multiplicative identity. In other words, if `f` respects the structure of the semirings, then the image under `f` of the multiplicative identity in `α` is the multiplicative identity in `β`, i.e., `f(1)` is equal to `1`.
More concisely: If `f` is a semiring homomorphism from semiring `α` to semiring `β`, then `f(1) = 1` in `β`.
|
IsRingHom.to_isSemiringHom
theorem IsRingHom.to_isSemiringHom :
∀ {α : Type u} {β : Type v} [inst : Ring α] [inst_1 : Ring β] {f : α → β}, IsRingHom f → IsSemiringHom f
This theorem states that for any two types `α` and `β`, if these types are rings and there exists a function `f` from `α` to `β` which is a ring homomorphism, then `f` is also a semiring homomorphism. In simpler terms, any function that preserves the ring structure (addition, subtraction, multiplication) will also preserve the semiring structure (addition and multiplication).
More concisely: If `α` and `β` are types of rings and `f : α → β` is a ring homomorphism, then `f` is a semiring homomorphism.
|
IsRingHom.map_add
theorem IsRingHom.map_add :
∀ {α : Type u} {β : Type v} [inst : Ring α] [inst_1 : Ring β] {f : α → β},
IsRingHom f → ∀ (x y : α), f (x + y) = f x + f y
This theorem states that if `f` is a ring homomorphism from a ring `α` to another ring `β`, then `f` preserves the addition operation. That is, for any two elements `x` and `y` from the ring `α`, the image of the sum of `x` and `y` under `f` is the same as the sum of the images of `x` and `y` under `f`. In mathematical notation, this is often expressed as `f(x + y) = f(x) + f(y)`.
More concisely: If `f` is a ring homomorphism from a ring `α` to a ring `β`, then `f(x + y) = f(x) + f(y)` for all `x, y ∈ α`.
|
IsRingHom.map_mul
theorem IsRingHom.map_mul :
∀ {α : Type u} {β : Type v} [inst : Ring α] [inst_1 : Ring β] {f : α → β},
IsRingHom f → ∀ (x y : α), f (x * y) = f x * f y
This theorem states that if `f` is a ring homomorphism (as denoted by `IsRingHom f`), then `f` preserves multiplication. Specifically for any two elements `x` and `y` in the ring `α`, the value of `f` applied to the product `x * y` in ring `α` is equal to the product of `f x` and `f y` in the ring `β`. In other words, applying `f` after multiplying `x` and `y` is the same as multiplying `f(x)` and `f(y)`. This is a fundamental property of ring homomorphisms.
More concisely: If `f` is a ring homomorphism, then `f (x * y) = f x * f y` for all `x, y` in the ring `α`.
|
IsRingHom.map_zero
theorem IsRingHom.map_zero :
∀ {α : Type u} {β : Type v} [inst : Ring α] [inst_1 : Ring β] {f : α → β}, IsRingHom f → f 0 = 0
This theorem states that for any two types `α` and `β` that have a ring structure, any function `f` from `α` to `β` that is a ring homomorphism will map the zero element in `α` to the zero element in `β`. In other words, for all rings `α` and `β`, a ring homomorphism `f: α → β` ensures that `f(0) = 0`.
More concisely: For any ring homomorphisms f : α → β, f maps the additive identity of α to the additive identity of β.
|
IsSemiringHom.to_isAddMonoidHom
theorem IsSemiringHom.to_isAddMonoidHom :
∀ {α : Type u} {β : Type v} [inst : Semiring α] [inst_1 : Semiring β] {f : α → β},
IsSemiringHom f → IsAddMonoidHom f
This theorem states that for any two types `α` and `β` that are both semirings, any function `f` from `α` to `β` that is a semiring homomorphism is also an additive monoid homomorphism. In other words, if a function preserves the structure of a semiring (meaning it respects both addition and multiplication operations), it also preserves the structure of an additive monoid (meaning it respects addition and the presence of a zero element).
More concisely: If `f` is a semiring homomorphism from semiring `α` to semiring `β`, then `f` is an additive monoid homomorphism from `α` to `β`.
|
IsRingHom.id
theorem IsRingHom.id : ∀ {α : Type u} [inst : Ring α], IsRingHom id
This theorem states that the identity map is a ring homomorphism for any given ring. In other words, if you have a ring, defined over some type `α`, then the identity function, which maps each element to itself, preserves the ring operations (addition and multiplication).
More concisely: For any ring `α`, the identity function is a ring homomorphism.
|
IsSemiringHom.comp
theorem IsSemiringHom.comp :
∀ {α : Type u} {β : Type v} [inst : Semiring α] [inst_1 : Semiring β] {f : α → β},
IsSemiringHom f → ∀ {γ : Type u_1} [inst_2 : Semiring γ] {g : β → γ}, IsSemiringHom g → IsSemiringHom (g ∘ f)
This theorem states that if you have two semiring homomorphisms (functions that preserve the structure of semirings), then their composition is also a semiring homomorphism. In more detail, given two types `α` and `β` that are semirings, and a function `f` from `α` to `β` that is a semiring homomorphism, and another type `γ` that is a semiring, and a function `g` from `β` to `γ` that is a semiring homomorphism, the composition of `g` and `f` (denoted `g ∘ f`) is also a semiring homomorphism.
More concisely: If `f` is a semiring homomorphism from `α` to `β` and `g` is a semiring homomorphism from `β` to `γ`, then their composition `g ∘ f` is a semiring homomorphism from `α` to `γ`.
|
IsRingHom.map_neg
theorem IsRingHom.map_neg :
∀ {α : Type u} {β : Type v} [inst : Ring α] [inst_1 : Ring β] {f : α → β} {x : α}, IsRingHom f → f (-x) = -f x := by
sorry
This theorem states that ring homomorphisms preserve additive inverses. Specifically, for any two types `α` and `β` that are rings, and for any function `f` from `α` to `β` that is a ring homomorphism, the image under `f` of the additive inverse of any element `x` in `α` is equal to the additive inverse of the image of `x` under `f`. In mathematical term, if `f` is a ring homomorphism from a ring `α` to a ring `β`, then for all `x` in `α`, `f(-x) = -f(x)`.
More concisely: For any ring homomorphism `f` from a ring `α` to a ring `β`, `f(-x) = -f(x)` for all `x` in `α`.
|
IsRingHom.comp
theorem IsRingHom.comp :
∀ {α : Type u} {β : Type v} [inst : Ring α] [inst_1 : Ring β] {f : α → β},
IsRingHom f → ∀ {γ : Type u_1} [inst_2 : Ring γ] {g : β → γ}, IsRingHom g → IsRingHom (g ∘ f)
This theorem states that if you have two ring homomorphisms, one from a ring `α` to a ring `β` (represented by the function `f`), and another from ring `β` to a ring `γ` (represented by the function `g`), then the composition of `g` and `f` (i.e., `g ∘ f`) is also a ring homomorphism. In other words, the property of being a ring homomorphism is preserved under function composition. Here, ring homomorphism refers to a function between two rings that preserves the ring operations (addition and multiplication) and the multiplicative identity.
More concisely: If `f` is a ring homomorphism from `α` to `β` and `g` is a ring homomorphism from `β` to `γ`, then their composition `g ∘ f` is a ring homomorphism from `α` to `γ`.
|
IsSemiringHom.map_zero
theorem IsSemiringHom.map_zero :
∀ {α : Type u} {β : Type v} [inst : Semiring α] [inst_1 : Semiring β] {f : α → β}, IsSemiringHom f → f 0 = 0 := by
sorry
This theorem, `IsSemiringHom.map_zero`, states that if `f` is a semiring homomorphism (a function that preserves the algebraic structure of semirings) from a semiring `α` to another semiring `β`, then `f` preserves the additive identity. In other words, `f` maps the zero element in `α` to the zero element in `β`.
More concisely: If `f` is a semiring homomorphism from semiring `α` to semiring `β`, then `f(0Δ) = 0β`, where `0Δ` denotes the additive identity in `α` and `0β` denotes the additive identity in `β`.
|
IsSemiringHom.map_mul
theorem IsSemiringHom.map_mul :
∀ {α : Type u} {β : Type v} [inst : Semiring α] [inst_1 : Semiring β] {f : α → β},
IsSemiringHom f → ∀ (x y : α), f (x * y) = f x * f y
This theorem states that if `f` is a function from one semiring to another, specified by the types `α` and `β`, and if `f` is a semiring homomorphism, then `f` preserves the multiplication operation from the first semiring to the second. In other words, for any two elements `x` and `y` from the first semiring, the multiplication of the images of `x` and `y` under `f` (i.e., `f x * f y`) is the same as the image under `f` of the product of `x` and `y` (i.e., `f (x * y)`). This is an important property of semiring homomorphisms.
More concisely: If `f:` `α` `->` `β` is a semiring homomorphism, then `f (x * y) = f x * f y` for all `x, y` in `α`, where `*` denotes multiplication in both semirings.
|
IsSemiringHom.map_add
theorem IsSemiringHom.map_add :
∀ {α : Type u} {β : Type v} [inst : Semiring α] [inst_1 : Semiring β] {f : α → β},
IsSemiringHom f → ∀ (x y : α), f (x + y) = f x + f y
The theorem `IsSemiringHom.map_add` states that for any two types `α` and `β` that have a semiring structure, any function `f` from `α` to `β` that preserves the semiring structure (denoted as `IsSemiringHom f`), the function `f` also preserves addition. In other words, for any two elements `x` and `y` from the semiring `α`, the image of the sum under `f` equals the sum of the images under `f`, i.e., `f(x+y) = f(x) + f(y)`.
More concisely: Given two semiring types `α` and `β` and a semiring homomorphism `f` from `α` to `β`, `f(x + y) = f(x) + f(y)` for all `x, y ∈ α`.
|
IsRingHom.of_semiring
theorem IsRingHom.of_semiring :
∀ {α : Type u} {β : Type v} [inst : Ring α] [inst_1 : Ring β] {f : α → β}, IsSemiringHom f → IsRingHom f
This theorem states that if we have a function `f` that maps one ring `α` to another ring `β`, and if this function is a semiring homomorphism (meaning it preserves the operations and properties of a semiring), then it is also a ring homomorphism. In other words, not only does `f` preserve the operations of addition and multiplication and the existence of an additive identity and a multiplicative identity, but it also preserves the additive inverse property of a ring.
More concisely: If `f` is a semiring homomorphism from a semiring `α` to a ring `β`, then `f` is a ring homomorphism.
|
IsRingHom.map_sub
theorem IsRingHom.map_sub :
∀ {α : Type u} {β : Type v} [inst : Ring α] [inst_1 : Ring β] {f : α → β} {x y : α},
IsRingHom f → f (x - y) = f x - f y
This theorem states that for any given ring homomorphism `f` from a ring `α` to another ring `β`, the subtraction operation is preserved. That is, if you subtract two elements `x` and `y` in the first ring and then apply the homomorphism, you get the same result as if you first apply the homomorphism to each element and then subtract the results. In formal terms, `f(x - y) = f(x) - f(y)` for all `x` and `y` in `α`.
More concisely: For any ring homomorphism `f` and elements `x` and `y` in a ring `α`, `f(x - y) = f(x) - f(y)`.
|