Theorem LinearMap.finrank_range_add_finrank_ker

Modification history

2026-09-30 11:16

Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean

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

Modified LinearMap.finrank_range_add_finrank_ker View on Github →

2023-04-25 11:42

Mathlib/LinearAlgebra/FiniteDimensional.lean

feat: port LinearAlgebra.FiniteDimensional (#3466)

Added LinearMap.finrank_range_add_finrank_ker View on Github →