pow_mem_of_mem — Mathlib

English

If a is in an ideal I, then all positive powers a^n with n > 0 also lie in I.

Русский

Если элемент a принадлежит идеалу I, то и все положительные степени a^n принадлежат I для n > 0.

LaTeX

$$$\forall I\; (I: \text{Ideal } \alpha) \; \forall a \in \alpha, \forall n \in \mathbb{N}, \; n > 0 \Rightarrow a^n \in I.$$$

Lean4

theorem pow_mem_of_mem (ha : a ∈ I) (n : ℕ) (hn : 0 < n) : a ^ n ∈ I :=
  Nat.casesOn n (Not.elim (by decide)) (fun m _hm => (pow_succ a m).symm ▸ I.mul_mem_left (a ^ m) ha) hn

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