mul

Mathlib.Algebra.Algebra.Operations

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

← MathLib Explorer

English

If m ∈ M and n ∈ N, then m n ∈ M * N.

Русский

Если m ∈ M и n ∈ N, то m n ∈ M * N.

LaTeX

$$$ m \in M \quad \text{and} \quad n \in N \Rightarrow m n \in M * N $$$

Lean4

/-- Multiplication of sub-R-modules of an R-module A that is also a semiring. The submodule `M * N`
consists of finite sums of elements `m * n` for `m ∈ M` and `n ∈ N`. -/
instance mul : Mul (Submodule R A) where mul := (· • ·)

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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