Skip to content

Commit

Permalink
fix
Browse files Browse the repository at this point in the history
  • Loading branch information
eric-wieser committed Feb 1, 2023
1 parent 04f0c28 commit d60476e
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/linear_algebra/matrix/general_linear_group.lean
Original file line number Diff line number Diff line change
Expand Up @@ -3,8 +3,8 @@ Copyright (c) 2021 Chris Birkbeck. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Chris Birkbeck
-/
import linear_algebra.general_linear_group
import linear_algebra.matrix.nonsingular_inverse
import linear_algebra.matrix.general_linear_group
import linear_algebra.matrix.special_linear_group

/-!
Expand Down

0 comments on commit d60476e

Please sign in to comment.