Commit 2021-09-29 11:22 43c1ab27

fix(linear_algebra/basic): generalize linear_map.add_comm_group to semilinear maps (#9402) Also generalizes coe_mk and golfs some proofs.

modified theorem linear_map.coe_mk