Commit 2023-03-23 16:06 fef9b590

View on Github →

feat: port LinearAlgebra.AffineSpace.AffineEquiv (#2692) This ran into many of the problems that #2899 did, where simp would fail but simp [(foo)] or simp [foo _] would succeed.

Estimated changes

added theorem AffineEquiv.coeFn_inj
added theorem AffineEquiv.coe_coe
added theorem AffineEquiv.coe_linear
added theorem AffineEquiv.coe_mk'
added theorem AffineEquiv.coe_mk
added theorem AffineEquiv.coe_mul
added theorem AffineEquiv.coe_one
added theorem AffineEquiv.coe_refl
added theorem AffineEquiv.coe_trans
added theorem AffineEquiv.ext
added theorem AffineEquiv.image_symm
added theorem AffineEquiv.inv_def
added theorem AffineEquiv.linear_mk'
added theorem AffineEquiv.map_vadd
added def AffineEquiv.mk'
added theorem AffineEquiv.mul_def
added theorem AffineEquiv.one_def
added theorem AffineEquiv.range_eq
added def AffineEquiv.refl
added theorem AffineEquiv.refl_apply
added theorem AffineEquiv.refl_trans
added def AffineEquiv.symm
added theorem AffineEquiv.symm_refl
added theorem AffineEquiv.trans_refl
added structure AffineEquiv
added theorem AffineMap.lineMap_vadd
added theorem AffineMap.lineMap_vsub
added theorem AffineMap.vadd_lineMap
added theorem AffineMap.vsub_lineMap