rank_vecMulVec_le — Mathlib

English

For w : m → R and v : n → R, the rank of the matrix vecMulVec(w,v) is at most 1.

Русский

Пусть w : m → R и v : n → R. Тогда ранк матрицы vecMulVec(w,v) не превосходит 1.

LaTeX

$$$\operatorname{rank}(\mathrm{vecMulVec}(w,v)) \le 1$$$

Lean4

theorem rank_vecMulVec_le (w : m → R) (v : n → R) : (Matrix.vecMulVec w v).rank ≤ 1 :=
  by
  rw [Matrix.vecMulVec_eq Unit]
  refine le_trans (rank_mul_le_left _ _) ?_
  nontriviality R
  exact rank_le_card_width _

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