Independent — Mathlib

English

A family f is independent if and only if the corresponding family of submodules given by rep ∘ f is linearly independent.

Русский

Семейство f независимо тогда и только тогда, когда соответствующее ему семейство подмодулей, заданное rep ∘ f, линейно независимо.

LaTeX

$$$ Independent(f) \\iff LinearIndependent(K, (Projectivization.rep \\circ f)) $$$

Lean4

/-- A linearly independent family of nonzero vectors gives an independent family of points
in projective space. -/
inductive Independent : (ι → ℙ K V) → Prop
  | mk (f : ι → V) (hf : ∀ i : ι, f i ≠ 0) (hl : LinearIndependent K f) : Independent fun i => mk K (f i) (hf i)

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