iff_fractionRing — Mathlib

English

For a module V over R, and its fraction field K, a family b: ι → V is linearly independent over R iff it is linearly independent over K.

Русский

Для модуля V над кольцом R и его полем частичных дробей K: семейство в состоит из элементов V, линейно независимо над R тогда и только тогда, когда линейно независимо над K.

LaTeX

$$$\\operatorname{LinearIndependent}_R b \\iff \\operatorname{LinearIndependent}_K b$$$

Lean4

theorem iff_fractionRing {ι : Type*} {b : ι → V} : LinearIndependent R b ↔ LinearIndependent K b :=
  ⟨.localization K R⁰, .restrict_scalars <| (faithfulSMul_iff_injective_smul_one ..).mp inferInstance⟩

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