mem_of_pow_mem — Mathlib

English

If r^n ∈ I for a prime ideal I and n > 0, then r ∈ I.

Русский

Если r^n ∈ I для простого идеала I и n > 0, то r ∈ I.

LaTeX

$$r^{n} \in I \Rightarrow r \in I \quad (n > 0)$$

Lean4

theorem mem_of_pow_mem {I : Ideal α} (hI : I.IsPrime) {r : α} (n : ℕ) (H : r ^ n ∈ I) : r ∈ I := by
  induction n with
  | zero =>
    rw [pow_zero] at H
    exact hI.one_notMem.elim H
  | succ n ih =>
    rw [pow_succ] at H
    exact Or.casesOn (hI.mem_or_mem H) ih id

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