Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes

modified theorem findim_bot
added theorem linear_map.is_unit_iff