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

Commit 2a32c70

Browse files
committed
refactor(linear_algebra/matrix/nonsingular_inverse): split out files for adjugate and nondegenerate (#9974)
This breaks the file roughly in two, and rescues lost lemmas that ended up in the wrong sections of the file. The module docstrings have been tweaked a little, but all the lemmas have just been moved around.
1 parent ce164e2 commit 2a32c70

File tree

5 files changed

+511
-466
lines changed

5 files changed

+511
-466
lines changed

src/linear_algebra/bilinear_form.lean

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -6,6 +6,7 @@ Authors: Andreas Swerdlow, Kexing Ying
66

77
import linear_algebra.dual
88
import linear_algebra.matrix.basis
9+
import linear_algebra.matrix.nondegenerate
910
import linear_algebra.matrix.nonsingular_inverse
1011
import linear_algebra.tensor_product
1112

0 commit comments

Comments
 (0)