mul_cancel_right_mem_nonZeroDivisors
theorem mul_cancel_right_mem_nonZeroDivisors :
∀ {R : Type u_5} [inst : Ring R] {x y r : R}, r ∈ nonZeroDivisors R → (x * r = y * r ↔ x = y)
This theorem states that for any ring 'R', and any elements 'x', 'y', and 'r' of 'R', if 'r' belongs to the submonoid of non-zero divisors of 'R', then 'x' times 'r' equals 'y' times 'r' if and only if 'x' equals 'y'. In simpler terms, the theorem says that if 'r' is in the set of non-zero divisors, then multiplication by 'r' from the right side can be 'cancelled' without changing the equality of 'x' and 'y'. In other words, it states the cancellation property for multiplication in a ring when the multiplicative factor is a non-zero divisor.
More concisely: For any ring 'R' and elements 'x', 'y' of 'R', if 'r' is a non-zero divisor in 'R' then x * r = y * r implies x = y.
|
mem_nonZeroDivisors_iff
theorem mem_nonZeroDivisors_iff :
∀ {M : Type u_2} [inst : MonoidWithZero M] {r : M}, r ∈ nonZeroDivisors M ↔ ∀ (x : M), x * r = 0 → x = 0
This theorem, `mem_nonZeroDivisors_iff`, states that for any type `M` which has an instance of `MonoidWithZero` and any element `r` of this `M`, `r` is a member of the submonoid of non-zero divisors of `M` if and only if for every `x` in `M`, the multiplication of `x` and `r` yielding zero implies `x` itself is zero. In terms of algebra, it describes the condition under which an element belongs to the set of non-zero divisors in a monoid with zero.
More concisely: An element `r` of a monoid `M` with zero is a non-zero divisor if and only if for all `x` in `M`, `x * r = 0` implies `x = 0`.
|
eq_zero_of_ne_zero_of_mul_left_eq_zero
theorem eq_zero_of_ne_zero_of_mul_left_eq_zero :
∀ {M : Type u_2} [inst : MonoidWithZero M] [inst_1 : NoZeroDivisors M] {x y : M}, x ≠ 0 → x * y = 0 → y = 0 := by
sorry
This theorem states that for any type `M` that forms a monoid with zero and has no zero divisors, given two elements `x` and `y` of this type, if `x` is not zero and the product of `x` and `y` is zero, then `y` must be zero. In simpler terms, in a system where no product of two non-zero elements can be zero, if a non-zero element multiplies with another element resulting in zero, then the second element must have been zero.
More concisely: In a monoid with no zero divisors, the product of two non-zero elements is non-zero.
|
nonZeroDivisors.ne_zero
theorem nonZeroDivisors.ne_zero :
∀ {M : Type u_2} [inst : MonoidWithZero M] [inst_1 : Nontrivial M] {x : M}, x ∈ nonZeroDivisors M → x ≠ 0 := by
sorry
This theorem states that for any type `M` that forms a `MonoidWithZero` (which is a monoid with an additional zero element) and is `Nontrivial` (meaning it has at least two distinct elements), any element `x` of `M` that belongs to the submonoid of non-zero-divisors (an element is a non-zero-divisor if when it multiplies any other element results in zero, then that other element must be zero) is not equal to zero.
More concisely: In a MonoidWithZero `M` with at least two distinct elements, every non-zero non-zero-divisor belongs to `M\backslash {0}`.
|
zero_not_mem_nonZeroDivisors
theorem zero_not_mem_nonZeroDivisors :
∀ {M : Type u_2} [inst : MonoidWithZero M] [inst_1 : Nontrivial M], 0 ∉ nonZeroDivisors M
The theorem `zero_not_mem_nonZeroDivisors` states that for any `MonoidWithZero` `M` which is nontrivial, the element 0 does not belong to the submonoid of non-zero-divisors of `M`. In other words, in a nontrivial monoid with zero, zero cannot be a non-zero-divisor, which is consistent with the mathematical expectation since multiplying any number by zero results in zero.
More concisely: In a nontrivial MonoidWithZero, the zero element is not a non-zero divisor.
|
eq_zero_of_ne_zero_of_mul_right_eq_zero
theorem eq_zero_of_ne_zero_of_mul_right_eq_zero :
∀ {M : Type u_2} [inst : MonoidWithZero M] [inst_1 : NoZeroDivisors M] {x y : M}, x ≠ 0 → y * x = 0 → y = 0 := by
sorry
This theorem states that for any type `M` that is a `MonoidWithZero` and `NoZeroDivisors`, given two elements `x` and `y` of this type, if `x` is not zero and the product of `y` and `x` is zero, then `y` must be zero. In plain language, in a multiplication scenario where we have non-zero divisors and the product with a non-zero number results in zero, the other factor must be zero.
More concisely: If `M` is a `MonoidWithZero` and `NoZeroDivisors` type, then for all non-zero `x` in `M`, if `x * y = 0`, then `y = 0`.
|
Mathlib.Algebra.GroupWithZero.NonZeroDivisors._auxLemma.2
theorem Mathlib.Algebra.GroupWithZero.NonZeroDivisors._auxLemma.2 :
∀ (M₀ : Type u_1) [inst : MonoidWithZero M₀] {x : M₀},
(x ∈ nonZeroDivisorsRight M₀) = ∀ (y : M₀), x * y = 0 → y = 0
This theorem states that for any `MonoidWithZero` M₀ and for any element `x` of M₀, `x` belongs to the set of non-right-zero-divisors if and only if for every element `y` of M₀, the product of `x` and `y` equalling zero implies `y` equals zero. This theorem essentially defines what it means for an element to not be a right zero divisor in a `MonoidWithZero`. In the language of algebra, it says that in a monoid with zero, an element is a non-right-zero-divisor if it doesn't make any other non-zero element zero by right multiplication.
More concisely: An element of a `MonoidWithZero` is a non-right-zero-divisor if and only if it does not make any non-zero element zero by right multiplication.
|
map_ne_zero_of_mem_nonZeroDivisors
theorem map_ne_zero_of_mem_nonZeroDivisors :
∀ {M : Type u_2} {M' : Type u_3} {F : Type u_7} [inst : MonoidWithZero M] [inst_1 : MonoidWithZero M']
[inst_2 : FunLike F M M'] [inst_3 : Nontrivial M] [inst_4 : ZeroHomClass F M M'] (g : F),
Function.Injective ⇑g → ∀ {x : M}, x ∈ nonZeroDivisors M → g x ≠ 0
The theorem `map_ne_zero_of_mem_nonZeroDivisors` states that for any types `M` and `M'` that form monoids with zero (i.e., they are monoids that also have a zero element), a function `g` of type `F` that is a function-like mapping from `M` to `M'` and is injective, if `x` is a member of the non-zero-divisors of `M`, then the result of applying `g` to `x` must not be zero. This essentially says that the action of `g` preserves the property of being a non-zero-divisor under certain conditions. This theorem is important in the field of ring theory and algebra where non-zero-divisors play a crucial role.
More concisely: If `M` and `M'` are monoids with zero and `g : M -> M'` is an injective function-like mapping, then for every non-zero-divisor `x` in `M`, `g x` is non-zero in `M'`.
|
mem_nonZeroDivisors_of_ne_zero
theorem mem_nonZeroDivisors_of_ne_zero :
∀ {M : Type u_2} [inst : MonoidWithZero M] [inst_1 : NoZeroDivisors M] {x : M}, x ≠ 0 → x ∈ nonZeroDivisors M := by
sorry
This theorem states that for any MonoidWithZero `M` (a type of mathematical structure that combines the features of a group with zero and a monoid) and given that `M` has no zero divisors (no pair of non-zero elements that multiply to zero), if `x` is an element of `M` and `x` is not zero, then `x` belongs to the submonoid of non-zero divisors of `M`. In simple words, any non-zero element in a monoid with zero and no zero divisors is a non-zero divisor.
More concisely: In a MonoidWithZero without zero divisors, every non-zero element is a non-zero divisor.
|
nonZeroDivisors.coe_ne_zero
theorem nonZeroDivisors.coe_ne_zero :
∀ {M : Type u_2} [inst : MonoidWithZero M] [inst_1 : Nontrivial M] (x : ↥(nonZeroDivisors M)), ↑x ≠ 0
This theorem states that for any `MonoidWithZero` M that is `Nontrivial` (i.e., it has at least two distinct elements), all elements x of the submonoid of non-zero divisors of M are non-zero. Here, `nonZeroDivisors` is a submonoid of M consisting of elements x such that if z multiplied by x equals 0, then z must be 0. The notation `↑x` represents the process of coercing (or translating) x from the submonoid back to the original monoid M. Thus, the theorem asserts that no element of the non-zero divisors can be zero in the context of the monoid M.
More concisely: In any nontrivial MonoidWithZero M, all elements in the submonoid of non-zero divisors are non-zero.
|
nonZeroDivisors_le_comap_nonZeroDivisors_of_injective
theorem nonZeroDivisors_le_comap_nonZeroDivisors_of_injective :
∀ {M : Type u_2} {M' : Type u_3} {F : Type u_7} [inst : MonoidWithZero M] [inst_1 : MonoidWithZero M']
[inst_2 : FunLike F M M'] [inst_3 : NoZeroDivisors M'] [inst_4 : MonoidWithZeroHomClass F M M'] (f : F),
Function.Injective ⇑f → nonZeroDivisors M ≤ Submonoid.comap f (nonZeroDivisors M')
This theorem states that for all structures `M` and `M'` of type `Type`, where `M` and `M'` are monoids with zero, and for all structures `F` of type `Type` that behave functionally from `M` to `M'` (i.e., `F` is a monoid homomorphism from `M` to `M'`), if `f` is an injective function of type `F` and `M'` has no zero divisors, then the submonoid of non-zero divisors of `M` is a subset of or equal to the preimage of the submonoid of non-zero divisors of `M'` under the function `f`. In other words, if two elements of `M` have the same image in `M'` under `f`, and `M'` does not have zero divisors, then those two elements must be the same in `M`.
More concisely: If `M` and `M'` are monoids with zero, `F : M → M'` is a monoid homomorphism, `f : F → M'` is an injection, and `M'` has no zero divisors, then the preimage of the submonoid of non-zero divisors of `M'` under `f` is contained in the submonoid of non-zero divisors of `M`.
|
mem_nonZeroDivisors_iff_ne_zero
theorem mem_nonZeroDivisors_iff_ne_zero :
∀ {M : Type u_2} [inst : MonoidWithZero M] [inst_1 : NoZeroDivisors M] [inst_2 : Nontrivial M] {x : M},
x ∈ nonZeroDivisors M ↔ x ≠ 0
The theorem `mem_nonZeroDivisors_iff_ne_zero` states that for any given type `M` equipped with `MonoidWithZero`, `NoZeroDivisors`, and `Nontrivial` structures, an element `x` of type `M` is in the submonoid of non-zero-divisors of `M` if and only if `x` is not equal to zero. In other words, in such a structure, an element is a non-zero divisor if and only if it is not the zero element.
More concisely: An element x of a monoid M equipped with MonoidWithZero, NoZeroDivisors, and Nontrivial structures is a non-zero divisor if and only if x ≠ 0.
|
mul_cancel_left_mem_nonZeroDivisors
theorem mul_cancel_left_mem_nonZeroDivisors :
∀ {R' : Type u_6} [inst : CommRing R'] {x y r : R'}, r ∈ nonZeroDivisors R' → (r * x = r * y ↔ x = y)
The theorem `mul_cancel_left_mem_nonZeroDivisors` states that for any type `R'` which forms a commutative ring, given any elements `x`, `y`, and `r` of `R'`, if `r` belongs to the set of non-zero divisors of `R'`, then the equality of the products `r * x` and `r * y` implies the equality of `x` and `y`. In other words, multiplication by `r` is cancellable on the left within the set of non-zero divisors of a commutative ring.
More concisely: If `r` is a non-zero divisor in a commutative ring `R'`, then `r * x = r * y` implies `x = y`.
|
mul_right_mem_nonZeroDivisors_eq_zero_iff
theorem mul_right_mem_nonZeroDivisors_eq_zero_iff :
∀ {M : Type u_2} [inst : MonoidWithZero M] {x r : M}, r ∈ nonZeroDivisors M → (x * r = 0 ↔ x = 0)
The theorem `mul_right_mem_nonZeroDivisors_eq_zero_iff` asserts that for any type `M` which has a structure of a `MonoidWithZero`, and for any two elements `x` and `r` of `M`, if `r` is a member of the submonoid of non-zero-divisors of `M`, then the product `x * r` equals zero if and only if `x` equals zero.
In other words, this theorem states that within a monoid with zero, when we multiply any element `x` by a non-zero-divisor `r`, the result will be zero only if `x` itself is zero.
More concisely: In a monoid with zero, if a non-zero-divisor `r` is multiplied with any element `x`, then their product is zero if and only if `x` is zero.
|
nonZeroSMulDivisors_mulOpposite_eq_op_nonZeroDivisors
theorem nonZeroSMulDivisors_mulOpposite_eq_op_nonZeroDivisors :
∀ (R : Type u_2) [inst : MonoidWithZero R], nonZeroSMulDivisors Rᵐᵒᵖ R = (nonZeroDivisors R).op
This theorem states that for any `MonoidWithZero` `R`, the set of non-zero '•'-divisors, where '•' stands for a right multiplication operation, corresponds to the set of non-zero divisors of `R`. The `MulOpposite` form of `R` is used because the non-zero divisors were defined with right multiplication. In other words, the elements of `R` that do not lead to a zero result when right-multiplied by any non-zero element of `R` are the same as the elements of `R` that do not lead to a zero result when left-multiplied by any non-zero element of `R`.
More concisely: For any MonoidWithZero R, the set of elements that do not make any non-zero element of R multiplied from the right result in zero is equal to the set of elements that do not make any non-zero element of R multiplied from the left result in zero.
|