linearIndependent_iff_smaller — Mathlib

English

Equivalence of linear independence statements via a smaller factorization is shown.

Русский

Показано эквивалентность линейной независимости через меньшую факторизацию.

LaTeX

$$$$ \\text{Equiv}\\; (\\mathrm{LinearIndependent}_{\\mathbb{Z}}\\; (\\mathrm{GoodProducts}.\\mathrm{eval}\\; (\\pi C (ord I ·< o)))) \\; (\\mathrm{LinearIndependent}_{\\mathbb{Z}}\\; (\\lambda p. p.1)) $$$$

Lean4

theorem linearIndependent_iff_smaller (o : Ordinal) :
    LinearIndependent ℤ (GoodProducts.eval (π C (ord I · < o))) ↔ LinearIndependent ℤ (fun (p : smaller C o) ↦ p.1) :=
  by
  rw [GoodProducts.linearIndependent_iff_range, ←
    LinearMap.linearIndependent_iff (πs C o) (LinearMap.ker_eq_bot_of_injective (injective_πs _ _)), ←
    smaller_factorization C o]
  exact linearIndependent_equiv _

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