dpow_mem — Mathlib

English

If I is an ideal of a commutative semiring A and m ≠ 0, then for any x ∈ I the m-th divided power dpow I m x lies in I.

Русский

Пусть I — идеал в коммутативном полугруппе A. Если m ≠ 0 и x ∈ I, то dpow I m x ∈ I.

LaTeX

$$$m \neq 0 \land x \in I \implies dpow\_I(m, x) \in I$$$

Lean4

theorem dpow_mem {m : ℕ} (hm : m ≠ 0) {x : A} (hx : x ∈ I) : dpow I m x ∈ I :=
  by
  rw [dpow_eq_of_mem hx]
  exact Ideal.mul_mem_left I _ (Ideal.pow_mem_of_mem I hx _ (Nat.pos_of_ne_zero hm))

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