mul_le_mul

Mathlib.Algebra.Ring.Submonoid.Pointwise

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

English

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

Русский

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

LaTeX

$$$ (M \le P) \land (N \le Q) \Rightarrow M * N \le P * Q $$$

Lean4

@[mono, gcongr]
theorem mul_le_mul (hmp : M ≤ P) (hnq : N ≤ Q) : M * N ≤ P * Q :=
  smul_le_smul hmp hnq

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

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

Разделы

Аффилиация

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