Theorem finite_dimensional.finrank_map_subtype_eq
Modification history
2023-04-14 22:49
src/linear_algebra/finite_dimensional.lean
feat(linear_algebra/finite_dimensional): generalize results to `module.finite` (#18811) …
Deleted finite_dimensional.finrank_map_subtype_eqView on Github →