RingHom.isUnit_map
theorem RingHom.isUnit_map :
∀ {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : Semiring β] (f : α →+* β) {a : α},
IsUnit a → IsUnit (f a)
This theorem states that for any given types `α` and `β`, with `α` and `β` being semirings, and for a ring homomorphism `f` from `α` to `β`, if an element `a` from `α` is a unit, then the image of `a` under `f` is also a unit in `β`. In mathematical terms, this means that if `a` in a semiring `α` has a multiplicative inverse, then its image under a ring homomorphism `f` in semiring `β` also has a multiplicative inverse.
More concisely: If `f` is a ring homomorphism from semiring `α` to semiring `β`, and `a` in `α` is a unit, then `f(a)` is a unit in `β`.
|
RingHom.map_dvd
theorem RingHom.map_dvd :
∀ {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : Semiring β] (f : α →+* β) {a b : α},
a ∣ b → f a ∣ f b
This theorem states that for any two types `α` and `β` where both are instances of a semiring, and a `RingHom` (ring homomorphism) `f` from `α` to `β`, if `a` divides `b` (denoted as `a ∣ b`) in the semiring `α`, then `f(a)` divides `f(b)` in the semiring `β`. In simpler terms, this theorem asserts that if `a` is a factor of `b`, then the image of `a` under a ring homomorphism is a factor of the image of `b` under the same ring homomorphism.
More concisely: Given two semirings `α` and `β`, any `RingHom` `f` from `α` to `β`, and `a ∈ α` dividing `b ∈ α`, then `f(a)` divides `f(b)` in `β`.
|
RingHom.codomain_trivial_iff_range_eq_singleton_zero
theorem RingHom.codomain_trivial_iff_range_eq_singleton_zero :
∀ {α : Type u_2} {β : Type u_3} {x : NonAssocSemiring α} {x_1 : NonAssocSemiring β} (f : α →+* β),
0 = 1 ↔ Set.range ⇑f = {0}
This theorem states that for any non-associative semiring, represented as `NonAssocSemiring`, with elements from types `α` and `β`, and for a ring homomorphism `f` from `α` to `β`, the codomain of `f` is trivial, meaning the zero and one elements are the same (`0 = 1`), if and only if the range of `f` is the singleton set containing only the zero element. In other words, a ring homomorphism has a trivial codomain if and only if all elements in the domain are mapped to zero in the codomain.
More concisely: A ring homomorphism from a non-associative semiring to another semiring has a trivial codomain if and only if it maps all elements to the zero element in the codomain.
|
Function.Injective.isDomain
theorem Function.Injective.isDomain :
∀ {α : Type u_2} {β : Type u_3} [inst : Ring α] [inst_1 : IsDomain α] [inst_2 : Ring β] (f : β →+* α),
Function.Injective ⇑f → IsDomain β
The theorem `Function.Injective.isDomain` states that for any types `α` and `β` where `α` is a ring and an integral domain, and `β` is a ring, if there exists a ring homomorphism function `f` from `β` to `α` which is injective, then `β` is also an integral domain. In other words, the property of being an integral domain (i.e., a nonzero commutative ring in which the product of any two nonzero elements is nonzero) can be pulled back along an injective ring homomorphism.
More concisely: If `f` is an injective ring homomorphism from an integral domain `β` to a ring `α` (where `α` is also an integral domain), then `β` is an integral domain.
|