rank_mul_le_right — Mathlib

English

Let A ∈ M_{m×n}(R) and B ∈ M_{n×o}(R). Then rank(AB) ≤ rank(B).

Русский

Пусть A ∈ M_{m×n}(R) и B ∈ M_{n×o}(R). Тогда ранг(AB) ≤ ранг(B).

LaTeX

$$$\operatorname{rank}(AB) \le \operatorname{rank}(B)$$$

Lean4

theorem rank_mul_le_right (A : Matrix m n R) (B : Matrix n o R) : (A * B).rank ≤ B.rank :=
  by
  nontriviality R
  rw [rank, rank, mulVecLin_mul]
  exact finrank_le_finrank_of_rank_le_rank (LinearMap.lift_rank_comp_le_right _ _) (rank_lt_aleph0 _ _)

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