English
Under the hypotheses of Ne-zero scalars, the Pi.single indexed family is linearly independent.
Русский
При предположениях ненулевых скаляров семейство Pi.single индексировано линейно независимо.
LaTeX
$$LinearIndependent R (fun i => Pi.single i (v i))$$
Lean4
/-- `Pi.basis (s : ∀ j, Basis (ιs j) R (Ms j))` is the `Σ j, ιs j`-indexed basis on `Π j, Ms j`
given by `s j` on each component.
For the standard basis over `R` on the finite-dimensional space `η → R` see `Pi.basisFun`.
-/
protected noncomputable def basis (s : ∀ j, Basis (ιs j) R (Ms j)) : Basis (Σ j, ιs j) R (∀ j, Ms j) :=
Basis.ofRepr ((LinearEquiv.piCongrRight fun j => (s j).repr) ≪≫ₗ (Finsupp.sigmaFinsuppLEquivPiFinsupp R).symm)
