span_pair_eq_span_right_iff_dvd

Mathlib.RingTheory.Ideal.Span

URI: https://scilib.ai/kg/mathlib#Ideal.span_pair_eq_span_right_iff_dvd

← MathLib Explorer

English

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

Русский

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

LaTeX

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

Lean4

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

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru