Commit 2026-04-17 13:58 f55473ee

View on Github →

chore(LinearAlgebra/Dimension): move proof of finrank_le_finrank_of_surjective earlier (#38129)

  • Move LinearMap.finrank_le_finrank_of_surjective one file earlier by simplifying the proof to match LinearMap.finrank_le_finrank_of_injective

Estimated changes