Theorem Matrix.rank_mul_ge

Modification history

2026-09-30 11:16

Mathlib/LinearAlgebra/Matrix/Rank.lean

feat(LinearAlgebra/Matrix): add Sylvester's rank inequality (#43065)

Added Matrix.rank_mul_ge View on Github →