Theorems · Theorem · functional analysis

RCLike.linearIndependent_of_ne_zero_of_wInner_one_eq_zero

∀ {ι : Type u_1} {κ : Type u_2} {𝕜 : Type u_3} [inst : Fintype ι] [inst_1 : RCLike 𝕜] {f : κ → ι → 𝕜},
  (∀ (k : κ), f k ≠ 0) → (Pairwise fun k₁ k₂ => ⟪f k₁, f k₂⟫_[𝕜] = 0) → LinearIndependent 𝕜 f

Defined in

Mathlib.Analysis.RCLike.Inner

Cited by

1 results in Mathlib

Foundations

Depth 228 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

FintypeRCLike