rank_mul_le

Mathlib.LinearAlgebra.Matrix.Rank

URI: https://scilib.ai/kg/mathlib#Matrix.rank_mul_le

← MathLib Explorer

English

For A ∈ M_{m×n}(R) and B ∈ M_{n×o}(R), rank(AB) ≤ min(rank(A), rank(B)).

Русский

Для A ∈ M_{m×n}(R) и B ∈ M_{n×o}(R) ранг(AB) не превосходит min{ранг(A), ранг(B)}.

LaTeX

$$$\operatorname{rank}(AB) \le \min\{\operatorname{rank}(A), \operatorname{rank}(B)\}$$$

Lean4

theorem rank_mul_le (A : Matrix m n R) (B : Matrix n o R) : (A * B).rank ≤ min A.rank B.rank :=
  le_min (rank_mul_le_left _ _) (rank_mul_le_right _ _)

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

Научная платформа российской исследовательской школы.

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru