Commit 2020-08-23 02:34 7ac7246e
View on Github →feat(linear_algebra/finite_dimensional): Add linear_equiv.of_inj_endo
and related lemmas (#3878)
This PR prepares #3864.
- Move the section
zero_dim
up. - Add several lemmas about finite dimensional vector spaces. The only new definition is
linear_equiv.of_injective_endo
, which produces a linear equivalence from an injective endomorphism.