multiset_prod_le_inf — Mathlib

English

If I and J are ideals with I + J = R (coprime), then IJ = I ∩ J.

Русский

Если идеалы I и J удовлетворяют I + J = R (сопряжены), тогда произведение IJ равно их пересечению I ∩ J.

LaTeX

$$$ IJ = I \cap J \quad \text{if } I + J = R. $$$

Lean4

theorem multiset_prod_le_inf {s : Multiset (Ideal R)} : s.prod ≤ s.inf := by
  classical
  refine s.induction_on ?_ ?_
  · rw [Multiset.inf_zero]
    exact le_top
  intro a s ih
  rw [Multiset.prod_cons, Multiset.inf_cons]
  exact le_trans mul_le_inf (inf_le_inf le_rfl ih)

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