Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-10-21 15:31 1b4e7694

View on Github →

feat(linear_algebra/affine_space): define affine_equiv (#2909) Define

  • affine_equiv to be an invertible affine map (e.g., extend both affine_map and equiv);
  • conversion to linear_equiv;
  • group structure on affine automorphisms;
  • prove standard lemmas for equivalences (apply_symm_apply, symm_apply_eq etc). API changes
  • make G implicit in equiv.vadd_const.

Estimated changes

modified theorem equiv.coe_vadd_const
modified theorem equiv.coe_vadd_const_symm
added theorem affine_equiv.coe_mul
added theorem affine_equiv.coe_one
added theorem affine_equiv.coe_refl
added theorem affine_equiv.coe_trans
added theorem affine_equiv.ext
added theorem affine_equiv.inv_def
added theorem affine_equiv.map_vadd
added theorem affine_equiv.mul_def
added theorem affine_equiv.one_def
added theorem affine_equiv.range_eq
added theorem affine_equiv.symm_refl
added structure affine_equiv