mathlib3

a6179f61 - feat(linear_algebra/affine_space/affine_equiv): isomorphism with the units (#10798)

feat(linear_algebra/affine_space/affine_equiv): isomorphism with the units (#10798) This adds: * `affine_equiv.equiv_units_affine_map` (the main point in this PR) * `affine_map.linear_hom` * `affine_equiv.linear_hom` * `simps` configuration for `affine_equiv`. In order to makes `simp` happy, we adjust the order of the implicit variables to all lemmas in this file, so that they match the order of the arguments to `affine_equiv`. The new definition can be used to majorly golf `homothety_units_mul_hom`