rank_mul_le_left — Mathlib

English

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

Русский

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

LaTeX

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

Lean4

theorem rank_mul_le_left (A : Matrix m n R) (B : Matrix n o R) : (A * B).rank ≤ A.rank :=
  by
  nontriviality R
  rw [rank, rank, mulVecLin_mul]
  exact Cardinal.toNat_le_toNat (LinearMap.rank_comp_le_left _ _) (rank_lt_aleph0 _ _)

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