Commute.isNilpotent_mul_left
theorem Commute.isNilpotent_mul_left :
∀ {R : Type u_1} {x y : R} [inst : Semiring R], Commute x y → IsNilpotent x → IsNilpotent (x * y)
The theorem states that if two elements `x` and `y` of a given semiring `R` commute, and if the element `x` is nilpotent, then the product `x * y` is also nilpotent. In other words, if the multiplication operation between `x` and `y` is commutative (i.e., `x * y = y * x`) and there exists a natural number `n` such that `x` raised to the power `n` equals zero, then there also exists a natural number for which the power of the product `x * y` equals zero.
More concisely: If `x` and `y` are commuting elements of a semiring, and `x` is nilpotent, then `x * y` is nilpotent.
|
IsNilpotent.map
theorem IsNilpotent.map :
∀ {R : Type u_1} {S : Type u_2} [inst : MonoidWithZero R] [inst_1 : MonoidWithZero S] {r : R} {F : Type u_3}
[inst_2 : FunLike F R S] [inst_3 : MonoidWithZeroHomClass F R S], IsNilpotent r → ∀ (f : F), IsNilpotent (f r)
The theorem `IsNilpotent.map` states that given two types `R` and `S` that are both monoids with zero, an object `r` of type `R`, and a function-like object `f` of type `F` that maps from `R` to `S`, if `r` is a nilpotent element in `R` (i.e., there exists a natural number `n` such that `r` raised to the power `n` equals zero), then `f(r)` is also a nilpotent element in `S`. Essentially, the nilpotency property is preserved under the map `f`.
More concisely: If `r` is a nilpotent element in the monoid `(R, ∘)` with zero, then `f(r)` is a nilpotent element in the monoid `(S, ∘)` with zero, where `f : R → S` is a function-like object.
|
isRadical_iff_pow_one_lt
theorem isRadical_iff_pow_one_lt :
∀ {R : Type u_1} {y : R} [inst : MonoidWithZero R] (k : ℕ), 1 < k → (IsRadical y ↔ ∀ (x : R), y ∣ x ^ k → y ∣ x)
The theorem `isRadical_iff_pow_one_lt` states that for any type `R` that is a monoid with zero, and any element `y` from `R`, and any natural number `k` greater than 1, `y` is a radical if and only if for any element `x` from `R`, whenever `y` divides `x` raised to the power `k`, `y` divides `x`. A radical element in this context is defined as an element that divides another whenever it can divide a power of the other.
More concisely: For any monoid with zero `R` and `y` in `R` with `k` a natural number greater than 1, `y` is a radical if and only if for all `x` in `R`, `y` divides `x^k` implies `y` divides `x`.
|
IsNilpotent.eq_zero
theorem IsNilpotent.eq_zero :
∀ {R : Type u_1} {x : R} [inst : Zero R] [inst_1 : Pow R ℕ] [inst_2 : IsReduced R], IsNilpotent x → x = 0 := by
sorry
This theorem states that for any type `R` that has a zero element, an exponentiation operation, and satisfies the property of being 'reduced' (i.e., having no non-zero nilpotent elements), if an element `x` of `R` is nilpotent (meaning there exists a natural number `n` such that `x` to the power `n` equals zero), then that element `x` must be zero.
More concisely: In a reduced ring with zero multiplicative identity and exponentiation operation, every nilpotent element is the additive identity.
|
IsReduced.eq_zero
theorem IsReduced.eq_zero :
∀ {R : Type u_3} [inst : Zero R] [inst_1 : Pow R ℕ] [self : IsReduced R] (x : R), IsNilpotent x → x = 0
The theorem `IsReduced.eq_zero` states that in a reduced mathematical structure, there are no nonzero nilpotent elements. In other words, for any element `x` of a type `R` that is reduced (i.e., has the `IsReduced` property), if `x` is nilpotent (meaning there exists a natural number `n` such that `x^n` equals zero), then `x` itself must be zero. This theorem is important in the study of algebraic structures like rings and fields, where the concept of 'reducedness' and 'nilpotency' play key roles.
More concisely: In a reduced mathematical structure, every nilpotent element is the additive identity (zero).
|
Commute.isNilpotent_mul_right
theorem Commute.isNilpotent_mul_right :
∀ {R : Type u_1} {x y : R} [inst : Semiring R], Commute x y → IsNilpotent y → IsNilpotent (x * y)
The theorem `Commute.isNilpotent_mul_right` states that for any semiring `R` and any two elements `x` and `y` of `R`, if `x` and `y` commute (i.e., `x * y = y * x`) and `y` is nilpotent (i.e., there exists a natural number `n` such that `y^n = 0`), then the product `x * y` is also nilpotent. This means, in the context of algebra, that if multiplication of two elements `x` and `y` is commutative and one of them annihilates to zero when raised to some power, their multiplication will also annihilate to zero when raised to some power.
More concisely: If `x` and `y` are commuting elements in a semiring with `y` being nilpotent, then `x * y` is also nilpotent.
|