mathlib
abe81bcb - feat(linear_algebra/matrix/general_linear_group): GL(n, R) (#8466)

Commit
4 years ago
feat(linear_algebra/matrix/general_linear_group): GL(n, R) (#8466) added this file which contains definition of the general linear group as well as the subgroup of matrices with positive determinant.
Author
Parents
Loading