mathlib

1b4e7694 - feat(linear_algebra/affine_space): define `affine_equiv` (#2909)

feat(linear_algebra/affine_space): define `affine_equiv` (#2909) Define * [X] `affine_equiv` to be an invertible affine map (e.g., extend both `affine_map` and `equiv`); * [X] conversion to `linear_equiv`; * [X] `group` structure on affine automorphisms; * [X] prove standard lemmas for equivalences (`apply_symm_apply`, `symm_apply_eq` etc). API changes * make `G` implicit in `equiv.vadd_const`.