Sum of Three Squares
Set up
def
rel
:
Setoid
(
Matrix
n
n
R
)
:=
MulAction.orbitRel
(
SpecialLinearGroup
n
R
)
(
Matrix
n
n
R
)