linearIndependent_iff_union_smaller

English

For the set of GoodProducts evaluated on C, linear independence over the integers is equivalent to the linear independence of the function p ↦ p.1 from the union over smaller indices.

Русский

Линейная независимость множества, полученного из GoodProducts на C, над целыми эквивалентна линейной независимости отображения p ↦ p.1 из объединения smaller.

LaTeX

$$$\\operatorname{LinearIndependent}_{\\mathbb{Z}}\\big(\\mathrm{GoodProducts}.\\mathrm{eval}\\;C\\big) \\;\\Leftrightarrow\\; \\operatorname{LinearIndependent}_{\\mathbb{Z}}\\big(\\lambda p: p.1\\big)$$$

Lean4

theorem linearIndependent_iff_union_smaller :
    LinearIndependent ℤ (GoodProducts.eval C) ↔
      LinearIndependent ℤ (fun (p : ⋃ (e : { o' // o' < o }), (smaller C e.val)) ↦ p.1) :=
  by
  rw [GoodProducts.linearIndependent_iff_range, ← range_equiv_factorization C ho hsC]
  exact linearIndependent_equiv (range_equiv C ho hsC)

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