InnerProductGeometry.angle_smul_right_of_pos
∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V) {r : ℝ},
0 < r → InnerProductGeometry.angle x (r • y) = InnerProductGeometry.angle x yThe angle between a vector and a positive multiple of a vector.
- Cited by
- 6 results in Mathlib
- Foundations
- Depth 189 from the axioms · uses propext, Classical.choice, Quot.sound
Around this declaration
Dashed lines are statement dependencies; solid lines are citations in proofs.
Cites16
Mathlib declarations this one mentions in its statement or cites explicitly in its proof. Plumbing is filtered out.
- Realstatement and proof · cited by 25,697
- NormedAddCommGroupstatement and proof · cited by 15,752
- Norm.normproof · cited by 5,413
- InnerProductSpacestatement and proof · cited by 3,523
- mul_commproof · cited by 2,262
- mul_assocproof · cited by 1,667
- le_of_ltproof · cited by 1,175
- Inner.innerproof · cited by 1,089
- ne_of_gtproof · cited by 637
- abs_of_nonnegproof · cited by 279
- norm_smulproof · cited by 242
- InnerProductGeometry.anglestatement · cited by 170
Cited by6
Results whose statement or proof uses this declaration.
- InnerProductGeometry.angle_smul_left_of_posproof · cited by 4
- EuclideanGeometry.angle_smul_right_of_posproof · cited by 2
- InnerProductGeometry.angle_smul_right_of_negproof · cited by 2
- InnerProductGeometry.angle_eq_angle_add_add_angle_add_of_mem_spanproof · cited by 1
- Orientation.angle_eq_iff_oangle_eq_or_sameRayproof · cited by 1
- EuclideanGeometry.angle_homothetyproof · cited by 0