Commit 2023-03-07 21:44 161a7501

View on Github →

feat: port LinearAlgebra.AffineSpace.AffineMap (#2570)

Estimated changes

added theorem AffineMap.add_linear
added theorem AffineMap.coe_add
added theorem AffineMap.coe_comp
added theorem AffineMap.coe_const
added theorem AffineMap.coe_fst
added theorem AffineMap.coe_id
added theorem AffineMap.coe_lineMap
added theorem AffineMap.coe_mk'
added theorem AffineMap.coe_mk
added theorem AffineMap.coe_mul
added theorem AffineMap.coe_neg
added theorem AffineMap.coe_one
added theorem AffineMap.coe_smul
added theorem AffineMap.coe_snd
added theorem AffineMap.coe_sub
added theorem AffineMap.coe_zero
added def AffineMap.comp
added theorem AffineMap.comp_apply
added theorem AffineMap.comp_assoc
added theorem AffineMap.comp_id
added theorem AffineMap.comp_lineMap
added def AffineMap.const
added theorem AffineMap.const_apply
added theorem AffineMap.const_linear
added theorem AffineMap.decomp'
added theorem AffineMap.decomp
added theorem AffineMap.ext
added theorem AffineMap.ext_iff
added def AffineMap.fst
added theorem AffineMap.fst_lineMap
added theorem AffineMap.fst_linear
added def AffineMap.id
added theorem AffineMap.id_apply
added theorem AffineMap.id_comp
added theorem AffineMap.id_linear
added theorem AffineMap.image_uIcc
added theorem AffineMap.lineMap_same
added theorem AffineMap.lineMap_symm
added theorem AffineMap.map_vadd
added def AffineMap.mk'
added theorem AffineMap.mk'_linear
added theorem AffineMap.neg_linear
added def AffineMap.proj
added theorem AffineMap.proj_apply
added theorem AffineMap.proj_linear
added theorem AffineMap.smul_linear
added def AffineMap.snd
added theorem AffineMap.snd_lineMap
added theorem AffineMap.snd_linear
added theorem AffineMap.sub_linear
added theorem AffineMap.vadd_apply
added theorem AffineMap.vsub_apply
added theorem AffineMap.zero_linear
added structure AffineMap