inf_mul

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

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

English

In the fractional setting, (I ∩ J) * K = I * K ∩ J * K.

Русский

Для дробных идеалов выполняется: (I ∩ J) · K = I · K ∩ J · K.

LaTeX

$$(I ∩ J) * K = I * J ∧ I * K$$

Lean4

theorem inf_mul (I J K : Ideal A) : (I ⊓ J) * K = I * K ⊓ J * K := by simp only [Ideal.mul_inf, mul_comm _ K]

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

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

Разделы

Аффилиация

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