Commit 2022-03-10 06:34 750ca956

chore(linear_algebra/affine_space/affine_map): golf using the injective APIs (#12543) The extra whitespace means this isn't actually any shorter by number of lines, but it does eliminate 12 trivial proofs. Again, the has_scalar instance has been hoisted from lower down the file, so that we have the nat and int actions available when we create the add_comm_group structure. Previously we just built the same has_scalar structure three times.