Commit 2020-08-15 12:06 36b4a1e3

View on Github →

refactor(algebra/add_torsor): use out_param (#3727)

Estimated changes

deleted theorem add_action.vadd_assoc
deleted theorem add_action.vadd_comm
deleted theorem add_action.zero_vadd
deleted theorem add_torsor.vadd_vsub
deleted theorem add_torsor.vsub_self
deleted def add_torsor.vsub_set
deleted theorem add_torsor.vsub_set_empty
deleted theorem add_torsor.vsub_set_mono
deleted theorem add_torsor.vsub_vadd
added theorem eq_of_vsub_eq_zero
added theorem eq_vadd_iff_vsub_eq
added theorem neg_vsub_eq_vsub_rev
added theorem vadd_assoc
added theorem vadd_comm
modified theorem vadd_eq_add
added theorem vadd_left_cancel
added theorem vadd_left_cancel_iff
added theorem vadd_right_cancel
added theorem vadd_right_cancel_iff
added theorem vadd_vsub
added theorem vadd_vsub_assoc
added theorem vsub_add_vsub_cancel
modified theorem vsub_eq_sub
added theorem vsub_eq_zero_iff_eq
added theorem vsub_left_cancel
added theorem vsub_left_cancel_iff
added theorem vsub_mem_vsub_set
added theorem vsub_right_cancel
added theorem vsub_right_cancel_iff
added theorem vsub_self
added def vsub_set
added theorem vsub_set_empty
added theorem vsub_set_mono
added theorem vsub_set_singleton
added theorem vsub_vadd
added theorem vsub_vadd_eq_vsub_sub
added theorem zero_vadd
modified theorem affine_map.add_linear
modified theorem affine_map.coe_add
modified theorem affine_map.coe_comp
modified theorem affine_map.coe_const
modified theorem affine_map.coe_id
modified theorem affine_map.coe_mul
modified theorem affine_map.coe_one
modified theorem affine_map.coe_smul
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 def affine_map.const
modified theorem affine_map.const_linear
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.homothety
modified theorem affine_map.homothety_apply
modified theorem affine_map.homothety_one
modified theorem affine_map.homothety_zero
modified def affine_map.id
modified theorem affine_map.id_apply
modified theorem affine_map.id_comp
modified theorem affine_map.id_linear
modified def affine_map.line_map
modified theorem affine_map.line_map_zero
modified theorem affine_map.linear_map_vsub
modified theorem affine_map.map_vadd
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
modified structure affine_map
deleted def affine_space
modified def affine_span
added theorem affine_span_nonempty
modified theorem affine_subspace.bot_coe
modified theorem affine_subspace.ext
modified theorem affine_subspace.inf_coe
modified theorem affine_subspace.le_def'
modified theorem affine_subspace.le_def
modified theorem affine_subspace.lt_def
modified theorem affine_subspace.mem_coe
modified theorem affine_subspace.mem_inf_iff
modified theorem affine_subspace.mem_top
modified def affine_subspace.mk'
modified theorem affine_subspace.mk'_eq
modified theorem affine_subspace.not_mem_bot
modified theorem affine_subspace.span_empty
modified theorem affine_subspace.span_union
modified theorem affine_subspace.span_univ
modified theorem affine_subspace.top_coe
modified structure affine_subspace
modified theorem direction_affine_span
modified theorem mem_affine_span
added theorem mem_span_points
added def span_points
added theorem span_points_nonempty
added theorem subset_span_points
added def vector_span
added theorem vector_span_def
added theorem vector_span_empty
added theorem vector_span_singleton
added theorem vsub_mem_vector_span