localization — Mathlib

English

If R is localized to Rₛ and we have a module M with a basis that is localized, then the localized basis remains linearly independent in the localized module.

Русский

Если локализация сохраняет базис модуля, то локализованный базис линейно независим.

LaTeX

$$LinearIndependent R b → LinearIndependent Rₛ b$$

Lean4

theorem localization [Module Rₛ M] [IsScalarTower R Rₛ M] {ι : Type*} {b : ι → M} (hli : LinearIndependent R b) :
    LinearIndependent Rₛ b := by
  have := isLocalizedModule_id S M Rₛ
  exact hli.of_isLocalizedModule Rₛ S .id

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