localized'_eq_map — Mathlib

English

For a localization p: S, the localized' module with respect to p equals the map of I under algebra map.

Русский

Для локализации p: S локализованный'' модуль по отношению к p равен образу I под алгебраическим отображением.

LaTeX

$$$\\operatorname{Submodule.localized'} S p (\\mathrm{Algebra.linearMap} R S) I = I.map (\\mathrm{algebraMap} R S)$$$

Lean4

theorem localized'_eq_map (I : Ideal R) : Submodule.localized' S p (Algebra.linearMap R S) I = I.map (algebraMap R S) :=
  by rw [map, span, Submodule.localized'_eq_span, Algebra.coe_linearMap]

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