Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-17 05:18 877f2e7a

View on Github →

refactor(linear_algebra/ray): redefine same_ray to allow zero vectors (#12618) In a strictly convex space, the new definition is equivalent to the fact that the triangle inequality becomes an equality. The old definition was only used for nonzero vectors in mathlib. Also make the definition of ray_vector semireducible so that ray_vector.setoid can be an instance.

Estimated changes

Modified src/analysis/convex/basic.lean

added theorem mem_segment_iff_same_ray

added theorem same_ray_of_mem_segment

modified theorem segment_same

Created src/analysis/normed_space/ray.lean

added theorem same_ray.norm_add

added theorem same_ray.norm_smul_eq

added theorem same_ray.norm_sub

added theorem same_ray_iff_inv_norm_smul_eq

added theorem same_ray_iff_inv_norm_smul_eq_of_ne

added theorem same_ray_iff_norm_smul_eq

Modified src/linear_algebra/orientation.lean

modified theorem basis.map_orientation_eq_det_inv_smul

modified def orientation.map

modified theorem orientation.map_apply

modified theorem orientation.map_refl

modified theorem orientation.map_symm

modified def orientation

Modified src/linear_algebra/ray.lean

added theorem eq_zero_of_same_ray_neg_smul_right

modified theorem eq_zero_of_same_ray_self_neg

modified theorem equiv_iff_same_ray

deleted theorem equivalence_same_ray

modified theorem module.ray.ind

modified def module.ray.map

modified theorem module.ray.map_apply

modified theorem module.ray.map_refl

modified theorem module.ray.map_symm

modified theorem module.ray.ne_neg_self

added theorem module.ray.neg_units_smul

modified def module.ray.some_ray_vector

modified theorem module.ray.some_ray_vector_ray

modified def module.ray.some_vector

modified theorem module.ray.some_vector_ne_zero

modified theorem module.ray.some_vector_ray

modified theorem module.ray.units_smul_of_neg

modified theorem module.ray.units_smul_of_pos

modified def module.ray

added theorem neg_ray_of_ne_zero

modified theorem ray_eq_iff

deleted theorem ray_neg

modified theorem ray_pos_smul

modified theorem ray_vector.coe_neg

modified theorem ray_vector.equiv_neg_iff

modified def ray_vector.map_linear_equiv

deleted def ray_vector.same_ray_setoid

modified def ray_vector

added theorem same_ray.add_left

added theorem same_ray.add_right

added theorem same_ray.exists_eq_smul

added theorem same_ray.exists_eq_smul_add

added theorem same_ray.exists_left_eq_smul

added theorem same_ray.exists_pos

added theorem same_ray.exists_right_eq_smul

modified theorem same_ray.map

deleted theorem same_ray.neg

added theorem same_ray.nonneg_smul_left

added theorem same_ray.nonneg_smul_right

added theorem same_ray.of_subsingleton'

added theorem same_ray.of_subsingleton

modified theorem same_ray.pos_smul_left

modified theorem same_ray.pos_smul_right

modified theorem same_ray.refl

modified theorem same_ray.smul

modified theorem same_ray.symm

modified theorem same_ray.trans

added theorem same_ray.zero_left

added theorem same_ray.zero_right

modified theorem same_ray_comm

deleted theorem same_ray_iff_mem_orbit

modified theorem same_ray_map_iff

modified theorem same_ray_neg_iff

modified theorem same_ray_neg_smul_left_iff

added theorem same_ray_neg_smul_left_iff_of_ne

modified theorem same_ray_neg_smul_right_iff

added theorem same_ray_neg_smul_right_iff_of_ne

modified theorem same_ray_neg_swap

added theorem same_ray_nonneg_smul_left

added theorem same_ray_nonneg_smul_right

modified theorem same_ray_pos_smul_left

modified theorem same_ray_pos_smul_right

deleted def same_ray_setoid

deleted theorem same_ray_setoid_eq_orbit_rel

modified theorem same_ray_smul_left_iff

added theorem same_ray_smul_left_iff_of_ne

modified theorem same_ray_smul_right_iff

added theorem same_ray_smul_right_iff_of_ne