Commit 2022-03-03 21:31 e84c1a96
View on Github →chore(linear_algebra/general_linear_group): replace coe_fn with coe in lemma statements (#12397)
This way, all the lemmas are expressed in terms of ↑ and not ⇑.
This matches the approach used in special_linear_group.