disjoint_powers_iff_notMem — Mathlib

English

For a radical ideal I and y in R, Disjoint(powers y, I) iff y ∉ I.

Русский

Для радикального идеала I и элемента y выполняется: Disjoint(powers y, I) тогда и только тогда, когда y ∉ I.

LaTeX

$$$\\text{Disjoint}((\\{y^n : n \\in \\mathbb{N}\\}\\,), I) \\iff y \\notin I$$$

Lean4

theorem disjoint_powers_iff_notMem (y : R) (hI : I.IsRadical) : Disjoint (Submonoid.powers y : Set R) ↑I ↔ y ∉ I.1 :=
  by
  refine ⟨fun h => Set.disjoint_left.1 h (Submonoid.mem_powers _), fun h => disjoint_iff.mpr (eq_bot_iff.mpr ?_)⟩
  rintro x ⟨⟨n, rfl⟩, hx'⟩
  exact h (hI <| mem_radical_of_pow_mem <| le_radical hx')

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