linearIndependent_iff — Mathlib

English

If hv is LI and f is injective on the ambient, then the image under f of a LI family remains LI.

Русский

Если hv линейно независимо и f инъективно на окружении, то образ LI семейства остаётся LI.

LaTeX

$$$\\text{LinearIndependent } R\\ v \\rightarrow \\text{LinearIndependent } R (f\\circ v)$$$

Lean4

/-- If `f` is an injective linear map, then the family `f ∘ v` is linearly independent
if and only if the family `v` is linearly independent. -/
protected theorem linearIndependent_iff (f : M →ₗ[R] M') (hf_inj : LinearMap.ker f = ⊥) :
    LinearIndependent R (f ∘ v) ↔ LinearIndependent R v :=
  f.linearIndependent_iff_of_disjoint <| by simp_rw [hf_inj, disjoint_bot_right]

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