span_pair_add_mul_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem span_pair_add_mul_left {R : Type u} [CommRing R] {x y : R} (z : R) :
    (span {x + y * z, y} : Ideal R) = span { x, y } := by
  ext
  rw [mem_span_pair, mem_span_pair]
  exact
    ⟨fun ⟨a, b, h⟩ =>
      ⟨a, b + a * z, by
        rw [← h]
        ring1⟩,
      fun ⟨a, b, h⟩ =>
      ⟨a, b - a * z, by
        rw [← h]
        ring1⟩⟩

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