coeIdeal_le_coeIdeal' — Mathlib

English

Under IsLocalization, the order between fractional ideals is captured by the order of their underlying ideals.

Русский

При локализации порядок дробных идеалов соответствует порядку их оснований-идеалов.

LaTeX

$$[IsLocalization S P] (h : S ≤ nonZeroDivisors R) {I J : Ideal R} : (I : FractionalIdeal S P) ≤ J ↔ I ≤ J$$

Lean4

theorem coeIdeal_le_coeIdeal' [IsLocalization S P] (h : S ≤ nonZeroDivisors R) {I J : Ideal R} :
    (I : FractionalIdeal S P) ≤ J ↔ I ≤ J :=
  coeSubmodule_le_coeSubmodule h

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