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