mul_le_mul_left

Mathlib.Algebra.Ring.Submonoid.Pointwise

URI: https://scilib.ai/kg/mathlib#AddSubmonoid.mul_le_mul_left

English

If M ≤ N, then M * P ≤ N * P.

Русский

Если M ⊆ N, то M · P ⊆ N · P.

LaTeX

$$$ M \le N \Rightarrow M * P \le N * P $$$

Lean4

theorem mul_le_mul_left (h : M ≤ N) : M * P ≤ N * P :=
  smul_le_smul_left h

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

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

Разделы

Аффилиация

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