Mathlib v3 is deprecated. Go to Mathlib v4

Def submodule.comap_subtype_equiv_of_le

Modification history

2020-08-08 09:22
src/linear_algebra/basic.lean
feat(linear_algebra/finite_dimensional): finite dimensional `is_basis` helpers (#3720) …
Added submodule.comap_subtype_equiv_of_leView on Github →