mul_le_inf

Mathlib.RingTheory.Ideal.Operations

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

English

For any commutative ring R and ideals I, J of R, the product I J is contained in the intersection I ∩ J: I J ≤ I ∩ J.

Русский

Для коммутативного кольца R и идеалов I, J выполняется включение произведения: I J ⊆ I ∩ J.

LaTeX

$$$ I J \le I \cap J. $$$

Lean4

theorem mul_le_inf : I * J ≤ I ⊓ J :=
  mul_le.2 fun r hri s hsj => ⟨I.mul_mem_right s hri, J.mul_mem_left r hsj⟩

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

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

Разделы

Аффилиация

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