Commit 2020-10-18 21:34 61e1111d

View on Github →

chore(linear_algebra/affine_space): introduce notation for affine_map (#4675)

Estimated changes

modified theorem affine_map.add_linear
modified theorem affine_map.apply_line_map
modified theorem affine_map.coe_add
modified theorem affine_map.coe_comp
modified theorem affine_map.coe_fst
modified theorem affine_map.coe_mul
modified theorem affine_map.coe_one
modified theorem affine_map.coe_smul
modified theorem affine_map.coe_snd
modified theorem affine_map.coe_zero
modified def affine_map.comp
modified theorem affine_map.comp_apply
modified theorem affine_map.comp_assoc
modified theorem affine_map.comp_id
modified theorem affine_map.comp_line_map
modified def affine_map.const
modified theorem affine_map.decomp'
modified theorem affine_map.decomp
modified theorem affine_map.ext
modified theorem affine_map.ext_iff
modified def affine_map.fst
modified theorem affine_map.fst_linear
modified def affine_map.homothety
modified def affine_map.id
modified theorem affine_map.id_comp
modified theorem affine_map.image_interval
modified def affine_map.line_map
modified theorem affine_map.linear_map_vsub
modified theorem affine_map.map_vadd
modified def affine_map.snd
modified theorem affine_map.snd_linear
modified theorem affine_map.to_fun_eq_coe
modified theorem affine_map.vadd_apply
modified theorem affine_map.vsub_apply
modified theorem affine_map.zero_linear