Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-05-22 19:04 d07e3b3e

View on Github →

feat(linear_algebra/basic): general_linear_group basics (#1064)

feat(linear_algebra/basic): general_linear_group basics This patch proves that the general_linear_group (defined as units in the endomorphism ring) are equivalent to the group of linear equivalences.
shorten proof of ext
Add mul_equiv
Use coe
Fix stupid error

Estimated changes

Modified src/linear_algebra/basic.lean

added theorem linear_equiv.ext

added theorem linear_equiv.to_equiv_injective

added def linear_map.general_linear_group.general_linear_equiv

added theorem linear_map.general_linear_group.general_linear_equiv_to_linear_map

added def linear_map.general_linear_group.of_linear_equiv

added def linear_map.general_linear_group.to_linear_equiv