The underlying matrix of a positive-determinant invertible matrix #
Matrix.GLPos n R is a subgroup of GL n R, which is a group of units, so
reading off the matrix takes two coercions. toMat is that composite, together
with the two lemmas saying it is a monoid map.
Neutral general-linear-group API: it mentions no cover, no phase and no
stability condition, and it is consumed independently by the universal cover of
GL⁺(2, ℝ) under UniversalCover/, by the complex-coordinate adapter in
LinearAlgebra/Complex/Coordinates.lean, and by the stability action under
CategoryTheory/Triangulated/StabilityCondition/Symmetry/GLTilde/Action/.
Extracted by MO1.12 (#1323) from the cover's Basic.lean, where it was
declared; the fully qualified names are unchanged, per the cutover ledger's
first standing decision.
The matrix underlying an element of GL⁺(2, ℝ).