Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-18 18:09 a6179f61

View on Github →

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

Estimated changes