instPosMulReflectLENonZeroDivisorsOfIsDedekindDomain

English

For a Dedekind domain, the order relation is reflected by multiplication by a nonzero fractional ideal.

Русский

Для Дедекинд домена порядок отражается умножением на ненулевой дробный идеал.

LaTeX

$$$$\\operatorname{PosMulReflectLE}\\; (\\text{FractionalIdeal})$$$$

Lean4

instance [IsDedekindDomain A] : PosMulReflectLE (FractionalIdeal A⁰ K) where
  elim I _ _ := (FractionalIdeal.mul_left_le_iff I.2.ne').mp

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