span_singleton_neg — Mathlib

English

In a commutative ring, the span of {x, y + x z} equals the span of {x, y}.

Русский

В коммутативном кольце порождение {x, y + x z} равно порождению {x, y}.

LaTeX

$$$$ \operatorname{span}(\{ x, y + x z \}) = \operatorname{span}(\{ x, y \}) $$$$

Lean4

@[simp]
theorem span_singleton_neg (x : α) : (span {-x} : Ideal α) = span { x } :=
  by
  ext
  simp only [mem_span_singleton']
  exact ⟨fun ⟨y, h⟩ => ⟨-y, h ▸ neg_mul_comm y x⟩, fun ⟨y, h⟩ => ⟨-y, h ▸ neg_mul_neg y x⟩⟩

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