Commit 2024-01-24 02:51 0faddd84

View on Github →

feat: n • v and v are on the same ray (#9104) From LeanAPAP

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/GroupPower/CovariantClass.lean

added theorem pow_lt_pow_left'

Created Mathlib/Algebra/Order/Module/Algebra.lean

added theorem algebraMap_le_algebraMap

added theorem algebraMap_lt_algebraMap

added theorem algebraMap_mono

added theorem algebraMap_nonneg

added theorem algebraMap_pos

added theorem algebraMap_strictMono

Modified Mathlib/Algebra/Order/Module/Defs.lean

Modified Mathlib/Analysis/InnerProductSpace/TwoDim.lean

Modified Mathlib/Data/IsROrC/Basic.lean

added theorem IsROrC.norm_nsmul

Modified Mathlib/LinearAlgebra/Ray.lean

modified theorem SameRay.nonneg_smul_left

modified theorem SameRay.nonneg_smul_right

modified theorem SameRay.pos_smul_left

modified theorem SameRay.pos_smul_right

modified theorem SameRay.sameRay_nonneg_smul_left

modified theorem SameRay.sameRay_nonneg_smul_right

modified theorem SameRay.sameRay_pos_smul_left

modified theorem SameRay.sameRay_pos_smul_right