Commit 2020-06-12 18:08 ce594be5

View on Github →

feat(linear_algebra/affine_space): define a few affine maps (#2981)

Estimated changes

added theorem affine_map.add_linear
added theorem affine_map.coe_add
added theorem affine_map.coe_const
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
modified theorem affine_map.ext
added theorem affine_map.ext_iff
added theorem affine_map.id_comp
added theorem affine_map.id_linear
deleted theorem affine_map.map_vsub
added theorem affine_map.vadd_apply
added theorem affine_map.vsub_apply
added theorem affine_map.zero_linear