zeroLocus_singleton_pow — Mathlib

English

For any f and n>0, the zero locus of {f^n} equals the zero locus of {f}:

Русский

Для любого элемента f и n>0 нулевой локус {f^n} равен нулевому локусу {f}:

LaTeX

$$$\\mathrm{zeroLocus}({f^{n}}) = \\mathrm{zeroLocus}({f}) \\quad (n > 0).$$$

Lean4

@[simp]
theorem zeroLocus_singleton_pow (f : R) (n : ℕ) (hn : 0 < n) : zeroLocus ({f ^ n} : Set R) = zeroLocus { f } :=
  Set.ext fun x => by simpa using x.2.pow_mem_iff_mem n hn

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