Commit 2023-02-27 13:07 9777fdce

View on Github →

feat: port LinearAlgebra.Ray (#2468)

Estimated changes

Modified Mathlib.lean

Created Mathlib/LinearAlgebra/Ray.lean

added theorem Function.Injective.sameRay_map_iff

added theorem Module.Ray.ind

added theorem Module.Ray.linearEquiv_smul_eq_map

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 theorem Module.Ray.neg_units_smul

added def Module.Ray.someRayVector

added theorem Module.Ray.someRayVector_ray

added def Module.Ray.someVector

added theorem Module.Ray.someVector_ne_zero

added theorem Module.Ray.someVector_ray

added theorem Module.Ray.units_smul_of_neg

added theorem Module.Ray.units_smul_of_pos

added def Module.Ray

added theorem RayVector.coe_neg

added theorem RayVector.equiv_neg_iff

added def RayVector.mapLinearEquiv

added def RayVector

added theorem SameRay.add_left

added theorem SameRay.add_right

added theorem SameRay.exists_eq_smul

added theorem SameRay.exists_eq_smul_add

added theorem SameRay.exists_nonneg_left

added theorem SameRay.exists_nonneg_right

added theorem SameRay.exists_pos

added theorem SameRay.exists_pos_left

added theorem SameRay.exists_pos_right

added theorem SameRay.map

added theorem SameRay.nonneg_smul_left

added theorem SameRay.nonneg_smul_right

added theorem SameRay.of_subsingleton'

added theorem SameRay.of_subsingleton

added theorem SameRay.pos_smul_left

added theorem SameRay.pos_smul_right

added theorem SameRay.refl

added theorem SameRay.sameRay_comm

added theorem SameRay.sameRay_map_iff

added theorem SameRay.sameRay_nonneg_smul_left

added theorem SameRay.sameRay_nonneg_smul_right

added theorem SameRay.sameRay_pos_smul_left

added theorem SameRay.sameRay_pos_smul_right

added theorem SameRay.smul

added theorem SameRay.symm

added theorem SameRay.trans

added theorem SameRay.zero_left

added theorem SameRay.zero_right

added def SameRay

added theorem eq_zero_of_sameRay_neg_smul_right

added theorem eq_zero_of_sameRay_self_neg

added theorem equiv_iff_sameRay

added theorem exists_nonneg_left_iff_sameRay

added theorem exists_nonneg_right_iff_sameRay

added theorem exists_pos_left_iff_sameRay

added theorem exists_pos_left_iff_sameRay_and_ne_zero

added theorem exists_pos_right_iff_sameRay

added theorem exists_pos_right_iff_sameRay_and_ne_zero

added theorem neg_rayOfNeZero

added def rayOfNeZero

added theorem ray_eq_iff

added theorem ray_pos_smul

added theorem sameRay_neg_iff

added theorem sameRay_neg_smul_left_iff

added theorem sameRay_neg_smul_left_iff_of_ne

added theorem sameRay_neg_smul_right_iff

added theorem sameRay_neg_smul_right_iff_of_ne

added theorem sameRay_neg_swap

added theorem sameRay_of_mem_orbit

added theorem sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent

added theorem sameRay_or_sameRay_neg_iff_not_linearIndependent

added theorem sameRay_smul_left_iff

added theorem sameRay_smul_left_iff_of_ne

added theorem sameRay_smul_right_iff

added theorem sameRay_smul_right_iff_of_ne

added theorem smul_rayOfNeZero

added theorem units_inv_smul

added theorem units_smul_eq_neg_iff

added theorem units_smul_eq_self_iff