Rotations by oriented angles.

This file defines rotations by oriented angles in real inner product spaces.

Main definitions

• Orientation.rotation is the rotation by an oriented angle with respect to an orientation.

def Orientation.rotationAux {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) : V →ₗᵢ[ℝ] V

Auxiliary construction to build a rotation by the oriented angle θ.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Orientation.rotationAux_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) (x : V) : (Orientation.rotationAux o θ) x = Real.Angle.cos θ • x + Real.Angle.sin θ • (Orientation.rightAngleRotation o) x

def Orientation.rotation {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) : V ≃ₗᵢ[ℝ] V

A rotation by the oriented angle θ.

Equations

• One or more equations did not get rendered due to their size.

theorem Orientation.rotation_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) (x : V) : (Orientation.rotation o θ) x = Real.Angle.cos θ • x + Real.Angle.sin θ • (Orientation.rightAngleRotation o) x

theorem Orientation.rotation_symm_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) (x : V) : (LinearIsometryEquiv.symm (Orientation.rotation o θ)) x = Real.Angle.cos θ • x - Real.Angle.sin θ • (Orientation.rightAngleRotation o) x

theorem Orientation.rotation_eq_matrix_toLin {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) {x : V} (hx : x ≠ 0) : ↑(Orientation.rotation o θ).toLinearEquiv = (Matrix.toLin (Orientation.basisRightAngleRotation o x hx) (Orientation.basisRightAngleRotation o x hx)) (Matrix.of ![![Real.Angle.cos θ, -Real.Angle.sin θ], ![Real.Angle.sin θ, Real.Angle.cos θ]])

@[simp]

theorem Orientation.det_rotation {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) : LinearMap.det ↑(Orientation.rotation o θ).toLinearEquiv = 1

The determinant of rotation (as a linear map) is equal to 1.

@[simp]

theorem Orientation.linearEquiv_det_rotation {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) : LinearEquiv.det (Orientation.rotation o θ).toLinearEquiv = 1

The determinant of rotation (as a linear equiv) is equal to 1.

@[simp]

theorem Orientation.rotation_symm {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) : LinearIsometryEquiv.symm (Orientation.rotation o θ) = Orientation.rotation o (-θ)

The inverse of rotation is rotation by the negation of the angle.

@[simp]

theorem Orientation.rotation_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) : Orientation.rotation o 0 = LinearIsometryEquiv.refl ℝ V

Rotation by 0 is the identity.

@[simp]

theorem Orientation.rotation_pi {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) : Orientation.rotation o ↑Real.pi = LinearIsometryEquiv.neg ℝ

Rotation by π is negation.

theorem Orientation.rotation_pi_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) : (Orientation.rotation o ↑Real.pi) x = -x

Rotation by π is negation.

theorem Orientation.rotation_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) : Orientation.rotation o ↑(Real.pi / 2) = Orientation.rightAngleRotation o

Rotation by π / 2 is the "right-angle-rotation" map J.

@[simp]

theorem Orientation.rotation_rotation {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ₁ : Real.Angle) (θ₂ : Real.Angle) (x : V) : (Orientation.rotation o θ₁) ((Orientation.rotation o θ₂) x) = (Orientation.rotation o (θ₁ + θ₂)) x

Rotating twice is equivalent to rotating by the sum of the angles.

@[simp]

theorem Orientation.rotation_trans {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ₁ : Real.Angle) (θ₂ : Real.Angle) : LinearIsometryEquiv.trans (Orientation.rotation o θ₁) (Orientation.rotation o θ₂) = Orientation.rotation o (θ₂ + θ₁)

Rotating twice is equivalent to rotating by the sum of the angles.

@[simp]

theorem Orientation.kahler_rotation_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) (θ : Real.Angle) : ((Orientation.kahler o) ((Orientation.rotation o θ) x)) y = (starRingEnd ℂ) ↑(Real.Angle.expMapCircle θ) * ((Orientation.kahler o) x) y

Rotating the first of two vectors by θ scales their Kahler form by cos θ - sin θ * I.

theorem Orientation.neg_rotation {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) (x : V) : -(Orientation.rotation o θ) x = (Orientation.rotation o (↑Real.pi + θ)) x

Negating a rotation is equivalent to rotation by π plus the angle.

@[simp]

theorem Orientation.neg_rotation_neg_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) : -(Orientation.rotation o ↑(-Real.pi / 2)) x = (Orientation.rotation o ↑(Real.pi / 2)) x

Negating a rotation by -π / 2 is equivalent to rotation by π / 2.

theorem Orientation.neg_rotation_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) : -(Orientation.rotation o ↑(Real.pi / 2)) x = (Orientation.rotation o ↑(-Real.pi / 2)) x

Negating a rotation by π / 2 is equivalent to rotation by -π / 2.

theorem Orientation.kahler_rotation_left' {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) (θ : Real.Angle) : ((Orientation.kahler o) ((Orientation.rotation o θ) x)) y = ↑(Real.Angle.expMapCircle (-θ)) * ((Orientation.kahler o) x) y

Rotating the first of two vectors by θ scales their Kahler form by cos (-θ) + sin (-θ) * I.

@[simp]

theorem Orientation.kahler_rotation_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) (θ : Real.Angle) : ((Orientation.kahler o) x) ((Orientation.rotation o θ) y) = ↑(Real.Angle.expMapCircle θ) * ((Orientation.kahler o) x) y

Rotating the second of two vectors by θ scales their Kahler form by cos θ + sin θ * I.

@[simp]

theorem Orientation.oangle_rotation_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (hx : x ≠ 0) (hy : y ≠ 0) (θ : Real.Angle) : Orientation.oangle o ((Orientation.rotation o θ) x) y = Orientation.oangle o x y - θ

Rotating the first vector by θ subtracts θ from the angle between two vectors.

@[simp]

theorem Orientation.oangle_rotation_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (hx : x ≠ 0) (hy : y ≠ 0) (θ : Real.Angle) : Orientation.oangle o x ((Orientation.rotation o θ) y) = Orientation.oangle o x y + θ

Rotating the second vector by θ adds θ to the angle between two vectors.

@[simp]

theorem Orientation.oangle_rotation_self_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} (hx : x ≠ 0) (θ : Real.Angle) : Orientation.oangle o ((Orientation.rotation o θ) x) x = -θ

The rotation of a vector by θ has an angle of -θ from that vector.

@[simp]

theorem Orientation.oangle_rotation_self_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} (hx : x ≠ 0) (θ : Real.Angle) : Orientation.oangle o x ((Orientation.rotation o θ) x) = θ

A vector has an angle of θ from the rotation of that vector by θ.

@[simp]

theorem Orientation.oangle_rotation_oangle_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) : Orientation.oangle o ((Orientation.rotation o (Orientation.oangle o x y)) x) y = 0

Rotating the first vector by the angle between the two vectors results in an angle of 0.

@[simp]

theorem Orientation.oangle_rotation_oangle_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) : Orientation.oangle o y ((Orientation.rotation o (Orientation.oangle o x y)) x) = 0

Rotating the first vector by the angle between the two vectors and swapping the vectors results in an angle of 0.

@[simp]

theorem Orientation.oangle_rotation {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) (θ : Real.Angle) : Orientation.oangle o ((Orientation.rotation o θ) x) ((Orientation.rotation o θ) y) = Orientation.oangle o x y

Rotating both vectors by the same angle does not change the angle between those vectors.

@[simp]

theorem Orientation.rotation_eq_self_iff_angle_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} (hx : x ≠ 0) (θ : Real.Angle) : (Orientation.rotation o θ) x = x ↔ θ = 0

A rotation of a nonzero vector equals that vector if and only if the angle is zero.

@[simp]

theorem Orientation.eq_rotation_self_iff_angle_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} (hx : x ≠ 0) (θ : Real.Angle) : x = (Orientation.rotation o θ) x ↔ θ = 0

A nonzero vector equals a rotation of that vector if and only if the angle is zero.

theorem Orientation.rotation_eq_self_iff {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (θ : Real.Angle) : (Orientation.rotation o θ) x = x ↔ x = 0 ∨ θ = 0

A rotation of a vector equals that vector if and only if the vector or the angle is zero.

theorem Orientation.eq_rotation_self_iff {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (θ : Real.Angle) : x = (Orientation.rotation o θ) x ↔ x = 0 ∨ θ = 0

A vector equals a rotation of that vector if and only if the vector or the angle is zero.

@[simp]

theorem Orientation.rotation_oangle_eq_iff_norm_eq {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (y : V) : (Orientation.rotation o (Orientation.oangle o x y)) x = y ↔ ‖x‖ = ‖y‖

Rotating a vector by the angle to another vector gives the second vector if and only if the norms are equal.

theorem Orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_of_ne_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (hx : x ≠ 0) (hy : y ≠ 0) (θ : Real.Angle) : Orientation.oangle o x y = θ ↔ y = (‖y‖ / ‖x‖) • (Orientation.rotation o θ) x

The angle between two nonzero vectors is θ if and only if the second vector is the first rotated by θ and scaled by the ratio of the norms.

theorem Orientation.oangle_eq_iff_eq_pos_smul_rotation_of_ne_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (hx : x ≠ 0) (hy : y ≠ 0) (θ : Real.Angle) : Orientation.oangle o x y = θ ↔ ∃ (r : ℝ), 0 < r ∧ y = r • (Orientation.rotation o θ) x

The angle between two nonzero vectors is θ if and only if the second vector is the first rotated by θ and scaled by a positive real.

theorem Orientation.oangle_eq_iff_eq_norm_div_norm_smul_rotation_or_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (θ : Real.Angle) : Orientation.oangle o x y = θ ↔ x ≠ 0 ∧ y ≠ 0 ∧ y = (‖y‖ / ‖x‖) • (Orientation.rotation o θ) x ∨ θ = 0 ∧ (x = 0 ∨ y = 0)

The angle between two vectors is θ if and only if they are nonzero and the second vector is the first rotated by θ and scaled by the ratio of the norms, or θ and at least one of the vectors are zero.

theorem Orientation.oangle_eq_iff_eq_pos_smul_rotation_or_eq_zero {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} (θ : Real.Angle) : Orientation.oangle o x y = θ ↔ (x ≠ 0 ∧ y ≠ 0 ∧ ∃ (r : ℝ), 0 < r ∧ y = r • (Orientation.rotation o θ) x) ∨ θ = 0 ∧ (x = 0 ∨ y = 0)

The angle between two vectors is θ if and only if they are nonzero and the second vector is the first rotated by θ and scaled by a positive real, or θ and at least one of the vectors are zero.

theorem Orientation.exists_linearIsometryEquiv_eq_of_det_pos {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {f : V ≃ₗᵢ[ℝ] V} (hd : 0 < LinearMap.det ↑f.toLinearEquiv) : ∃ (θ : Real.Angle), f = Orientation.rotation o θ

Any linear isometric equivalence in V with positive determinant is rotation.

theorem Orientation.rotation_map {V : Type u_1} {V' : Type u_2} [NormedAddCommGroup V] [NormedAddCommGroup V'] [InnerProductSpace ℝ V] [InnerProductSpace ℝ V'] [Fact (FiniteDimensional.finrank ℝ V = 2)] [Fact (FiniteDimensional.finrank ℝ V' = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) (f : V ≃ₗᵢ[ℝ] V') (x : V') : (Orientation.rotation ((Orientation.map (Fin 2) f.toLinearEquiv) o) θ) x = f ((Orientation.rotation o θ) ((LinearIsometryEquiv.symm f) x))

@[simp]

theorem Complex.rotation (θ : Real.Angle) (z : ℂ) : (Orientation.rotation Complex.orientation θ) z = ↑(Real.Angle.expMapCircle θ) * z

theorem Orientation.rotation_map_complex {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) (f : V ≃ₗᵢ[ℝ] ℂ) (hf : (Orientation.map (Fin 2) f.toLinearEquiv) o = Complex.orientation) (x : V) : f ((Orientation.rotation o θ) x) = ↑(Real.Angle.expMapCircle θ) * f x

Rotation in an oriented real inner product space of dimension 2 can be evaluated in terms of a complex-number representation of the space.

theorem Orientation.rotation_neg_orientation_eq_neg {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) : Orientation.rotation (-o) θ = Orientation.rotation o (-θ)

Negating the orientation negates the angle in rotation.

@[simp]

theorem Orientation.inner_rotation_pi_div_two_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) : ⟪(Orientation.rotation o ↑(Real.pi / 2)) x, x⟫_ℝ = 0

The inner product between a π / 2 rotation of a vector and that vector is zero.

@[simp]

theorem Orientation.inner_rotation_pi_div_two_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) : ⟪x, (Orientation.rotation o ↑(Real.pi / 2)) x⟫_ℝ = 0

The inner product between a vector and a π / 2 rotation of that vector is zero.

@[simp]

theorem Orientation.inner_smul_rotation_pi_div_two_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (r : ℝ) : ⟪r • (Orientation.rotation o ↑(Real.pi / 2)) x, x⟫_ℝ = 0

The inner product between a multiple of a π / 2 rotation of a vector and that vector is zero.

@[simp]

theorem Orientation.inner_smul_rotation_pi_div_two_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (r : ℝ) : ⟪x, r • (Orientation.rotation o ↑(Real.pi / 2)) x⟫_ℝ = 0

The inner product between a vector and a multiple of a π / 2 rotation of that vector is zero.

@[simp]

theorem Orientation.inner_rotation_pi_div_two_left_smul {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (r : ℝ) : ⟪(Orientation.rotation o ↑(Real.pi / 2)) x, r • x⟫_ℝ = 0

The inner product between a π / 2 rotation of a vector and a multiple of that vector is zero.

@[simp]

theorem Orientation.inner_rotation_pi_div_two_right_smul {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (r : ℝ) : ⟪r • x, (Orientation.rotation o ↑(Real.pi / 2)) x⟫_ℝ = 0

The inner product between a multiple of a vector and a π / 2 rotation of that vector is zero.

@[simp]

theorem Orientation.inner_smul_rotation_pi_div_two_smul_left {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (r₁ : ℝ) (r₂ : ℝ) : ⟪r₁ • (Orientation.rotation o ↑(Real.pi / 2)) x, r₂ • x⟫_ℝ = 0

The inner product between a multiple of a π / 2 rotation of a vector and a multiple of that vector is zero.

@[simp]

theorem Orientation.inner_smul_rotation_pi_div_two_smul_right {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) (x : V) (r₁ : ℝ) (r₂ : ℝ) : ⟪r₂ • x, r₁ • (Orientation.rotation o ↑(Real.pi / 2)) x⟫_ℝ = 0

The inner product between a multiple of a vector and a multiple of a π / 2 rotation of that vector is zero.

theorem Orientation.inner_eq_zero_iff_eq_zero_or_eq_smul_rotation_pi_div_two {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [Fact (FiniteDimensional.finrank ℝ V = 2)] (o : Orientation ℝ V (Fin 2)) {x : V} {y : V} : ⟪x, y⟫_ℝ = 0 ↔ x = 0 ∨ ∃ (r : ℝ), r • (Orientation.rotation o ↑(Real.pi / 2)) x = y

The inner product between two vectors is zero if and only if the first vector is zero or the second is a multiple of a π / 2 rotation of that vector.