span_singleton_eq_span_singleton — Mathlib

English

For x,y in a domain, span{ x } = span{ y } iff x and y are associated (differ by a unit).

Русский

Для элементов x,y в области span{ x } = span{ y } тогда и только тогда, когда x и y эквивалентны по единице (ассоциированы).

LaTeX

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

Lean4

theorem span_singleton_eq_span_singleton {α : Type u} [CommSemiring α] [IsDomain α] {x y : α} :
    span ({ x } : Set α) = span ({ y } : Set α) ↔ Associated x y :=
  by
  rw [← dvd_dvd_iff_associated, le_antisymm_iff, and_comm]
  apply and_congr <;> rw [span_singleton_le_span_singleton]

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