instPosMulReflectLEIdeal — Mathlib

English

Left multiplication by nonzero ideals reflects the order: if I·X ≤ J·X for some nonzero X, then I ≤ J.

Русский

Левое умножение на ненулевой идеал отражает порядок: если I·X ≤ J·X для некоторого ненулевого X, то I ≤ J.

LaTeX

$$$\forall I,J,X\,(X\neq 0)\, (I X \le J X \Rightarrow I \le J)$$$

Lean4

instance : 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]

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