Theorem LinearMap.finrank_le_finrank_of_surjective

Modification history

2026-04-17 13:58
Mathlib/LinearAlgebra/Dimension/Constructions.lean
chore(LinearAlgebra/Dimension): move proof of `finrank_le_finrank_of_surjective` earlier (#38129) …
Modified LinearMap.finrank_le_finrank_of_surjectiveView on Github →
2026-04-15 19:09
Mathlib/LinearAlgebra/Dimension/Constructions.lean
feat(RingTheory/IsAdjoinRoot): add mkOfAdjoinEqTop' (#36421) …
Added LinearMap.finrank_le_finrank_of_surjectiveView on Github →