Skip to content
This repository was archived by the owner on Jul 24, 2024. It is now read-only.

Commit 544f45b

Browse files
committed
refactor(linear_algebra/bilinear_form): split off matrix part (#12435)
The bilinear form file is way too large. The part that concerns matrices is not depended on by the general theory, and belongs in its own file.
1 parent 5371338 commit 544f45b

File tree

5 files changed

+560
-511
lines changed

5 files changed

+560
-511
lines changed

src/algebra/lie/skew_adjoint.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
44
Authors: Oliver Nash
55
-/
66
import algebra.lie.matrix
7-
import linear_algebra.bilinear_form
7+
import linear_algebra.matrix.bilinear_form
88

99
/-!
1010
# Lie algebras of skew-adjoint endomorphisms of a bilinear form

0 commit comments

Comments
 (0)