coeIdeal_injective' — Mathlib

English

Under IsLocalization, the map I ↦ coeIdeal I is injective on ideals.

Русский

При локализации отображение I ↦ coeIdeal I инъективно на идеалах.

LaTeX

$$coeIdeal_injective' (h) : Function.Injective (fun I => (I : FractionalIdeal S P))$$

Lean4

theorem coeIdeal_injective' (h : S ≤ nonZeroDivisors R) :
    Function.Injective (fun (I : Ideal R) ↦ (I : FractionalIdeal S P)) := fun _ _ h' =>
  ((coeIdeal_le_coeIdeal' S h).mp h'.le).antisymm ((coeIdeal_le_coeIdeal' S h).mp h'.ge)

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