linearIndependent_one_tmul — Mathlib

English

If a family v is linearly independent over R, then its image under tensor by 1 in S is linearly independent over S.

Русский

Если семейство v линейно независимо над R, то образ под тензором с единицей в S линейно независим над S.

LaTeX

$$$\text{LinearIndependent}_R(v) \Rightarrow \text{LinearIndependent}_S((1) \otimes_S v) $$$

Lean4

theorem linearIndependent_one_tmul {S} [Semiring S] [Algebra R S] [Flat R S] {ι} {v : ι → M}
    (hv : LinearIndependent R v) : LinearIndependent S ((1 : S) ⊗ₜ[R] v ·) :=
  by
  classical rw [LinearIndependent, ← LinearMap.coe_restrictScalars R, Finsupp.linearCombination_one_tmul]
  simpa using lTensor_preserves_injective_linearMap _ hv

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