diff --git a/.github/workflows/check_file_import.yml b/.github/workflows/check_file_import.yml new file mode 100644 index 00000000..d29335c7 --- /dev/null +++ b/.github/workflows/check_file_import.yml @@ -0,0 +1,22 @@ +on: + push: + +name: check file import + +jobs: + check_file_import: + name: check file import + runs-on: ubuntu-latest + steps: + - name: clean up + run: | + find . -name . -o -prune -exec rm -rf -- {} + + + - uses: actions/checkout@v4 + + - name: update HepLean.lean + run: | + git ls-files 'HepLean/*.lean' | LC_ALL=C sort | sed 's/\.lean//;s,/,.,g;s/^/import /' > HepLean.lean + + - name: check that all files are imported + run: git diff --exit-code \ No newline at end of file diff --git a/HepLean/AnomalyCancellation/Basic.lean b/HepLean/AnomalyCancellation/Basic.lean index 4695374f..85932c31 100644 --- a/HepLean/AnomalyCancellation/Basic.lean +++ b/HepLean/AnomalyCancellation/Basic.lean @@ -4,13 +4,6 @@ Released under Apache 2.0 license. Authors: Joseph Tooby-Smith -/ import HepLean.AnomalyCancellation.LinearMaps -import Mathlib.Tactic.Polyrith -import Mathlib.Tactic.Linarith -import Mathlib.Tactic.FieldSimp -import Mathlib.NumberTheory.FLT.Basic -import Mathlib.Algebra.QuadraticDiscriminant -import Mathlib.Algebra.Module.Basic -import Mathlib.Algebra.Module.LinearMap.Basic /-! # Basic set up for anomaly cancellation conditions diff --git a/HepLean/AnomalyCancellation/LinearMaps.lean b/HepLean/AnomalyCancellation/LinearMaps.lean index 709c6e7c..8fe55723 100644 --- a/HepLean/AnomalyCancellation/LinearMaps.lean +++ b/HepLean/AnomalyCancellation/LinearMaps.lean @@ -14,6 +14,7 @@ quadratic and cubic equations. ## TODO Use definitions in `Mathlib4` for definitions where possible. +In particular a HomogeneousQuadratic should be a map `V →ₗ[ℚ] V →ₗ[ℚ] ℚ` etc. -/