Commit 2026-09-30 11:16 5bd58ac2

View on Github →

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

Estimated changes

Modified Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean

modified theorem LinearMap.finrank_range_add_finrank_ker

Modified Mathlib/LinearAlgebra/Matrix/Rank.lean

added theorem Matrix.rank_mul_ge