zeroLocus_singleton_pow — Mathlib

English

For a given f and n, if n > 0, then zeroLocus of {f^n} equals zeroLocus of {f}.

Русский

Для данного f и n, если n > 0, то нуль-множество {f^n} равно нуль-множество {f}.

LaTeX

$$$ \operatorname{zeroLocus}_{\mathcal{A}}(\{f^{n}\}) = \operatorname{zeroLocus}_{\mathcal{A}}(\{f\}) \quad \text{for } n>0 $$$

Lean4

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

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