localized'_smul — Mathlib

English

Localization respects smul by an ideal: the localized' of I·M' equals I localized' composed with smul.

Русский

Локализация сохраняет действие идеала: localized'(S,p,f)(I·M') = I·localized'(S,p,f)M'.

LaTeX

$$$\\operatorname{localized}'(S,p,f)(\\operatorname{I} \\cdot M') = I \\cdot \\operatorname{localized}'(S,p,f)M'.$$$

Lean4

theorem localized'_smul (I : Submodule R R) :
    (I • M').localized' S p f = I.localized' S p (Algebra.linearMap R S) • M'.localized' S p f :=
  Submodule.restrictScalars_injective R _ _ <| by
    simp_rw [restrictScalars_localized'_smul, restrictScalars_localized', localized₀_smul]

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