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.
leanprover-community · Oct 26, 2021 · 2a32c70 · 2a32c70
1 parent ce164e2
commit 2a32c70
Show file tree

Hide file tree

Showing 5 changed files with 511 additions and 466 deletions.
diff --git a/src/linear_algebra/bilinear_form.lean b/src/linear_algebra/bilinear_form.lean
@@ -6,6 +6,7 @@ Authors: Andreas Swerdlow, Kexing Ying
 
 import linear_algebra.dual
 import linear_algebra.matrix.basis
+import linear_algebra.matrix.nondegenerate
 import linear_algebra.matrix.nonsingular_inverse
 import linear_algebra.tensor_product