dpow_span_isSubideal — Mathlib

English

If S ⊆ I, then the span of all hI.dpow n x with n ≠ 0 and x ∈ S lies inside I.

Русский

Если S ⊆ I, то множество значений hI.dpow n x с n ≠ 0 и x ∈ S образует подпоясание внутри I

LaTeX

$$span { y | ∃ n ≠ 0, ∃ x ∈ S, y = hI.dpow n x } ≤ I$$

Lean4

theorem _root_.DividedPowers.dpow_span_isSubideal {S : Set A} (hS : S ⊆ I) :
    span {y : A | ∃ (n : ℕ) (_ : n ≠ 0) (x : A) (_ : x ∈ S), y = hI.dpow n x} ≤ I :=
  by
  rw [span_le]
  rintro y ⟨n, hn, x, hx, hxy⟩
  exact hxy ▸ hI.dpow_mem hn (hS hx)

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