span_mul_span'

Mathlib.RingTheory.Ideal.Operations

URI: https://scilib.ai/kg/mathlib#Ideal.span_mul_span'

English

For sets S,T in a commutative semiring, span S · span T = span (S T).

Русский

Для множеств S,T в коммутативной полугруппе span S · span T = span(S T).

LaTeX

$$$ \\operatorname{span} S \\cdot \\operatorname{span} T = \\operatorname{span}(S T)$$$

Lean4

theorem span_mul_span' (S T : Set R) : span S * span T = span (S * T) :=
  by
  unfold span
  rw [Submodule.span_mul_span]

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

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

Разделы

Аффилиация

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