mul_mono

Mathlib.RingTheory.Ideal.Operations

URI: https://scilib.ai/kg/mathlib#Ideal.mul_mono

English

If I ≤ K and J ≤ L then I ⋅ J ≤ K ⋅ L.

Русский

Если I ≤ K и J ≤ L, то I⋅J ≤ K⋅L.

LaTeX

$$$I \cdot J \le K \cdot L$$$

Lean4

theorem mul_mono (hik : I ≤ K) (hjl : J ≤ L) : I * J ≤ K * L :=
  Submodule.smul_mono hik hjl

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

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

Разделы

Аффилиация

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