Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2020-06-12 18:08
ce594be5
View on Github →
feat(linear_algebra/affine_space): define a few affine maps (
#2981
)
Estimated changes
Modified
src/linear_algebra/affine_space.lean
added
theorem
affine_map.add_linear
added
theorem
affine_map.affine_apply_line_map
added
theorem
affine_map.affine_comp_line_map
added
theorem
affine_map.coe_add
added
theorem
affine_map.coe_const
added
theorem
affine_map.coe_homothety_affine
added
theorem
affine_map.coe_homothety_hom
added
theorem
affine_map.coe_mul
added
theorem
affine_map.coe_one
added
theorem
affine_map.coe_smul
added
theorem
affine_map.coe_zero
added
theorem
affine_map.comp_assoc
added
theorem
affine_map.comp_id
added
def
affine_map.const
added
theorem
affine_map.const_linear
modified
theorem
affine_map.ext
added
theorem
affine_map.ext_iff
added
def
affine_map.homothety
added
theorem
affine_map.homothety_add
added
def
affine_map.homothety_affine
added
theorem
affine_map.homothety_apply
added
theorem
affine_map.homothety_def
added
def
affine_map.homothety_hom
added
theorem
affine_map.homothety_mul
added
theorem
affine_map.homothety_one
added
theorem
affine_map.homothety_zero
added
theorem
affine_map.id_comp
added
theorem
affine_map.id_linear
added
def
affine_map.line_map
added
theorem
affine_map.line_map_apply
added
theorem
affine_map.line_map_apply_zero
added
theorem
affine_map.line_map_linear
added
theorem
affine_map.line_map_vadd_neg
added
theorem
affine_map.line_map_zero
added
theorem
affine_map.linear_map_vsub
deleted
theorem
affine_map.map_vsub
added
theorem
affine_map.vadd_apply
added
theorem
affine_map.vsub_apply
added
theorem
affine_map.zero_linear
added
theorem
linear_map.coe_to_affine_map
added
def
linear_map.to_affine_map
added
theorem
linear_map.to_affine_map_linear