span_singleton_dvd_span_singleton_iff_dvd

English

In a principal ideal domain, the principle that span of a is contained in span of b is equivalent to a dividing b.

Русский

В принципиальном кольце аналогично: кольцевой порождающий образует включение, если и только если a делит b.

LaTeX

$$Ideal.span{a} ∣ Ideal.span{b} ⇔ a ∣ b$$

Lean4

theorem span_singleton_dvd_span_singleton_iff_dvd {a b : R} : Ideal.span { a } ∣ Ideal.span ({ b } : Set R) ↔ a ∣ b :=
  ⟨fun h => mem_span_singleton.mp (dvd_iff_le.mp h (mem_span_singleton.mpr (dvd_refl b))), fun h =>
    dvd_iff_le.mpr fun _d hd => mem_span_singleton.mpr (dvd_trans h (mem_span_singleton.mp hd))⟩

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