mul_def

Mathlib.Algebra.Algebra.Operations

URI: https://scilib.ai/kg/mathlib#Submodule.mul_def

English

The product of submodules M and N equals the span of their pointwise products, i.e., M·N = span_R(M·N).

Русский

Произведение подмодулей M и N равно оболочке множества их попарных произведений: M·N = span_R(M·N).

LaTeX

$$$M \\cdot N = \\operatorname{span}_R\\bigl(M N : \\text{Set} A\\bigr)$$$

Lean4

theorem mul_def : M * N = span R (M * N : Set A) := by simp [← span_mul_span]

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

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

Разделы

Аффилиация

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