smul_mono

Mathlib.Algebra.Algebra.Operations

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

English

Equality of the scalar action when viewed as a Set and as a Submodule.

Русский

Согласование действия скалярного умножения при рассмотрении как множество и как подмодуль.

LaTeX

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

Lean4

theorem smul_mono (hij : I ≤ J) (hnp : N ≤ P) : I • N ≤ J • P :=
  AddSubmonoid.smul_le_smul hij hnp

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

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

Разделы

Аффилиация

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