feat(geometry/euclidean/oriented_angle): oriented angles with respect to an orientation (#12236)

Add definitions and lemmas for oriented angles defined to take an
orientation, instead of an orthonormal basis, as an argument.  These
are the versions intended to be used by most users when working with
oriented angles between vectors, instead of users needing to deal with
a choice of basis.

Apart from the last five lemmas that relate angles and rotations for
different orientations or relate them explicitly to the definitions
with respect to a basis, everything is deduced directly from the
corresponding lemma that takes an orthonormal basis as an argument.

Author: jsm28

src/geometry/euclidean/basic.lean

@@ -70,7 +70,8 @@ corresponding results for Euclidean affine spaces.
 variables {V : Type*} [inner_product_space ℝ V]
 
 /-- The undirected angle between two vectors. If either vector is 0,
-this is π/2. -/
+this is π/2. See `orientation.oangle` for the corresponding oriented angle
+definition. -/
 def angle (x y : V) : ℝ := real.arccos (inner x y / (∥x∥ * ∥y∥))
 
 lemma is_conformal_map.preserves_angle {E F : Type*}