map_eq_zero
theorem map_eq_zero :
∀ {M₀ : Type u_2} {G₀ : Type u_3} {F : Type u_6} [inst : MonoidWithZero M₀] [inst_1 : GroupWithZero G₀]
[inst_2 : Nontrivial M₀] [inst_3 : FunLike F G₀ M₀] [inst_4 : MonoidWithZeroHomClass F G₀ M₀] (f : F) {a : G₀},
f a = 0 ↔ a = 0
This theorem, `map_eq_zero`, states that for all types `M₀`, `G₀`, and `F`, given that `M₀` is a monoid with a zero element, `G₀` is a group with a zero element, `M₀` is nontrivial (has at least two distinct elements), `F` is a function-like from `G₀` to `M₀`, and `F` is a homomorphism from a monoid with a zero element to another monoid with zero, for any function `f` of type `F` and any element `a` of `G₀`, `f a` equals zero if and only if `a` equals zero. In less formal terms, this theorem states that under these conditions, a homomorphism from a group with zero to a monoid with zero sends an element to zero if and only if the element itself is zero.
More concisely: Given a homomorphism `F` from a group `G₀` with identity `e` to a monoid `M₀` with identity and zero `0`, if `F(e) = 0` and `F(a) = 0` for some `a` in `G₀`, then `a = e`.
|
Mathlib.Algebra.GroupWithZero.Units.Lemmas._auxLemma.1
theorem Mathlib.Algebra.GroupWithZero.Units.Lemmas._auxLemma.1 :
∀ {M₀ : Type u_2} {G₀ : Type u_3} {F : Type u_6} [inst : MonoidWithZero M₀] [inst_1 : GroupWithZero G₀]
[inst_2 : Nontrivial M₀] [inst_3 : FunLike F G₀ M₀] [inst_4 : MonoidWithZeroHomClass F G₀ M₀] (f : F) {a : G₀},
(f a = 0) = (a = 0)
This theorem states that for any types `M₀`, `G₀`, and `F`, given the conditions that `M₀` is a monoid with zero, `G₀` is a group with zero, `M₀` is nontrivial, `F` is a function-like structure from `G₀` to `M₀` obeying the rules of a monoid with zero homomorphism, and for any function `f` of type `F` and any element `a` of type `G₀`, the proposition that `f(a)` equals zero is equivalent to the proposition that `a` equals zero. Basically, it ensures that applying the function `f` to the zero element of `G₀` yields the zero element of `M₀`.
More concisely: If `F` is a monoid homomorphism from the group `G₀` with nontrivial identity to the monoid `M₀`, then `F(0) = 0`, where `0` denotes the zero elements in `G₀` and `M₀`.
|
map_inv₀
theorem map_inv₀ :
∀ {G₀ : Type u_3} {G₀' : Type u_5} {F : Type u_6} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero G₀']
[inst_2 : FunLike F G₀ G₀'] [inst_3 : MonoidWithZeroHomClass F G₀ G₀'] (f : F) (a : G₀), f a⁻¹ = (f a)⁻¹
The theorem `map_inv₀` states that for any two types `G₀` and `G₀'` representing groups with zeros, and a type `F` representing a function-like entity from `G₀` to `G₀'`, if there is an instance of `F` being a monoid homomorphism with zeros from `G₀` to `G₀'`, then the function `f` of type `F` maps the inverse of an element `a` in `G₀` to the inverse of `f a` in `G₀'`. In other words, under a monoid homomorphism that preserves the zero element, the inverse of an element in the original group maps to the inverse of its image in the target group.
More concisely: If `F` is a monoid homomorphism from group `G₀` to group `G₀'` preserving zeros, then `f(x⁻¹) = (f(x))⁻¹` for all `x` in `G₀`.
|
map_div₀
theorem map_div₀ :
∀ {G₀ : Type u_3} {G₀' : Type u_5} {F : Type u_6} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero G₀']
[inst_2 : FunLike F G₀ G₀'] [inst_3 : MonoidWithZeroHomClass F G₀ G₀'] (f : F) (a b : G₀),
f (a / b) = f a / f b
The theorem `map_div₀` states that for all types `G₀`, `G₀'`, and `F`, given that `G₀` and `G₀'` are groups with zero, the type `F` is a function-like from `G₀` to `G₀'`, and `F` is a class of monoids with zero homomorphism from `G₀` to `G₀'`, then for any function `f` of type `F` and any elements `a` and `b` of `G₀`, the function application of `f` on the division of `a` and `b` (i.e., `f (a / b)`) is equal to the division of the function application of `f` on `a` and on `b` (i.e., `f a / f b`). In other words, the homomorphism `f` preserves the division operation.
More concisely: Given groups with zero `G₀` and `G₀'`, a function-like `F` from `G₀` to `G₀'` that is a monoid homomorphism with zero, for all `a, b ∈ G₀`, `f (a / b) = f a / f b`.
|
map_ne_zero
theorem map_ne_zero :
∀ {M₀ : Type u_2} {G₀ : Type u_3} {F : Type u_6} [inst : MonoidWithZero M₀] [inst_1 : GroupWithZero G₀]
[inst_2 : Nontrivial M₀] [inst_3 : FunLike F G₀ M₀] [inst_4 : MonoidWithZeroHomClass F G₀ M₀] (f : F) {a : G₀},
f a ≠ 0 ↔ a ≠ 0
The theorem `map_ne_zero` states that for any types `M₀`, `G₀`, and `F` where `M₀` is a monoid with zero, `G₀` is a group with zero, and `M₀` is nontrivial (i.e., it has at least two distinct elements). If `F` is a type that behaves like a function from `G₀` to `M₀` (expressed by `FunLike F G₀ M₀`) and there exists a structure of a monoid with zero homomorphism from `G₀` to `M₀` over `F` (expressed by `MonoidWithZeroHomClass F G₀ M₀`), then for any function `f : F` and any element `a : G₀`, `f a` is nonzero if and only if `a` is nonzero. In other words, the function `f` will map nonzero elements of `G₀` to nonzero elements of `M₀` and zero elements to zero.
More concisely: If `F` is a function from a group `G₀` to a monoid `M₀` with zero, with a monoid homomorphism structure, then `F(a)` is nonzero if and only if `a` is nonzero.
|
Commute.div_eq_div_iff
theorem Commute.div_eq_div_iff :
∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a b c d : G₀},
Commute b d → b ≠ 0 → d ≠ 0 → (a / b = c / d ↔ a * d = c * b)
The theorem `Commute.div_eq_div_iff` states that for any type `G₀` which is a `GroupWithZero` (an algebraic structure that is both a group and a monoid with a zero element), and any four elements `a`, `b`, `c`, `d` of this type, if `b` and `d` commute (meaning `b * d = d * b`), and neither `b` nor `d` are the zero element, then the equality of the ratios `a / b` and `c / d` is equivalent to the equality of the products `a * d` and `c * b`. This is a generalized version of the mathematical statement that in a field, the fraction `a/b` equals `c/d` if and only if `a * d` equals `c * b`, extended to `GroupWithZero`.
More concisely: In a `GroupWithZero` type `G₀`, if `b` and `d` are non-zero commuting elements, then `a / b = c / d` if and only if `a * d = c * b`.
|
map_zpow₀
theorem map_zpow₀ :
∀ {F : Type u_8} {G₀ : Type u_9} {G₀' : Type u_10} [inst : GroupWithZero G₀] [inst_1 : GroupWithZero G₀']
[inst_2 : FunLike F G₀ G₀'] [inst_3 : MonoidWithZeroHomClass F G₀ G₀'] (f : F) (x : G₀) (n : ℤ),
f (x ^ n) = f x ^ n
This theorem states that if we have a monoid homomorphism `f` between two `GroupWithZero`s (which are groups with an additional zero element) and this homomorphism maps `0` to `0`, then for any integer `n` and any element `x` of the original `GroupWithZero`, the result of applying `f` to `x` raised to power `n` is equal to the result of first applying `f` to `x` and then raising the result to power `n`. In other words, the homomorphism `f` preserves exponentiation for integer exponents.
More concisely: If `f` is a homomorphism between two `GroupWithZero`s mapping `0` to `0`, then for all integers `n` and elements `x` in the original `GroupWithZero`, `f(x^n) = (f(x))^n`.
|