instMulRightMono

Mathlib.Algebra.Algebra.Operations

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

English

Left multiplication by a submodule is monotone: if M ≤ M', then M * N ≤ M' * N.

Русский

Левая умножение подмодуля на другой подмодуль монотонно: если M ≤ M', то M * N ≤ M' * N.

LaTeX

$$$ M \le M' \Rightarrow M * N \le M' * N $$$

Lean4

instance : MulRightMono (Submodule R A) where elim _ _ _ := smul_mono_left

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

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

Разделы

Аффилиация

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