Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-15 12:06 36b4a1e3

View on Github →

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

Estimated changes

Modified src/algebra/add_torsor.lean

deleted theorem add_action.vadd_assoc

deleted theorem add_action.vadd_comm

deleted theorem add_action.vadd_left_cancel

deleted theorem add_action.vadd_left_cancel_iff

deleted theorem add_action.zero_vadd

deleted theorem add_torsor.eq_of_vsub_eq_zero

deleted theorem add_torsor.eq_vadd_iff_vsub_eq

deleted theorem add_torsor.neg_vsub_eq_vsub_rev

deleted theorem add_torsor.vadd_right_cancel

deleted theorem add_torsor.vadd_right_cancel_iff

deleted theorem add_torsor.vadd_vsub

deleted theorem add_torsor.vadd_vsub_assoc

deleted theorem add_torsor.vadd_vsub_vadd_cancel_left

deleted theorem add_torsor.vadd_vsub_vadd_cancel_right

deleted theorem add_torsor.vsub_add_vsub_cancel

deleted theorem add_torsor.vsub_eq_zero_iff_eq

deleted theorem add_torsor.vsub_left_cancel

deleted theorem add_torsor.vsub_left_cancel_iff

deleted theorem add_torsor.vsub_mem_vsub_set

deleted theorem add_torsor.vsub_right_cancel

deleted theorem add_torsor.vsub_right_cancel_iff

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_finite_of_finite

deleted theorem add_torsor.vsub_set_mono

deleted theorem add_torsor.vsub_set_singleton

deleted theorem add_torsor.vsub_sub_vsub_cancel_left

deleted theorem add_torsor.vsub_sub_vsub_cancel_right

deleted theorem add_torsor.vsub_vadd

deleted theorem add_torsor.vsub_vadd_eq_vsub_sub

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 vadd_vsub_vadd_cancel_left

added theorem vadd_vsub_vadd_cancel_right

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_finite_of_finite

added theorem vsub_set_mono

added theorem vsub_set_singleton

added theorem vsub_sub_vsub_cancel_left

added theorem vsub_sub_vsub_cancel_right

added theorem vsub_vadd

added theorem vsub_vadd_eq_vsub_sub

added theorem zero_vadd

Modified src/analysis/convex/basic.lean

modified theorem convex.affine_image

modified theorem convex.affine_preimage

modified theorem convex.combo_affine_apply

modified theorem convex_on.comp_affine_map

Modified src/analysis/convex/extrema.lean

Modified src/analysis/normed_space/add_torsor.lean

deleted theorem add_torsor.dist_eq_norm

added theorem dist_eq_norm_vsub

modified theorem dist_vadd_cancel_left

modified theorem dist_vadd_cancel_right

modified theorem isometric.coe_vadd_const

modified theorem isometric.coe_vadd_const_symm

deleted theorem isometric.isometry_vadd_vsub_of_isometry

modified theorem isometric.vadd_const_to_equiv

added theorem isometry.vadd_vsub

Modified src/analysis/normed_space/mazur_ulam.lean

modified theorem isometric.coe_to_affine_map

modified def isometric.to_affine_map

Modified src/geometry/euclidean.lean

deleted def euclidean_affine_space

modified theorem euclidean_geometry.angle_add_angle_eq_pi_of_angle_eq_pi

modified theorem euclidean_geometry.angle_comm

modified theorem euclidean_geometry.angle_eq_angle_of_angle_eq_pi

modified theorem euclidean_geometry.angle_eq_left

modified theorem euclidean_geometry.angle_eq_of_ne

modified theorem euclidean_geometry.angle_eq_right

modified theorem euclidean_geometry.angle_eq_zero_of_angle_eq_pi_left

modified theorem euclidean_geometry.angle_eq_zero_of_angle_eq_pi_right

modified theorem euclidean_geometry.angle_le_pi

modified theorem euclidean_geometry.angle_nonneg

modified theorem euclidean_geometry.dist_eq_of_angle_eq_angle_of_angle_ne_pi

modified theorem euclidean_geometry.dist_orthogonal_projection_eq_zero_iff

modified theorem euclidean_geometry.dist_orthogonal_projection_ne_zero_of_not_mem

modified theorem euclidean_geometry.dist_square_smul_orthogonal_vadd_smul_orthogonal_vadd

modified theorem euclidean_geometry.inter_eq_singleton_orthogonal_projection

modified theorem euclidean_geometry.inter_eq_singleton_orthogonal_projection_fn

modified def euclidean_geometry.orthogonal_projection

modified theorem euclidean_geometry.orthogonal_projection_eq_self_iff

modified def euclidean_geometry.orthogonal_projection_fn

modified theorem euclidean_geometry.orthogonal_projection_fn_eq

modified theorem euclidean_geometry.orthogonal_projection_fn_mem

modified theorem euclidean_geometry.orthogonal_projection_fn_mem_orthogonal

modified theorem euclidean_geometry.orthogonal_projection_fn_vsub_mem_direction_orthogonal

modified theorem euclidean_geometry.orthogonal_projection_mem

modified theorem euclidean_geometry.orthogonal_projection_mem_orthogonal

modified theorem euclidean_geometry.orthogonal_projection_vadd_eq_self

modified theorem euclidean_geometry.orthogonal_projection_vadd_smul_vsub_orthogonal_projection

modified theorem euclidean_geometry.orthogonal_projection_vsub_mem_direction

modified theorem euclidean_geometry.orthogonal_projection_vsub_mem_direction_orthogonal

modified theorem euclidean_geometry.vsub_orthogonal_projection_mem_direction

modified theorem euclidean_geometry.vsub_orthogonal_projection_mem_direction_orthogonal

Modified src/linear_algebra/affine_space/basic.lean

modified theorem affine_map.add_linear

modified theorem affine_map.affine_apply_line_map

modified theorem affine_map.affine_comp_line_map

modified theorem affine_map.coe_add

modified theorem affine_map.coe_comp

modified theorem affine_map.coe_const

modified theorem affine_map.coe_homothety_hom

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 def affine_map.homothety_affine

modified theorem affine_map.homothety_apply

modified def affine_map.homothety_hom

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 theorem affine_space.affine_span_nonempty

deleted theorem affine_space.mem_span_points

deleted def affine_space.span_points

deleted theorem affine_space.span_points_nonempty

deleted theorem affine_space.subset_span_points

deleted theorem affine_space.vadd_mem_span_points_of_mem_span_points_of_mem_vector_span

deleted def affine_space.vector_span

deleted theorem affine_space.vector_span_def

deleted theorem affine_space.vector_span_empty

deleted theorem affine_space.vector_span_eq_span_vsub_set_left

deleted theorem affine_space.vector_span_eq_span_vsub_set_right

deleted theorem affine_space.vector_span_range_eq_span_range_vsub_left

deleted theorem affine_space.vector_span_range_eq_span_range_vsub_right

deleted theorem affine_space.vector_span_singleton

deleted theorem affine_space.vsub_mem_vector_span

deleted theorem affine_space.vsub_mem_vector_span_of_mem_span_points_of_mem_span_points

deleted theorem affine_space.vsub_set_subset_vector_span

deleted def affine_space

modified def affine_span

added theorem affine_span_nonempty

modified theorem affine_subspace.affine_span_coe

modified theorem affine_subspace.affine_span_eq_Inf

modified theorem affine_subspace.bot_coe

modified theorem affine_subspace.coe_affine_span_singleton

modified theorem affine_subspace.coe_direction_eq_vsub_set

modified theorem affine_subspace.coe_direction_eq_vsub_set_left

modified theorem affine_subspace.coe_direction_eq_vsub_set_right

modified def affine_subspace.direction

modified theorem affine_subspace.direction_affine_span_insert

modified theorem affine_subspace.direction_bot

modified theorem affine_subspace.direction_eq_vector_span

modified theorem affine_subspace.direction_inf

modified theorem affine_subspace.direction_le

modified theorem affine_subspace.direction_lt_of_nonempty

modified def affine_subspace.direction_of_nonempty

modified theorem affine_subspace.direction_of_nonempty_eq_direction

modified theorem affine_subspace.direction_sup

modified theorem affine_subspace.direction_top

modified theorem affine_subspace.exists_of_lt

modified theorem affine_subspace.ext

modified theorem affine_subspace.ext_of_direction_eq

modified theorem affine_subspace.inf_coe

modified theorem affine_subspace.inter_eq_singleton_of_nonempty_of_is_compl

modified theorem affine_subspace.inter_nonempty_of_nonempty_of_sup_direction_eq_top

modified theorem affine_subspace.le_def'

modified theorem affine_subspace.le_def

modified theorem affine_subspace.lt_def

modified theorem affine_subspace.lt_iff_le_and_exists

modified theorem affine_subspace.mem_affine_span_insert_iff

modified theorem affine_subspace.mem_coe

modified theorem affine_subspace.mem_direction_iff_eq_vsub

modified theorem affine_subspace.mem_direction_iff_eq_vsub_left

modified theorem affine_subspace.mem_direction_iff_eq_vsub_right

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_le_iff_exists

modified theorem affine_subspace.not_mem_bot

modified theorem affine_subspace.span_empty

modified theorem affine_subspace.span_points_subset_coe_of_subset_coe

modified theorem affine_subspace.span_union

modified theorem affine_subspace.span_univ

modified theorem affine_subspace.sup_direction_le

modified theorem affine_subspace.sup_direction_lt_of_nonempty_of_inter_empty

modified theorem affine_subspace.top_coe

modified theorem affine_subspace.vadd_mem_of_mem_direction

modified theorem affine_subspace.vsub_left_mem_direction_iff_mem

modified theorem affine_subspace.vsub_mem_direction

modified theorem affine_subspace.vsub_right_mem_direction_iff_mem

modified structure affine_subspace

modified theorem direction_affine_span

modified def linear_map.to_affine_map

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 theorem vadd_mem_span_points_of_mem_span_points_of_mem_vector_span

added def vector_span

added theorem vector_span_def

added theorem vector_span_empty

added theorem vector_span_eq_span_vsub_set_left

added theorem vector_span_eq_span_vsub_set_right

added theorem vector_span_range_eq_span_range_vsub_left

added theorem vector_span_range_eq_span_range_vsub_right

added theorem vector_span_singleton

added theorem vsub_mem_vector_span

added theorem vsub_mem_vector_span_of_mem_span_points_of_mem_span_points

added theorem vsub_set_subset_vector_span

Modified src/linear_algebra/affine_space/combination.lean

added theorem affine_combination_mem_affine_span

modified def affine_map.weighted_vsub_of_point

deleted theorem affine_space.affine_combination_mem_affine_span

deleted theorem affine_space.eq_affine_combination_of_mem_affine_span

deleted theorem affine_space.mem_affine_span_iff_eq_affine_combination

deleted theorem affine_space.mem_vector_span_iff_eq_weighted_vsub

deleted theorem affine_space.weighted_vsub_mem_vector_span

added theorem eq_affine_combination_of_mem_affine_span

added theorem mem_affine_span_iff_eq_affine_combination

added theorem mem_vector_span_iff_eq_weighted_vsub

added theorem weighted_vsub_mem_vector_span

Modified src/linear_algebra/affine_space/finite_dimensional.lean

deleted theorem affine_space.finite_dimensional_direction_affine_span_of_finite

deleted theorem affine_space.finite_dimensional_vector_span_of_finite

added theorem finite_dimensional_direction_affine_span_of_finite

added theorem finite_dimensional_vector_span_of_finite

Modified src/linear_algebra/affine_space/independent.lean

added theorem affine.simplex.ext

added theorem affine.simplex.ext_iff

added def affine.simplex.face

added theorem affine.simplex.face_eq_mk_of_point

added theorem affine.simplex.face_points

added def affine.simplex.mk_of_point

added theorem affine.simplex.mk_of_point_points

added structure affine.simplex

added def affine.triangle

deleted theorem affine_space.simplex.ext

deleted theorem affine_space.simplex.ext_iff

deleted def affine_space.simplex.face

deleted theorem affine_space.simplex.face_eq_mk_of_point

deleted theorem affine_space.simplex.face_points

deleted def affine_space.simplex.mk_of_point

deleted theorem affine_space.simplex.mk_of_point_points

deleted structure affine_space.simplex

deleted def affine_space.triangle

Modified src/topology/algebra/affine.lean

modified theorem affine_map.continuous_iff