mul_inf

Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas

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

English

Ideals distribute over intersection: I * (J ∩ K) = I * J ∩ I * K.

Русский

Идеалы распределяются по пересечению: I · (J ∩ K) = (I · J) ∩ (I · K).

LaTeX

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

Lean4

theorem mul_inf (I J K : Ideal A) : I * (J ⊓ K) = I * J ⊓ I * K :=
  by
  rw [inf_eq_iInf, Ideal.mul_iInf, inf_eq_iInf]
  congr! 2 with ⟨⟩

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

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

Разделы

Аффилиация

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