span_pair_mul_span_pair — Mathlib

English

The product of the ideals generated by two-element sets satisfies a distributive rule: span{w,x} · span{y,z} = span{wy, wz, xy, xz}.

Русский

Произведение идеалов, порождаемых двумя элементами, удовлетворяет тождеству генераторов: span{w,x} · span{y,z} = span{wy, wz, xy, xz}.

LaTeX

$$$$ \operatorname{span}\{w,x\} \cdot \operatorname{span}\{y,z\} = \operatorname{span}\{wy, wz, xy, xz\} $$$$

Lean4

theorem span_pair_mul_span_pair (w x y z : R) :
    (span { w, x } : Ideal R) * span { y, z } = span {w * y, w * z, x * y, x * z} := by
  simp_rw [span_insert, sup_mul, mul_sup, span_singleton_mul_span_singleton, sup_assoc]

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