mul_le_mul_right

Mathlib.Algebra.Ring.Submonoid.Pointwise

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

English

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

Русский

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

LaTeX

$$$ N \le Q \Rightarrow M * N \le M * Q $$$

Lean4

theorem mul_le_mul_right (h : N ≤ P) : M * N ≤ M * P :=
  smul_le_smul_right h

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

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

Разделы

Аффилиация

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