linearIndependent — Mathlib

English

The span of spanFinBasis C s equals the whole module: top ≤ span of the range of spanFinBasis.

Русский

Замыкание порожденного набора spanFinBasis C s порождает весь модуль: верхний элемент пространства подмодулов принадлежит span.

LaTeX

$$$\\top \\leq \\operatorname{Submodule.span} \\mathbb{Z} (\\operatorname{Set.range}(\\operatorname{spanFinBasis} C s))$$$

Lean4

theorem linearIndependent (hC : IsClosed C) : LinearIndependent ℤ (GoodProducts.eval C) :=
  GoodProducts.linearIndependentAux (Ordinal.type (· < · : I → I → Prop)) (le_refl _) C hC
    (fun _ _ _ _ ↦ Ordinal.typein_lt_type _ _)

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