card_le_card_of_linearIndependent_aux

English

If R satisfies the strong rank condition and there is a linear independence of m elements of a free rank-n R-module, then m ≤ n.

Русский

Пусть R удовлетворяет условию сильной ранговости и существует линейно независимая система из m элементов свободного модуля ранга n. Тогда m ≤ n.

LaTeX

$$$m \\le n$$$

Lean4

/-- Let `R` satisfy the strong rank condition. If `m` elements of a free rank `n` `R`-module are
linearly independent, then `m ≤ n`. -/
theorem card_le_card_of_linearIndependent_aux {R : Type*} [Semiring R] [StrongRankCondition R] (n : ℕ) {m : ℕ}
    (v : Fin m → Fin n → R) : LinearIndependent R v → m ≤ n := fun h => by
  simpa using linearIndependent_le_basis (Pi.basisFun R (Fin n)) v h

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