instPosMulReflectLEIdealOfIsDedekindDomain

English

In a Dedekind domain, exists_multiset_prod_cons_le_and_prod_not_le states a minimal product of prime ideals containing I with a distinguished maximal M.

Русский

В Дедекинд домене существует минимальное произведение простых идеалов, содержащее I с указанным максимальным M.

LaTeX

$$$$\\exists Z: Multiset(PrimeSpectrum A), \\; (M :: Z.map PrimeSpectrum.asIdeal).prod \\le I \\land \\lnot(\\prod (Z.map PrimeSpectrum.asIdeal)).prod \\le I.$$$$

Lean4

instance [IsDedekindDomain A] : PosMulReflectLE (Ideal A) where
  elim I J K
    e := by
    dsimp
    rwa [← FractionalIdeal.coeIdeal_le_coeIdeal (FractionRing A), ←
      FractionalIdeal.mul_left_le_iff (J := I) (by simpa using I.2.ne'), ← FractionalIdeal.coeIdeal_mul, ←
      FractionalIdeal.coeIdeal_mul, FractionalIdeal.coeIdeal_le_coeIdeal]

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