mathlib3

750ca956 - chore(linear_algebra/affine_space/affine_map): golf using the injective APIs (#12543)

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.