span_pair_comm

Mathlib.RingTheory.Ideal.Span

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

English

Swapping the two generators does not change the generated ideal: span{ x, y } = span{ y, x }.

Русский

Порождение двух элементов не зависит от порядка: span{ x, y } = span{ y, x }.

LaTeX

$$$$ \operatorname{span}\{ x, y \} = \operatorname{span}\{ y, x \} $$$$

Lean4

theorem span_pair_comm {x y : α} : (span { x, y } : Ideal α) = span { y, x } := by simp only [span_insert, sup_comm]

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

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

Разделы

Аффилиация

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