feat(linear_algebra/orientation): orientations of modules and rays in…

… modules (#10306)

Define orientations of modules, along the lines of a definition
suggested by @hrmacbeth: equivalence classes of nonzero alternating
maps.  See:
https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there.20code.20for.20X.3F/topic/adding.20angles/near/243856522

Rays are defined in an arbitrary module over an
`ordered_comm_semiring`, then orientations are considered as the case
of rays for the space of alternating maps.  That definition uses an
arbitrary index type; the motivating use case is where this has the
cardinality of a basis (two-dimensional use cases will use an index
type that is definitionally `fin 2`, for example).

The motivating use case is over the reals, but the definitions and
lemmas are for `ordered_comm_semiring`, `ordered_comm_ring`,
`linear_ordered_comm_ring` or `linear_ordered_field` as appropriate (a
`nontrivial` `ordered_comm_semiring` looks like it's the weakest case
for which much useful can be done with this definition).

Given an intended use case (oriented angles for Euclidean geometry)
where it will make sense for many proofs (and notation) to fix a
choice of orientation throughout, there is also a `module.oriented`
type class so the choice of orientation can be implicit in such proofs
and the lemmas they use.  However, nothing yet makes use of the type
class; everything so far is for explicit rays or orientations.

I expect more definitions and lemmas about orientations will need
adding to make much use of orientations.  In particular, I expect to
need to add more about orientations in relation to bases
(e.g. extracting a basis that gives a given orientation, in positive
dimension).

docs/undergrad.yaml

@@ -37,7 +37,7 @@ Linear algebra:
     determinant of vectors: 'basis.det'
     determinant of endomorphisms: 'linear_map.det'
     special linear group: 'https://en.wikipedia.org/wiki/Special_linear_group'
-    orientation of a $\R$-vector space: 'https://en.wikipedia.org/wiki/Orientation_(vector_space)'
+    orientation of a $\R$-vector space: 'orientation'
   Matrices:
     commutative-ring-valued matrices: 'matrix'
     field-valued matrices: 'matrix'