Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-26 23:31 add068d1

View on Github →

chore(linear_algebra/orientation): split into 2 files (#12302) Move parts that don't need multilinear maps to a new file.

Estimated changes

deleted theorem equiv_iff_same_ray
deleted theorem equivalence_same_ray
deleted theorem module.ray.ind
deleted def module.ray.map
deleted theorem module.ray.map_apply
deleted theorem module.ray.map_refl
deleted theorem module.ray.map_symm
deleted theorem module.ray.ne_neg_self
deleted def module.ray
deleted theorem ray_eq_iff
deleted theorem ray_neg
deleted theorem ray_pos_smul
deleted theorem ray_vector.coe_neg
deleted theorem ray_vector.equiv_neg_iff
deleted def ray_vector
deleted theorem same_ray.map
deleted theorem same_ray.neg
deleted theorem same_ray.pos_smul_left
deleted theorem same_ray.pos_smul_right
deleted theorem same_ray.refl
deleted theorem same_ray.smul
deleted theorem same_ray.symm
deleted theorem same_ray.trans
deleted def same_ray
deleted theorem same_ray_comm
deleted theorem same_ray_iff_mem_orbit
deleted theorem same_ray_map_iff
deleted theorem same_ray_neg_iff
deleted theorem same_ray_neg_swap
deleted theorem same_ray_of_mem_orbit
deleted theorem same_ray_pos_smul_left
deleted theorem same_ray_pos_smul_right
deleted def same_ray_setoid
deleted theorem same_ray_smul_left_iff
deleted theorem same_ray_smul_right_iff
deleted theorem smul_ray_of_ne_zero
deleted theorem units_inv_smul
deleted theorem units_smul_eq_neg_iff
deleted theorem units_smul_eq_self_iff
added theorem equiv_iff_same_ray
added theorem equivalence_same_ray
added theorem module.ray.ind
added def module.ray.map
added theorem module.ray.map_apply
added theorem module.ray.map_refl
added theorem module.ray.map_symm
added theorem module.ray.ne_neg_self
added def module.ray
added theorem ray_eq_iff
added theorem ray_neg
added theorem ray_pos_smul
added theorem ray_vector.coe_neg
added def ray_vector
added theorem same_ray.map
added theorem same_ray.neg
added theorem same_ray.pos_smul_left
added theorem same_ray.refl
added theorem same_ray.smul
added theorem same_ray.symm
added theorem same_ray.trans
added def same_ray
added theorem same_ray_comm
added theorem same_ray_iff_mem_orbit
added theorem same_ray_map_iff
added theorem same_ray_neg_iff
added theorem same_ray_neg_swap
added theorem same_ray_of_mem_orbit
added theorem same_ray_pos_smul_left
added def same_ray_setoid
added theorem same_ray_smul_left_iff
added theorem smul_ray_of_ne_zero
added theorem units_inv_smul
added theorem units_smul_eq_neg_iff
added theorem units_smul_eq_self_iff