zeroLocus_pow — Mathlib

English

For any ideal I and any nonzero exponent n, the zero locus of I^n equals the zero locus of I:

Русский

Для идеала I и любого ненулевого показателя n нулевой локус I^n совпадает с нулевым локусом I:

LaTeX

$$$\\mathrm{zeroLocus}(I^{n}) = \\mathrm{zeroLocus}(I) \\quad (n \\neq 0).$$$

Lean4

@[simp]
theorem zeroLocus_pow (I : Ideal R) {n : ℕ} (hn : n ≠ 0) : zeroLocus ((I ^ n : Ideal R) : Set R) = zeroLocus I :=
  zeroLocus_radical (I ^ n) ▸ (I.radical_pow hn).symm ▸ zeroLocus_radical I

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