coe_inv_of_nonzero — Mathlib

English

For J ≠ 0, the inverse J^{-1} as a submodule equals IsLocalization.coeSubmodule K ⊤ / (J : Submodule R K).

Русский

Для J ≠ 0 обратное J^{-1} как подмодуль равно IsLocalization.coeSubmodule K ⊤ / (J : Submodule R K).

LaTeX

$$$$ (\uparrow J^{-1}) = \mathrm{IsLocalization.coeSubmodule}\,K\,\top \/ (J : \mathrm{Submodule}\, R K). $$$$

Lean4

theorem coe_inv_of_nonzero {J : FractionalIdeal R₁⁰ K} (h : J ≠ 0) :
    (↑J⁻¹ : Submodule R₁ K) = IsLocalization.coeSubmodule K ⊤ / (J : Submodule R₁ K) := by
  simp_rw [inv_nonzero _ h, coe_one, coe_mk, IsLocalization.coeSubmodule_top]

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