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

Merged

feat(linear_algebra/basic): general_linear_group basics #1064

mergify merged 7 commits into master from units-linear-equiv

jcommelin requested a review 7 years ago

feat(linear_algebra/basic): general_linear_group basics

9a756e7c

ChrisHughes24 commented on 2019-05-20

ChrisHughes24 assigned

ChrisHughes24 7 years ago

shorten proof of ext

3ed1b203

Add mul_equiv

b8c94d0f

Use coe

6e0aa5fa

Fix stupid error

ac52a760

ChrisHughes24 added ready-to-merge

ChrisHughes24 approved these changes on 2019-05-22

Merge branch 'master' into 'units-linear-equiv'

c151cebb

Merge branch 'master' into 'units-linear-equiv'

a517e9e4

mergify merged d07e3b3e into master 7 years ago

mergify deleted the units-linear-equiv branch 7 years ago

Reviewers

ChrisHughes24

Assignees

ChrisHughes24

Labels

ready-to-merge

Milestone

No milestone