span_pair_add_mul_right — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

@[simp]
theorem span_pair_add_mul_right {R : Type u} [CommRing R] {x y : R} (z : R) :
    (span {x, y + x * z} : Ideal R) = span { x, y } := by rw [span_pair_comm, span_pair_add_mul_left, span_pair_comm]

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