Skip to content

Instantly share code, notes, and snippets.

/-
The Genera Linear group $GL(n, R)$
-/
import linear_algebra.matrix
import linear_algebra.matrix.nonsingular_inverse
import linear_algebra.special_linear_group
/-!
/-
The Genera Linear group $GL(n, R)$
-/
import linear_algebra.matrix
import linear_algebra.matrix.nonsingular_inverse
import linear_algebra.special_linear_group
/-!