mathlib3

39d5a98c - feat(linear_algebra/affine_space/affine_equiv): lemmas about coercion to `affine_map` (#16284)

feat(linear_algebra/affine_space/affine_equiv): lemmas about coercion to `affine_map` (#16284) Add two more `rfl` (and `simp`) lemmas about the coercion from `affine_equiv` to `affine_map`. In both cases very similar lemmas are already present (in one case a version using `to_affine_map`, in one case a version for the coercion to a function), but apparently not these particular ones.