pow_eq_zero_of_mem — Mathlib

English

If the n-th power of an ideal I is zero, and n ≤ m, then any x ∈ I satisfies x^m = 0.

Русский

Если n-я степень идеала I равна нулю, и n ≤ m, то для любого x ∈ I выполняется x^m = 0.

LaTeX

$$$ \\forall I : \\mathrm{Ideal}\\, R, \\forall n,m:\\mathbb{N}, (I^{n} = 0) \\wedge (n \\le m) \\Rightarrow \\forall x \\in I, x^{m} = 0$$$

Lean4

theorem pow_eq_zero_of_mem {I : Ideal R} {n m : ℕ} (hnI : I ^ n = 0) (hmn : n ≤ m) {x : R} (hx : x ∈ I) : x ^ m = 0 :=
  by simpa [hnI] using pow_le_pow_right hmn <| pow_mem_pow hx m

Похожие утверждения