Commit 2020-06-05 08:41 edb4422a

View on Github →

feat(algebra/add_torsor): add equiv.const_vadd and equiv.vadd_const (#2907) Also define their isometric.* versions in analysis/normed_space/add_torsor.

Estimated changes

Modified src/algebra/add_torsor.lean

added theorem add_torsor.vadd_vsub_vadd_cancel_left

added theorem add_torsor.vadd_vsub_vadd_cancel_right

added theorem add_torsor.vsub_sub_vsub_cancel_left

added theorem add_torsor.vsub_sub_vsub_cancel_right

deleted theorem add_torsor.vsub_sub_vsub_left_cancel

deleted theorem add_torsor.vsub_sub_vsub_right_cancel

added theorem equiv.coe_const_vadd

added theorem equiv.coe_vadd_const

added theorem equiv.coe_vadd_const_symm

added def equiv.const_vadd

added theorem equiv.const_vadd_add

added def equiv.const_vadd_hom

added theorem equiv.const_vadd_zero

added def equiv.vadd_const

Modified src/analysis/normed_space/add_torsor.lean

added theorem dist_vadd_cancel_left

added theorem dist_vadd_cancel_right

added theorem isometric.coe_const_vadd

added theorem isometric.coe_vadd_const

added theorem isometric.coe_vadd_const_symm

added def isometric.const_vadd

added theorem isometric.const_vadd_zero

added def isometric.vadd_const

added theorem isometric.vadd_const_to_equiv