linearIndependent_single_one — Mathlib

English

For any index set ι and ring R, the family i ↦ Pi.single i 1 is linearly independent.

Русский

Для произвольного множества индексов ι и кольца R последовательность i ↦ Pi.single i 1 линейно независима.

LaTeX

$$LinearIndependent R (fun i => Pi.single i (1 : R))$$

Lean4

theorem linearIndependent_single_one (ι R : Type*) [Semiring R] [DecidableEq ι] :
    LinearIndependent R (fun i : ι ↦ Pi.single i (1 : R)) :=
  by
  rw [← linearIndependent_equiv (Equiv.sigmaPUnit ι)]
  exact
    Pi.linearIndependent_single (fun (_ : ι) (_ : Unit) ↦ (1 : R)) <| by
      simp +contextual [Fintype.linearIndependent_iffₛ]

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