smul_le

Mathlib.Algebra.Algebra.Operations

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

English

The set-based scalar multiplication agrees with the Submodule scalar multiplication.

Русский

Умножение множества на множество согласуется с умножением подмодуля.

LaTeX

$$$(I : Set A) \\cdot N = I \\cdot N$$$

Lean4

theorem smul_le : I • N ≤ P ↔ ∀ r ∈ I, ∀ n ∈ N, r • n ∈ P :=
  AddSubmonoid.smul_le

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

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

Разделы

Аффилиация

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