From f92291885a9b44314b33c61e8ce4672e7f7817a0 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Thu, 27 Jun 2024 08:43:57 -0400
Subject: [PATCH] remove matrix.rank file

---
 HepLean/Mathematics/Matrices/Rank.lean | 85 --------------------------
 scripts/check_file_imports.lean        |  5 +-
 2 files changed, 1 insertion(+), 89 deletions(-)
 delete mode 100644 HepLean/Mathematics/Matrices/Rank.lean

diff --git a/HepLean/Mathematics/Matrices/Rank.lean b/HepLean/Mathematics/Matrices/Rank.lean
deleted file mode 100644
index 28e098f..0000000
--- a/HepLean/Mathematics/Matrices/Rank.lean
+++ /dev/null
@@ -1,85 +0,0 @@
-/-
-Copyright (c) 2024 Joseph Tooby-Smith. All rights reserved.
-Released under Apache 2.0 license.
-Authors: Joseph Tooby-Smith
--/
-import Mathlib.LinearAlgebra.UnitaryGroup
-import Mathlib.Data.Complex.Exponential
-import Mathlib.Tactic.Polyrith
-import LeanCopilot
-/-!
-
-# Rank of matrices
-
-This field contains addiational lemmas and results about the rank of matrices beyond
-those which appear in Mathlib.
-
-Our method is to provide a certificate checker for the rank of the matrix.
-
-## TODO
-
-- Automate, following the method of `polyrith`, the process of finding the
-  row-reduced form of a matrix.
-
--/
-
-namespace Mathematics
-variable {n m : ℕ}
-open Matrix
-
-/-- The proposition on a matrix for it to be in row echelon form. -/
-def IsRowEchelonForm (M : Matrix (Fin n) (Fin m) ℚ) : Prop :=
-  ∀ i j, i < j →
-    match Fin.find (fun k => M i k ≠ 0), Fin.find (fun k => M j k ≠ 0) with
-    | some i', some j' => i' < j'
-    | some _, none => true
-    | none, some _ => false
-    | none, none => true
-
-instance (M : Matrix (Fin n) (Fin m) ℚ) : Decidable (IsRowEchelonForm M) := by
-  refine @Fintype.decidableForallFintype _ _ (fun i => ?_) _
-  refine @Fintype.decidableForallFintype _ _ (fun j => ?_) _
-  refine @instDecidableForall _  _ (i.decLt j) ?_
-  match  Fin.find (fun k => M i k ≠ 0), Fin.find (fun k => M j k ≠ 0) with
-  | some i', some j'  => exact i'.decLt j'
-  | some _, none => exact true.decEq true
-  | none, some _ => exact false.decEq true
-  | none, none => exact true.decEq true
-
-example : IsRowEchelonForm !![1, 2, 3; 0, 1, 3; 0, 0, 1] := by
-  decide
-
-example :  ¬ IsRowEchelonForm !![1, 2, 3; 0, 1, 3; 0, 2, 1] := by
-  decide
-
-/-- `M` is a row echelon form of `N`. -/
-structure RowEchelonFormOf (M : Matrix (Fin n) (Fin m) ℚ) where
-  rowEchelonForm : Matrix (Fin n) (Fin m) ℚ
-  transform : Matrix (Fin n) (Fin n) ℚ
-  transformInv : Matrix (Fin n) (Fin n) ℚ
-  transform_invert : transform * transformInv = 1 := by norm_num <;> decide
-  transform_mul : transform * M = rowEchelonForm := by norm_num
-  rowEchelonForm_isRowEchelonForm : IsRowEchelonForm rowEchelonForm := by decide
-
-def sageRowEchelonFormQuery (M : Matrix (Fin n) (Fin m) ℚ) : IO Unit :=
-  let M := List.map (fun i =>
-    String.intercalate ", " (List.map (fun j => toString (M i j)) (Fin.list m))) (Fin.list n)
-  let echelonForm :=
-"M = Matrix([[" ++ String.intercalate "],[" M ++ "]])
-REF, P = M.echelon_form(transformation=True)
-def format(matrix):
-  rows = []
-  for row in matrix.rows():
-      rows.append(', '.join(map(str, row)))
-  return \"!![\" + \"; \".join(rows) + \"]\"
-print(f\"rowEchelonForm := {format(REF)}\")
-print(f\"transform := {format(P)}\")
-print(f\"transformInv := {format(P.inverse())}\")"
-  IO.println (echelonForm)
-
-def myTestMatrix : RowEchelonFormOf !![1, 2, 3; 4, 5, 6; 7, 8, 9; 10, 11, 12] where
-  rowEchelonForm := !![1, 2, 3; 0, 3, 6; 0, 0, 0; 0, 0, 0]
-  transform := !![0, 0, 3, -2; 0, 0, 10, -7; 1, 0, -3, 2; 0, 1, -2, 1]
-  transformInv := !![1, 0, 1, 0; 4, -1, 0, 1; 7, -2, 0, 0; 10, -3, 0, 0]
-
-end Mathematics
diff --git a/scripts/check_file_imports.lean b/scripts/check_file_imports.lean
index ec21e44..394826c 100644
--- a/scripts/check_file_imports.lean
+++ b/scripts/check_file_imports.lean
@@ -22,11 +22,9 @@ The functions
 
 are adapted from `batteries.scripts.check_imports.lean` authored by Joe Hendrix.
 
-
 -/
 open Lean System Meta
 
-
 /--  Recursively finds files in directory. -/
 partial def addModulesIn (recurse : Bool) (prev : Array Name) (root : Name := .anonymous)
     (path : FilePath) : IO (Array Name) := do
@@ -41,7 +39,6 @@ partial def addModulesIn (recurse : Bool) (prev : Array Name) (root : Name := .a
       r := r.push (root.mkStr mod)
   pure r
 
-
 /-- Compute imports expected by `HepLean.lean` by looking at file structure. -/
 def expectedHepLeanImports : IO (Array Name) := do
   let mut needed := #[]
@@ -80,7 +77,7 @@ def checkMissingImports (modData : ModuleData) (reqImports : Array Name) :
 def main (_ : List String) : IO UInt32 := do
   initSearchPath (← findSysroot)
   let mods : Name :=  `HepLean
-  let imp :  Import := {module := mods}
+  let imp : Import := {module := mods}
   let mFile ← findOLean imp.module
   unless (← mFile.pathExists) do
         throw <| IO.userError s!"object file '{mFile}' of module {imp.module} does not exist"