coeIdeal_le_coeIdeal — Mathlib

English

In presence of localization, the lattice order on fractional ideals induced by coeIdeal respects ≤ on the underlying ideals.

Русский

При локализации тождественная когортная структура дробных идеалов сохраняет порядок ≤ между основаниями.

LaTeX

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

Lean4

@[simp]
theorem coeIdeal_le_coeIdeal (K : Type*) [CommRing K] [Algebra R K] [IsFractionRing R K] {I J : Ideal R} :
    (I : FractionalIdeal R⁰ K) ≤ J ↔ I ≤ J :=
  IsFractionRing.coeSubmodule_le_coeSubmodule

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