instMulPosReflectLENonZeroDivisorsOfIsDedekindDomain

English

For a Dedekind domain A, the product with nonzero divisors reflects order.

Русский

Для Дедекинд домена A произведение по ненулевым делителям отражает порядок.

LaTeX

$$$$\\forall I,J: \\text{FractionalIdeal}(A^0K)\;\\text{nonzero},\\; I \\le J \\Rightarrow I\\cdot M \\le J\\cdot M.$$$$

Lean4

instance [IsDedekindDomain A] : MulPosReflectLE (FractionalIdeal A⁰ K) where
  elim I J K e := by dsimp at *; rwa [mul_comm, mul_comm K, FractionalIdeal.mul_left_le_iff I.2.ne'] at e

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