le_singleton_iff — Mathlib

English

For any x in A, n a natural number, and any ideal I, the n-th power of I is contained in the principal ideal generated by x if and only if x belongs to I^n.

Русский

Для любого элемента x из A, натурального числа n и идеала I верно: I^n ⊆ (x) тогда и только если x ∈ I^n.

LaTeX

$$$I^n \\subseteq (x) \\quad\\Longleftrightarrow\\quad x \\in I^n$$

Lean4

theorem le_singleton_iff (x : A) (n : ℕ) (I : Ideal A) :
    Associates.mk I ^ n ≤ Associates.mk (Ideal.span { x }) ↔ x ∈ I ^ n := by
  simp_rw [← Associates.dvd_eq_le, ← Associates.mk_pow, Associates.mk_dvd_mk, Ideal.dvd_span_singleton]

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