dvd_span_singleton — Mathlib

English

For any ideal I and element x, I divides the span of x if and only if x ∈ I.

Русский

Для любого идеала I и элемента x выполняется: I делит span{ x } тогда и только тогда, когда x ∈ I.

LaTeX

$$$I \mid \mathrm{span}\{x\} \iff x \in I$$$

Lean4

@[simp]
theorem dvd_span_singleton {I : Ideal A} {x : A} : I ∣ Ideal.span { x } ↔ x ∈ I :=
  Ideal.dvd_iff_le.trans (Ideal.span_le.trans Set.singleton_subset_iff)

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