instHMul

Mathlib.RingTheory.Ideal.Operations

URI: https://scilib.ai/kg/mathlib#Ideal.IsTwoSided.instHMul

← MathLib Explorer

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

instance (priority := low) [J.IsTwoSided] : (I * J).IsTwoSided :=
  ⟨fun b ha ↦
    Submodule.mul_induction_on ha (fun i hi j hj ↦ by rw [mul_assoc]; exact mul_mem_mul hi (mul_mem_right _ _ hj))
      fun x y hx hy ↦ by rw [right_distrib]; exact add_mem hx hy⟩

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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