span_pair_eq_span_left_iff_dvd — Mathlib

English

In a commutative semiring, span{x,y} = span{x} iff x divides y.

Русский

В коммутативном полускольнике span{x,y} = span{x} тогда, когда x делит y.

LaTeX

$$$$ \operatorname{span} (\{ x, y \}) = \operatorname{span} (\{ x \}) \iff x \mid y $$$$

Lean4

@[simp]
theorem span_pair_eq_span_left_iff_dvd {x y : α} : span { x, y } = span { x } ↔ x ∣ y := by
  rw [Ideal.span_insert, sup_eq_left, span_singleton_le_span_singleton]

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