English
If A B = 0 with A and B of compatible sizes, then rank(A) + rank(B) ≤ card of the middle dimension.
Русский
Если A B = 0, то ранг A + ранг B не превосходит число столбцов/строк в среднюю размерность.
LaTeX
$$$ A \in M_{l,m}(R), B \in M_{m,n}(R), \ AB = 0 \Longrightarrow\ \operatorname{rank}(A) + \operatorname{rank}(B) \le |m|. $$$
Lean4
theorem rank_add_rank_le_card_of_mul_eq_zero [Field R] [Finite l] [Fintype m] {A : Matrix l m R} {B : Matrix m n R}
(hAB : A * B = 0) : A.rank + B.rank ≤ Fintype.card m := by
classical
let el : Basis l R (l → R) := Pi.basisFun R l
let em : Basis m R (m → R) := Pi.basisFun R m
let en : Basis n R (n → R) := Pi.basisFun R n
rw [Matrix.rank_eq_finrank_range_toLin A el em, Matrix.rank_eq_finrank_range_toLin B em en, ←
Module.finrank_fintype_fun_eq_card R, ← LinearMap.finrank_range_add_finrank_ker (Matrix.toLin em el A),
add_le_add_iff_left]
apply Submodule.finrank_mono
rw [LinearMap.range_le_ker_iff, ← Matrix.toLin_mul, hAB, map_zero]
