Mathlib Changelog
v4
Changelog
About
Github
Commit
2023-03-07 21:44
161a7501
View on Github →
feat: port LinearAlgebra.AffineSpace.AffineMap (
#2570
)
Estimated changes
Modified
Mathlib.lean
Created
Mathlib/LinearAlgebra/AffineSpace/AffineMap.lean
added
theorem
AffineMap.add_linear
added
theorem
AffineMap.apply_lineMap
added
theorem
AffineMap.coeFn_injective
added
theorem
AffineMap.coe_add
added
theorem
AffineMap.coe_comp
added
theorem
AffineMap.coe_const
added
theorem
AffineMap.coe_fst
added
theorem
AffineMap.coe_homothetyAffine
added
theorem
AffineMap.coe_homothetyHom
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.homothety
added
def
AffineMap.homothetyAffine
added
def
AffineMap.homothetyHom
added
theorem
AffineMap.homothety_add
added
theorem
AffineMap.homothety_apply
added
theorem
AffineMap.homothety_apply_same
added
theorem
AffineMap.homothety_def
added
theorem
AffineMap.homothety_eq_lineMap
added
theorem
AffineMap.homothety_mul
added
theorem
AffineMap.homothety_mul_apply
added
theorem
AffineMap.homothety_one
added
theorem
AffineMap.homothety_zero
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.image_vsub_image
added
theorem
AffineMap.left_vsub_lineMap
added
def
AffineMap.lineMap
added
theorem
AffineMap.lineMap_apply
added
theorem
AffineMap.lineMap_apply_module'
added
theorem
AffineMap.lineMap_apply_module
added
theorem
AffineMap.lineMap_apply_one
added
theorem
AffineMap.lineMap_apply_one_sub
added
theorem
AffineMap.lineMap_apply_ring'
added
theorem
AffineMap.lineMap_apply_ring
added
theorem
AffineMap.lineMap_apply_zero
added
theorem
AffineMap.lineMap_eq_left_iff
added
theorem
AffineMap.lineMap_eq_lineMap_iff
added
theorem
AffineMap.lineMap_eq_right_iff
added
theorem
AffineMap.lineMap_injective
added
theorem
AffineMap.lineMap_linear
added
theorem
AffineMap.lineMap_same
added
theorem
AffineMap.lineMap_same_apply
added
theorem
AffineMap.lineMap_symm
added
theorem
AffineMap.lineMap_vadd_apply
added
theorem
AffineMap.lineMap_vadd_lineMap
added
theorem
AffineMap.lineMap_vsub_left
added
theorem
AffineMap.lineMap_vsub_lineMap
added
theorem
AffineMap.lineMap_vsub_right
added
def
AffineMap.linearHom
added
theorem
AffineMap.linearMap_vsub
added
theorem
AffineMap.linear_bijective_iff
added
theorem
AffineMap.linear_eq_zero_iff_exists_const
added
theorem
AffineMap.linear_injective_iff
added
theorem
AffineMap.linear_surjective_iff
added
theorem
AffineMap.map_vadd
added
def
AffineMap.mk'
added
theorem
AffineMap.mk'_linear
added
theorem
AffineMap.neg_linear
added
theorem
AffineMap.pi_lineMap_apply
added
def
AffineMap.proj
added
theorem
AffineMap.proj_apply
added
theorem
AffineMap.proj_linear
added
theorem
AffineMap.right_vsub_lineMap
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
def
AffineMap.toConstProdLinearMap
added
theorem
AffineMap.vadd_apply
added
theorem
AffineMap.vsub_apply
added
theorem
AffineMap.zero_linear
added
structure
AffineMap
added
theorem
Convex.combo_affine_apply
added
theorem
LinearMap.coe_toAffineMap
added
def
LinearMap.toAffineMap
added
theorem
LinearMap.toAffineMap_linear