Mathlib Changelog
Changelog
About
Github
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