span_singleton_abs

Mathlib.RingTheory.Ideal.Span

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

English

In a ring with a linear order, the span of the absolute value |x| equals the span of x.

Русский

В кольце с линейным упорядочением порождение |x| равно порождению x.

LaTeX

$$$$ \operatorname{span} (\{|x|\}) = \operatorname{span} (\{x\}) $$$$

Lean4

@[simp]
theorem span_singleton_abs [LinearOrder α] (x : α) : span {|x|} = span { x } := by
  obtain h | h := abs_choice x <;> simp [h]

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

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

Разделы

Аффилиация

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