Mathlib.RingTheory.Nilpotent.Defs

IsNilpotent definition

[Zero R] [Pow R ℕ] (x : R) : Prop

Full source

/-- An element is said to be nilpotent if some natural-number-power of it equals zero.

Note that we require only the bare minimum assumptions for the definition to make sense. Even
`MonoidWithZero` is too strong since nilpotency is important in the study of rings that are only
power-associative. -/
def IsNilpotent [Zero R] [Pow R ℕ] (x : R) : Prop :=
  ∃ n : ℕ, x ^ n = 0

Nilpotent element

Informal description

An element $ x $ of a type $ R $ with a zero element and a natural number power operation is called *nilpotent* if there exists a natural number $ n $ such that $ x^n = 0 $.

IsNilpotent.mk theorem

[Zero R] [Pow R ℕ] (x : R) (n : ℕ) (e : x ^ n = 0) : IsNilpotent x

Full source

theorem IsNilpotent.mk [Zero R] [Pow R ℕ] (x : R) (n : ℕ) (e : x ^ n = 0) : IsNilpotent x :=
  ⟨n, e⟩

Existence of Nilpotency Exponent Implies Nilpotence

Informal description

Given an element $x$ in a type $R$ with a zero element and a natural number power operation, if there exists a natural number $n$ such that $x^n = 0$, then $x$ is nilpotent.

isNilpotent_of_subsingleton theorem

[Zero R] [Pow R ℕ] [Subsingleton R] : IsNilpotent x

Full source

@[simp] lemma isNilpotent_of_subsingleton [Zero R] [Pow R ℕ] [Subsingleton R] : IsNilpotent x :=
  ⟨0, Subsingleton.elim _ _⟩

Nilpotency in Subsingleton Types

Informal description

In a type $R$ with a zero element and a natural number power operation, if $R$ is a subsingleton (i.e., all elements of $R$ are equal), then every element $x \in R$ is nilpotent.

IsNilpotent.zero theorem

[MonoidWithZero R] : IsNilpotent (0 : R)

Full source

@[simp] theorem IsNilpotent.zero [MonoidWithZero R] : IsNilpotent (0 : R) :=
  ⟨1, pow_one 0⟩

Zero is Nilpotent in Monoids with Zero

Informal description

In any monoid with zero $R$, the zero element $0$ is nilpotent.

not_isNilpotent_one theorem

[MonoidWithZero R] [Nontrivial R] : ¬IsNilpotent (1 : R)

Full source

theorem not_isNilpotent_one [MonoidWithZero R] [Nontrivial R] :
    ¬ IsNilpotent (1 : R) := fun ⟨_, H⟩ ↦ zero_ne_one (H.symm.trans (one_pow _))

Non-nilpotency of the multiplicative identity in nontrivial monoids with zero

Informal description

In a nontrivial monoid with zero $R$, the multiplicative identity $1$ is not nilpotent, i.e., there does not exist a natural number $n$ such that $1^n = 0$.

IsNilpotent.pow_succ theorem

(n : ℕ) {S : Type*} [MonoidWithZero S] {x : S} (hx : IsNilpotent x) : IsNilpotent (x ^ n.succ)

Full source

lemma IsNilpotent.pow_succ (n : ℕ) {S : Type*} [MonoidWithZero S] {x : S}
    (hx : IsNilpotent x) : IsNilpotent (x ^ n.succ) := by
  obtain ⟨N, hN⟩ := hx
  use N
  rw [← pow_mul, Nat.succ_mul, pow_add, hN, mul_zero]

Nilpotency of Successor Powers: $x^{n+1}$ is nilpotent when $x$ is nilpotent

Informal description

Let $S$ be a monoid with zero and let $x \in S$ be a nilpotent element. Then for any natural number $n$, the element $x^{n+1}$ is also nilpotent.

IsNilpotent.of_pow theorem

[MonoidWithZero R] {x : R} {m : ℕ} (h : IsNilpotent (x ^ m)) : IsNilpotent x

Full source

theorem IsNilpotent.of_pow [MonoidWithZero R] {x : R} {m : ℕ}
    (h : IsNilpotent (x ^ m)) : IsNilpotent x := by
  obtain ⟨n, h⟩ := h
  use m * n
  rw [← h, pow_mul x m n]

Nilpotency of Element Implies Nilpotency of its Power

Informal description

Let $R$ be a monoid with zero and let $x \in R$. If there exists a natural number $m$ such that $x^m$ is nilpotent, then $x$ itself is nilpotent.

IsNilpotent.pow_of_pos theorem

{n} {S : Type*} [MonoidWithZero S] {x : S} (hx : IsNilpotent x) (hn : n ≠ 0) : IsNilpotent (x ^ n)

Full source

lemma IsNilpotent.pow_of_pos {n} {S : Type*} [MonoidWithZero S] {x : S}
    (hx : IsNilpotent x) (hn : n ≠ 0) : IsNilpotent (x ^ n) := by
  cases n with
  | zero => contradiction
  | succ => exact IsNilpotent.pow_succ _ hx

Nilpotency of Positive Powers: $x^n$ is nilpotent for $n > 0$ when $x$ is nilpotent

Informal description

Let $S$ be a monoid with zero and let $x \in S$ be a nilpotent element. For any positive natural number $n$, the element $x^n$ is also nilpotent.

IsNilpotent.pow_iff_pos theorem

{n} {S : Type*} [MonoidWithZero S] {x : S} (hn : n ≠ 0) : IsNilpotent (x ^ n) ↔ IsNilpotent x

Full source

@[simp]
lemma IsNilpotent.pow_iff_pos {n} {S : Type*} [MonoidWithZero S] {x : S} (hn : n ≠ 0) :
    IsNilpotentIsNilpotent (x ^ n) ↔ IsNilpotent x :=
  ⟨of_pow, (pow_of_pos · hn)⟩

Nilpotency of Powers: $x^n$ nilpotent $\iff$ $x$ nilpotent for $n > 0$

Informal description

Let $S$ be a monoid with zero and let $x \in S$. For any nonzero natural number $n$, the element $x^n$ is nilpotent if and only if $x$ is nilpotent.

IsNilpotent.map theorem

 [MonoidWithZero R] [MonoidWithZero S] {r : R} {F : Type*} [FunLike F R S] [MonoidWithZeroHomClass F R S]
  (hr : IsNilpotent r) (f : F) : IsNilpotent (f r)

Full source

theorem IsNilpotent.map [MonoidWithZero R] [MonoidWithZero S] {r : R} {F : Type*}
    [FunLike F R S] [MonoidWithZeroHomClass F R S] (hr : IsNilpotent r) (f : F) :
    IsNilpotent (f r) := by
  use hr.choose
  rw [← map_pow, hr.choose_spec, map_zero]

Nilpotency is preserved under monoid-with-zero homomorphisms

Informal description

Let $R$ and $S$ be monoids with zero, and let $F$ be a type of homomorphisms from $R$ to $S$ that preserve the monoid-with-zero structure. If $r \in R$ is nilpotent and $f \in F$ is such a homomorphism, then the image $f(r)$ is nilpotent in $S$.

IsNilpotent.map_iff theorem

 [MonoidWithZero R] [MonoidWithZero S] {r : R} {F : Type*} [FunLike F R S] [MonoidWithZeroHomClass F R S] {f : F}
  (hf : Function.Injective f) : IsNilpotent (f r) ↔ IsNilpotent r

Full source

lemma IsNilpotent.map_iff [MonoidWithZero R] [MonoidWithZero S] {r : R} {F : Type*}
    [FunLike F R S] [MonoidWithZeroHomClass F R S] {f : F} (hf : Function.Injective f) :
    IsNilpotentIsNilpotent (f r) ↔ IsNilpotent r :=
  ⟨fun ⟨k, hk⟩ ↦ ⟨k, (map_eq_zero_iff f hf).mp <| by rwa [map_pow]⟩, fun h ↦ h.map f⟩

Nilpotency is preserved under injective monoid-with-zero homomorphisms

Informal description

Let $R$ and $S$ be monoids with zero, and let $F$ be a type of homomorphisms from $R$ to $S$ that preserve the monoid-with-zero structure. For an element $r \in R$ and an injective homomorphism $f \in F$, the image $f(r)$ is nilpotent in $S$ if and only if $r$ is nilpotent in $R$.

IsUnit.isNilpotent_mul_unit_of_commute_iff theorem

[MonoidWithZero R] {r u : R} (hu : IsUnit u) (h_comm : Commute r u) : IsNilpotent (r * u) ↔ IsNilpotent r

Full source

theorem IsUnit.isNilpotent_mul_unit_of_commute_iff [MonoidWithZero R] {r u : R}
    (hu : IsUnit u) (h_comm : Commute r u) :
    IsNilpotentIsNilpotent (r * u) ↔ IsNilpotent r :=
  exists_congr fun n ↦ by rw [h_comm.mul_pow, (hu.pow n).mul_left_eq_zero]

Nilpotency of Product with Unit: $r \cdot u$ is nilpotent iff $r$ is nilpotent

Informal description

Let $R$ be a monoid with zero, and let $r, u \in R$ such that $u$ is a unit and $r$ commutes with $u$. Then the product $r \cdot u$ is nilpotent if and only if $r$ is nilpotent.

IsUnit.isNilpotent_unit_mul_of_commute_iff theorem

[MonoidWithZero R] {r u : R} (hu : IsUnit u) (h_comm : Commute r u) : IsNilpotent (u * r) ↔ IsNilpotent r

Full source

theorem IsUnit.isNilpotent_unit_mul_of_commute_iff [MonoidWithZero R] {r u : R}
    (hu : IsUnit u) (h_comm : Commute r u) :
    IsNilpotentIsNilpotent (u * r) ↔ IsNilpotent r :=
  h_comm ▸ hu.isNilpotent_mul_unit_of_commute_iff h_comm

Nilpotency of Unit Multiplied by Commuting Element: $u \cdot r$ is nilpotent iff $r$ is nilpotent

Informal description

Let $R$ be a monoid with zero, and let $r, u \in R$ such that $u$ is a unit and $r$ commutes with $u$. Then the product $u \cdot r$ is nilpotent if and only if $r$ is nilpotent.

nilpotencyClass definition

: ℕ

Full source

/-- If `x` is nilpotent, the nilpotency class is the smallest natural number `k` such that
`x ^ k = 0`. If `x` is not nilpotent, the nilpotency class takes the junk value `0`. -/
noncomputable def nilpotencyClass : ℕ := sInf {k | x ^ k = 0}

Nilpotency class of an element

Informal description

For a nilpotent element $ x $ in a monoid with zero, the nilpotency class is the smallest natural number $ k $ such that $ x^k = 0 $. If $ x $ is not nilpotent, the nilpotency class is defined to be 0.

nilpotencyClass_eq_zero_of_subsingleton theorem

[Subsingleton R] : nilpotencyClass x = 0

Full source

@[simp] lemma nilpotencyClass_eq_zero_of_subsingleton [Subsingleton R] :
    nilpotencyClass x = 0 := by
  let s : Set ℕ := {k | x ^ k = 0}
  suffices s = univ by change sInf _ = 0; simp [s] at this; simp [this]
  exact eq_univ_iff_forall.mpr fun k ↦ Subsingleton.elim _ _

Nilpotency Class is Zero in Subsingleton Monoid

Informal description

In a monoid with zero $R$ that is a subsingleton (i.e., all elements are equal), the nilpotency class of any element $x$ is zero, i.e., $\text{nilpotencyClass}(x) = 0$.

isNilpotent_of_pos_nilpotencyClass theorem

(hx : 0 < nilpotencyClass x) : IsNilpotent x

Full source

lemma isNilpotent_of_pos_nilpotencyClass (hx : 0 < nilpotencyClass x) :
    IsNilpotent x := by
  let s : Set ℕ := {k | x ^ k = 0}
  change s.Nonempty
  change 0 < sInf s at hx
  by_contra contra
  simp [not_nonempty_iff_eq_empty.mp contra] at hx

Positivity of Nilpotency Class Implies Nilpotence

Informal description

If the nilpotency class of an element $x$ in a monoid with zero is positive (i.e., $\text{nilpotencyClass}(x) > 0$), then $x$ is nilpotent.

pow_nilpotencyClass theorem

(hx : IsNilpotent x) : x ^ (nilpotencyClass x) = 0

Full source

lemma pow_nilpotencyClass (hx : IsNilpotent x) : x ^ (nilpotencyClass x) = 0 :=
  Nat.sInf_mem hx

Nilpotent Element to Nilpotency Class Power Equals Zero

Informal description

For any nilpotent element $x$ in a monoid with zero, raising $x$ to the power of its nilpotency class yields zero, i.e., $x^{\text{nilpotencyClass}(x)} = 0$.

nilpotencyClass_eq_succ_iff theorem

{k : ℕ} : nilpotencyClass x = k + 1 ↔ x ^ (k + 1) = 0 ∧ x ^ k ≠ 0

Full source

lemma nilpotencyClass_eq_succ_iff {k : ℕ} :
    nilpotencyClassnilpotencyClass x = k + 1 ↔ x ^ (k + 1) = 0 ∧ x ^ k ≠ 0 := by
  let s : Set ℕ := {k | x ^ k = 0}
  have : ∀ k₁ k₂ : ℕ, k₁ ≤ k₂ → k₁ ∈ s → k₂ ∈ s := fun k₁ k₂ h_le hk₁ ↦ pow_eq_zero_of_le h_le hk₁
  simp [s, nilpotencyClass, Nat.sInf_upward_closed_eq_succ_iff this]

Characterization of Nilpotency Class: $\text{nilpotencyClass}(x) = k + 1 \leftrightarrow (x^{k+1} = 0 \land x^k \neq 0)$

Informal description

For any natural number $k$, the nilpotency class of an element $x$ in a monoid with zero is equal to $k + 1$ if and only if $x^{k + 1} = 0$ and $x^k \neq 0$.

nilpotencyClass_zero theorem

[Nontrivial R] : nilpotencyClass (0 : R) = 1

Full source

@[simp] lemma nilpotencyClass_zero [Nontrivial R] :
    nilpotencyClass (0 : R) = 1 :=
  nilpotencyClass_eq_succ_iff.mpr <| by constructor <;> simp

Nilpotency Class of Zero in Nontrivial Monoid is One

Informal description

In a nontrivial monoid with zero $R$, the nilpotency class of the zero element is $1$, i.e., $\text{nilpotencyClass}(0) = 1$.

pos_nilpotencyClass_iff theorem

[Nontrivial R] : 0 < nilpotencyClass x ↔ IsNilpotent x

Full source

@[simp] lemma pos_nilpotencyClass_iff [Nontrivial R] :
    0 < nilpotencyClass x ↔ IsNilpotent x := by
  refine ⟨isNilpotent_of_pos_nilpotencyClass, fun hx ↦ Nat.pos_of_ne_zero fun hx' ↦ ?_⟩
  replace hx := pow_nilpotencyClass hx
  rw [hx', pow_zero] at hx
  exact one_ne_zero hx

Positivity of Nilpotency Class Characterizes Nilpotent Elements

Informal description

Let $R$ be a nontrivial monoid with zero. For any element $x \in R$, the nilpotency class of $x$ is positive if and only if $x$ is nilpotent. In other words, $0 < \text{nilpotencyClass}(x) \leftrightarrow \exists n \in \mathbb{N}, x^n = 0$.

pow_pred_nilpotencyClass theorem

[Nontrivial R] (hx : IsNilpotent x) : x ^ (nilpotencyClass x - 1) ≠ 0

Full source

lemma pow_pred_nilpotencyClass [Nontrivial R] (hx : IsNilpotent x) :
    x ^ (nilpotencyClass x - 1) ≠ 0 :=
  (nilpotencyClass_eq_succ_iff.mp <| Nat.eq_add_of_sub_eq (pos_nilpotencyClass_iff.mpr hx) rfl).2

Non-vanishing of Nilpotent Element at Predicted Power

Informal description

Let $R$ be a nontrivial monoid with zero. For any nilpotent element $x \in R$, the element raised to the power of its nilpotency class minus one is nonzero, i.e., $x^{\text{nilpotencyClass}(x) - 1} \neq 0$.

nilpotencyClass_eq_one theorem

[Nontrivial R] : nilpotencyClass x = 1 ↔ x = 0

Full source

@[simp] lemma nilpotencyClass_eq_one [Nontrivial R] :
    nilpotencyClassnilpotencyClass x = 1 ↔ x = 0 :=
  ⟨eq_zero_of_nilpotencyClass_eq_one, fun hx ↦ hx ▸ nilpotencyClass_zero⟩

Nilpotency Class One Characterizes Zero Element in Nontrivial Monoid

Informal description

Let $R$ be a nontrivial monoid with zero. For any element $x \in R$, the nilpotency class of $x$ is equal to $1$ if and only if $x$ is the zero element, i.e., $\text{nilpotencyClass}(x) = 1 \leftrightarrow x = 0$.

IsReduced structure

(R : Type*) [Zero R] [Pow R ℕ]

Full source

/-- A structure that has zero and pow is reduced if it has no nonzero nilpotent elements. -/
@[mk_iff]
class IsReduced (R : Type*) [Zero R] [Pow R ℕ] : Prop where
  /-- A reduced structure has no nonzero nilpotent elements. -/
  eq_zero : ∀ x : R, IsNilpotent x → x = 0

Reduced structure

Informal description

A structure $(R, 0, \cdot^n)$ is called *reduced* if it has no nonzero nilpotent elements, i.e., for any $x \in R$ and $n \in \mathbb{N}$, if $x^n = 0$ then $x = 0$.

IsReduced.pow_eq_zero theorem

[Zero R] [Pow R ℕ] [IsReduced R] {n : ℕ} (h : x ^ n = 0) : x = 0

Full source

theorem pow_eq_zero [Zero R] [Pow R ℕ] [IsReduced R] {n : ℕ} (h : x ^ n = 0) :
    x = 0 := IsReduced.eq_zero x ⟨n, h⟩

Vanishing of Powers in Reduced Structures

Informal description

Let $R$ be a reduced structure with zero and power operations. For any element $x \in R$ and natural number $n$, if $x^n = 0$ then $x = 0$.

IsReduced.pow_eq_zero_iff theorem

[MonoidWithZero R] [IsReduced R] {n : ℕ} (hn : n ≠ 0) : x ^ n = 0 ↔ x = 0

Full source

@[simp]
theorem pow_eq_zero_iff [MonoidWithZero R] [IsReduced R] {n : ℕ} (hn : n ≠ 0) :
    x ^ n = 0 ↔ x = 0 := ⟨pow_eq_zero, fun h ↦ h.symm ▸ zero_pow hn⟩

Characterization of Nilpotency in Reduced Monoids: $x^n = 0 \leftrightarrow x = 0$ for $n \neq 0$

Informal description

Let $R$ be a reduced monoid with zero. For any nonzero natural number $n$ and any element $x \in R$, the $n$-th power of $x$ is zero if and only if $x$ is zero, i.e., $x^n = 0 \leftrightarrow x = 0$.

IsReduced.pow_ne_zero_iff theorem

[MonoidWithZero R] [IsReduced R] {n : ℕ} (hn : n ≠ 0) : x ^ n ≠ 0 ↔ x ≠ 0

Full source

theorem pow_ne_zero_iff [MonoidWithZero R] [IsReduced R] {n : ℕ} (hn : n ≠ 0) :
    x ^ n ≠ 0x ^ n ≠ 0 ↔ x ≠ 0 := not_congr (pow_eq_zero_iff hn)

Nonzero Powers in Reduced Monoids: $x^n \neq 0 \leftrightarrow x \neq 0$ for $n \neq 0$

Informal description

Let $R$ be a reduced monoid with zero. For any nonzero natural number $n$ and any element $x \in R$, the $n$-th power of $x$ is nonzero if and only if $x$ is nonzero, i.e., $x^n \neq 0 \leftrightarrow x \neq 0$.

IsReduced.pow_ne_zero theorem

[Zero R] [Pow R ℕ] [IsReduced R] (n : ℕ) (h : x ≠ 0) : x ^ n ≠ 0

Full source

theorem pow_ne_zero [Zero R] [Pow R ℕ] [IsReduced R] (n : ℕ) (h : x ≠ 0) :
    x ^ n ≠ 0 := fun H ↦ h (pow_eq_zero H)

Nonzero Elements Have Nonzero Powers in Reduced Structures

Informal description

Let $R$ be a reduced structure with zero and power operations. For any element $x \in R$ and natural number $n$, if $x$ is nonzero, then $x^n$ is also nonzero.

IsReduced.pow_eq_zero_iff' theorem

[MonoidWithZero R] [IsReduced R] [Nontrivial R] {n : ℕ} : x ^ n = 0 ↔ x = 0 ∧ n ≠ 0

Full source

/-- A variant of `IsReduced.pow_eq_zero_iff` assuming `R` is not trivial. -/
@[simp]
theorem pow_eq_zero_iff' [MonoidWithZero R] [IsReduced R] [Nontrivial R] {n : ℕ} :
    x ^ n = 0 ↔ x = 0 ∧ n ≠ 0 := by
  cases n <;> simp

Characterization of Zero Powers in Reduced Nontrivial Monoids

Informal description

Let $R$ be a nontrivial monoid with zero that is reduced. For any element $x \in R$ and natural number $n$, the power $x^n$ equals zero if and only if $x = 0$ and $n \neq 0$.

isReduced_of_noZeroDivisors instance

[MonoidWithZero R] [NoZeroDivisors R] : IsReduced R

Full source

instance (priority := 900) isReduced_of_noZeroDivisors [MonoidWithZero R] [NoZeroDivisors R] :
    IsReduced R :=
  ⟨fun _ ⟨_, hn⟩ => pow_eq_zero hn⟩

Monoids with No Zero Divisors are Reduced

Informal description

Every monoid with zero that has no zero divisors is reduced, meaning it has no nonzero nilpotent elements.

isReduced_of_subsingleton instance

[Zero R] [Pow R ℕ] [Subsingleton R] : IsReduced R

Full source

instance (priority := 900) isReduced_of_subsingleton [Zero R] [Pow R ℕ] [Subsingleton R] :
    IsReduced R :=
  ⟨fun _ _ => Subsingleton.elim _ _⟩

Subsingleton Monoids are Reduced

Informal description

Every subsingleton monoid with zero is reduced, meaning it has no nonzero nilpotent elements.

isNilpotent_iff_eq_zero theorem

[MonoidWithZero R] [IsReduced R] : IsNilpotent x ↔ x = 0

Full source

@[simp]
theorem isNilpotent_iff_eq_zero [MonoidWithZero R] [IsReduced R] : IsNilpotentIsNilpotent x ↔ x = 0 :=
  ⟨fun h => h.eq_zero, fun h => h.symm ▸ IsNilpotent.zero⟩

Characterization of Nilpotent Elements in Reduced Monoids: $x^n = 0 \iff x = 0$

Informal description

Let $R$ be a monoid with zero that is reduced (i.e., has no nonzero nilpotent elements). Then an element $x \in R$ is nilpotent if and only if $x = 0$.

isReduced_of_injective theorem

 [MonoidWithZero R] [MonoidWithZero S] {F : Type*} [FunLike F R S] [MonoidWithZeroHomClass F R S] (f : F)
  (hf : Function.Injective f) [IsReduced S] : IsReduced R

Full source

theorem isReduced_of_injective [MonoidWithZero R] [MonoidWithZero S] {F : Type*}
    [FunLike F R S] [MonoidWithZeroHomClass F R S]
    (f : F) (hf : Function.Injective f) [IsReduced S] :
    IsReduced R := by
  constructor
  intro x hx
  apply hf
  rw [map_zero]
  exact (hx.map f).eq_zero

Injective Monoid Homomorphisms Preserve Reduced Structure

Informal description

Let $R$ and $S$ be monoids with zero, and let $F$ be a type of homomorphisms from $R$ to $S$ that preserve the monoid-with-zero structure. Given an injective homomorphism $f \in F$ and assuming $S$ is reduced (i.e., has no nonzero nilpotent elements), then $R$ is also reduced.

instIsReducedForall instance

(ι) (R : ι → Type*) [∀ i, Zero (R i)] [∀ i, Pow (R i) ℕ] [∀ i, IsReduced (R i)] : IsReduced (∀ i, R i)

Full source

instance (ι) (R : ι → Type*) [∀ i, Zero (R i)] [∀ i, Pow (R i) ℕ]
    [∀ i, IsReduced (R i)] : IsReduced (∀ i, R i) where
  eq_zero _ := fun ⟨n, hn⟩ ↦ funext fun i ↦ IsReduced.eq_zero _ ⟨n, congr_fun hn i⟩

Product of Reduced Structures is Reduced

Informal description

For any family of types $(R_i)_{i \in \iota}$ where each $R_i$ is a reduced structure (i.e., has no nonzero nilpotent elements), the product type $\prod_{i \in \iota} R_i$ is also a reduced structure.

IsRadical definition

[Dvd R] [Pow R ℕ] (y : R) : Prop

Full source

/-- An element `y` in a monoid is radical if for any element `x`, `y` divides `x` whenever it
  divides a power of `x`. -/
def IsRadical [Dvd R] [Pow R ℕ] (y : R) : Prop :=
  ∀ (n : ℕ) (x), y ∣ x ^ n → y ∣ x

Radical element in a monoid

Informal description

An element $y$ in a monoid with a divisibility relation and a power operation is called *radical* if for every natural number $n$ and every element $x$, whenever $y$ divides $x^n$, it also divides $x$.

isRadical_iff_pow_one_lt theorem

[Monoid R] (k : ℕ) (hk : 1 < k) : IsRadical y ↔ ∀ x, y ∣ x ^ k → y ∣ x

Full source

theorem isRadical_iff_pow_one_lt [Monoid R] (k : ℕ) (hk : 1 < k) :
    IsRadicalIsRadical y ↔ ∀ x, y ∣ x ^ k → y ∣ x :=
  ⟨(· k), k.pow_imp_self_of_one_lt hk _ fun _ _ h ↦ .inl (dvd_mul_of_dvd_left h _)⟩

Characterization of Radical Elements via Powers: $y$ is radical $\iff$ ($y \mid x^k \implies y \mid x$) for $k > 1$

Informal description

Let $R$ be a monoid and $k$ a natural number with $k > 1$. An element $y \in R$ is *radical* if and only if for every $x \in R$, whenever $y$ divides $x^k$, it also divides $x$.

Commute.isNilpotent_mul_left theorem

(h_comm : Commute x y) (h : IsNilpotent x) : IsNilpotent (x * y)

Full source

theorem isNilpotent_mul_left (h_comm : Commute x y) (h : IsNilpotent x) : IsNilpotent (x * y) := by
  obtain ⟨n, hn⟩ := h
  use n
  rw [h_comm.mul_pow, hn, zero_mul]

Product with Nilpotent Element is Nilpotent under Commutativity (Left)

Informal description

Let $x$ and $y$ be elements in a multiplicative structure such that $x$ and $y$ commute (i.e., $x * y = y * x$). If $x$ is nilpotent (i.e., there exists a natural number $n$ such that $x^n = 0$), then the product $x * y$ is also nilpotent.

Commute.isNilpotent_mul_right theorem

(h_comm : Commute x y) (h : IsNilpotent y) : IsNilpotent (x * y)

Full source

theorem isNilpotent_mul_right (h_comm : Commute x y) (h : IsNilpotent y) : IsNilpotent (x * y) := by
  rw [h_comm.eq]
  exact h_comm.symm.isNilpotent_mul_left h

Product with Nilpotent Element is Nilpotent under Commutativity (Right)

Informal description

Let $x$ and $y$ be elements in a multiplicative structure such that $x$ and $y$ commute (i.e., $x * y = y * x$). If $y$ is nilpotent (i.e., there exists a natural number $n$ such that $y^n = 0$), then the product $x * y$ is also nilpotent.

Main definitions