feat(linear_algebra/unitary_group): better constructor (#15209)
`A ∈ matrix.unitary_group n α` means by definition (for reasons of agreement with something more general) that `A * star A = 1` and `star A * A = 1`. But either condition implies the other, so we provide a lemma to reduce to the first.
