From b26f9e66912edbc8cf3794b6047a647d2baa7b3a Mon Sep 17 00:00:00 2001 From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com> Date: Fri, 26 Jul 2024 16:32:54 -0400 Subject: [PATCH] bump to v4.10.0-rc2 --- HepLean/Mathematics/LinearMaps.lean | 2 +- HepLean/Mathematics/SO3/Basic.lean | 2 +- HepLean/SpaceTime/LorentzGroup/Proper.lean | 1 - README.md | 32 +++++++++++----------- lake-manifest.json | 10 +++---- lakefile.toml | 6 ++-- lean-toolchain | 2 +- 7 files changed, 27 insertions(+), 28 deletions(-) diff --git a/HepLean/Mathematics/LinearMaps.lean b/HepLean/Mathematics/LinearMaps.lean index 36885fe..bb65a7b 100644 --- a/HepLean/Mathematics/LinearMaps.lean +++ b/HepLean/Mathematics/LinearMaps.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import Mathlib.Tactic.Polyrith -import Mathlib.Algebra.Module.LinearMap.Basic +import Mathlib.Algebra.Module.LinearMap.Defs import Mathlib.Data.Fintype.BigOperators /-! # Linear maps diff --git a/HepLean/Mathematics/SO3/Basic.lean b/HepLean/Mathematics/SO3/Basic.lean index 1d78a7c..37681b2 100644 --- a/HepLean/Mathematics/SO3/Basic.lean +++ b/HepLean/Mathematics/SO3/Basic.lean @@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import Mathlib.LinearAlgebra.UnitaryGroup -import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup +import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs import Mathlib.Data.Complex.Exponential import Mathlib.LinearAlgebra.Eigenspace.Basic import Mathlib.Analysis.InnerProductSpace.PiL2 diff --git a/HepLean/SpaceTime/LorentzGroup/Proper.lean b/HepLean/SpaceTime/LorentzGroup/Proper.lean index 7336389..944c8e1 100644 --- a/HepLean/SpaceTime/LorentzGroup/Proper.lean +++ b/HepLean/SpaceTime/LorentzGroup/Proper.lean @@ -46,7 +46,6 @@ def coeForℤ₂ : C(({-1, 1} : Set ℝ), ℤ₂) where toFun x := if x = ⟨1, Set.mem_insert_of_mem (-1) rfl⟩ then (Additive.toMul 0) else (Additive.toMul (1 : ZMod 2)) continuous_toFun := by - haveI : DiscreteTopology ({-1, 1} : Set ℝ) := discrete_of_t1_of_finite exact continuous_of_discreteTopology /-- The continuous map taking a Lorentz matrix to its determinant. -/ diff --git a/README.md b/README.md index 7ef0097..8a499e0 100644 --- a/README.md +++ b/README.md @@ -4,7 +4,7 @@ [![](https://img.shields.io/badge/PRs-Welcome-green)](https://github.com/HEPLean/HepLean/pulls) [![](https://img.shields.io/badge/Lean-Zulip-green)](https://leanprover.zulipchat.com) [![](https://img.shields.io/badge/TODO-List-green)](https://heplean.github.io/HepLean/TODOList) -[![](https://img.shields.io/badge/Lean-v4.10.0--rc1-blue)](https://github.com/leanprover/lean4/releases/tag/v4.10.0-rc1) +[![](https://img.shields.io/badge/Lean-v4.10.0--rc2-blue)](https://github.com/leanprover/lean4/releases/tag/v4.10.0-rc2) A project to digitalize high energy physics. @@ -12,58 +12,58 @@ A project to digitalize high energy physics. - Use Lean to create an exhaustive database of definitions, theorems, proofs, and calculations in high energy physics. - Make a library that is easy to use by the high energy physics community. -- Keep the database up-to date with developments in MathLib4. -- Create GitHub workflows of relevance to the high energy physics community. +- Keep the database up-to date with developments in MathLib4. +- Create GitHub workflows of relevance to the high energy physics community. ## Areas of high energy physics with some coverage in HepLean - + [![](https://img.shields.io/badge/The_CKM_Matrix-blue)](https://heplean.github.io/HepLean/docs/HepLean/FlavorPhysics/CKMMatrix/Basic.html) [![](https://img.shields.io/badge/Higgs_Field-blue)](https://heplean.github.io/HepLean/docs/HepLean/StandardModel/HiggsBoson/Basic.html) [![](https://img.shields.io/badge/2HDM-blue)](https://heplean.github.io/HepLean/docs/HepLean/BeyondTheStandardModel/TwoHDM/Basic.html) [![](https://img.shields.io/badge/Lorentz_Group-blue)](https://heplean.github.io/HepLean/docs/HepLean/SpaceTime/LorentzGroup/Basic.html) [![](https://img.shields.io/badge/Anomaly_Cancellation-blue)](https://heplean.github.io/HepLean/docs/HepLean/AnomalyCancellation/Basic.html) [![](https://img.shields.io/badge/Feynman_diagrams-blue)](https://heplean.github.io/HepLean/docs/HepLean/FeynmanDiagrams/PhiFour/Basic.html) -## Where to learn more +## Where to learn more - Read the associated paper: https://arxiv.org/abs/2405.08863 -- The documentation for this project is at: +- The documentation for this project is at: https://heplean.github.io/HepLean/ - Watch this overview of HepLean: https://www.youtube.com/watch?v=W2cObnopqas -- A list of 'Frequently asked questions' can be found on the Wiki for this project: +- A list of 'Frequently asked questions' can be found on the Wiki for this project: https://github.com/HEPLean/HepLean/wiki/The-answers-to-some-questions -- Feel free to connect on the Lean Zulip channel: +- Feel free to connect on the Lean Zulip channel: https://leanprover.zulipchat.com - A small example script relating to the three fermion anomaly cancellation condition can be found [here](https://live.lean-lang.org/#code=import%20Mathlib.Tactic.Polyrith%20%0A%0Atheorem%20threeFamily%20(a%20b%20c%20%3A%20ℚ)%20(h%20%3A%20a%20%2B%20b%20%2B%20c%20%3D%200)%20(h3%20%3A%20a%20%5E%203%20%2B%20b%20%5E%203%20%2B%20c%20%5E%203%20%3D%200)%20%3A%20%0A%20%20%20%20a%20%3D%200%20∨%20b%20%3D%200%20∨%20c%20%3D%200%20%20%3A%3D%20by%20%0A%20%20have%20h1%20%3A%20c%20%3D%20-%20(a%20%2B%20b)%20%3A%3D%20by%20%0A%20%20%20%20linear_combination%20h%20%0A%20%20have%20h4%20%3A%20%203%20*%20a%20*%20b%20*%20c%20%3D%200%20%3A%3D%20by%20%0A%20%20%20%20rw%20%5B←%20h3%2C%20h1%5D%0A%20%20%20%20ring%20%0A%20%20simp%20at%20h4%20%0A%20%20exact%20or_assoc.mp%20h4%0A%20%20%0A) -## Contributing +## Contributing -We follow here roughly the same contribution policies as MathLib4 (which can be found [here](https://leanprover-community.github.io/contribute/index.html)). +We follow here roughly the same contribution policies as MathLib4 (which can be found [here](https://leanprover-community.github.io/contribute/index.html)). A guide to contributing can be found [here](https://github.com/HEPLean/HepLean/blob/master/CONTRIBUTING.md). -If you want permission to create a pull-request for this repository contact Joseph Tooby-Smith on the lean Zulip, or email. +If you want permission to create a pull-request for this repository contact Joseph Tooby-Smith on the lean Zulip, or email. ## Installation -### Installing Lean 4 +### Installing Lean 4 -The installation instructions for Lean 4 are given here: https://leanprover-community.github.io/get_started.html. +The installation instructions for Lean 4 are given here: https://leanprover-community.github.io/get_started.html. -### Installing HepLean +### Installing HepLean -- Clone this repository (or download the repository as a Zip file) +- Clone this repository (or download the repository as a Zip file) - Open a terminal at the top-level in the corresponding directory. - Run `lake exe cache get`. The command `lake` should have been installed when you installed Lean. - Run `lake build`. @@ -72,4 +72,4 @@ The installation instructions for Lean 4 are given here: https://leanprover-comm ### Optional extras - [Lean Copilot](https://github.com/lean-dojo/LeanCopilot) allows the use of large language models in Lean. -- [tryAtEachStep](https://github.com/dwrensha/tryAtEachStep) allows one to apply a tactic, e.g. `exact?` at each step of a lemma in a file to see if it completes the goal. This is useful for golfing proofs. +- [tryAtEachStep](https://github.com/dwrensha/tryAtEachStep) allows one to apply a tactic, e.g. `exact?` at each step of a lemma in a file to see if it completes the goal. This is useful for golfing proofs. diff --git a/lake-manifest.json b/lake-manifest.json index b682f84..837bdcd 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -5,7 +5,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "2ead90d24b4fac3a05c9c4294daa39bd8686fb98", + "rev": "c0efc1fd2a0bec51bd55c5b17348af13d7419239", "name": "batteries", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -25,7 +25,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "a64fe24aa94e21404940e9217363a9a1ed9a33a6", + "rev": "deb5bd446a108da8aa8c1a1b62dd50722b961b73", "name": "aesop", "manifestFile": "lake-manifest.json", "inputRev": "master", @@ -55,7 +55,7 @@ "type": "git", "subDir": null, "scope": "leanprover-community", - "rev": "d366a602cc4a325a6f9db3a3991dfa6d6cf409c5", + "rev": "68b518c9b352fbee16e6d632adcb7a6d0760e2b7", "name": "importGraph", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -65,10 +65,10 @@ "type": "git", "subDir": null, "scope": "", - "rev": "f5c3f06aa7f6d6c221786d2890c345a00e6341f8", + "rev": "984c68d7773ac133c74543b99b82c33e53baea6b", "name": "mathlib", "manifestFile": "lake-manifest.json", - "inputRev": "v4.10.0-rc1", + "inputRev": "v4.10.0-rc2", "inherited": false, "configFile": "lakefile.lean"}, {"url": "https://github.com/acmepjz/md4lean", diff --git a/lakefile.toml b/lakefile.toml index 0326152..275ff94 100644 --- a/lakefile.toml +++ b/lakefile.toml @@ -6,7 +6,7 @@ defaultTargets = ["HepLean"] [[require]] name = "mathlib" git = "https://github.com/leanprover-community/mathlib4.git" -rev = "v4.10.0-rc1" +rev = "v4.10.0-rc2" [[require]] name = "«doc-gen4»" @@ -24,7 +24,7 @@ name = "HepLean" # -- Optional inclusion of tryAtEachStep #[[require]] -#name = "tryAtEachStep" +#name = "tryAtEachStep" #git = "https://github.com/dwrensha/tryAtEachStep" #rev = "main" @@ -63,4 +63,4 @@ srcDir = "scripts" # -- Optional inclusion of openAI_doc_check. Needs `llm` above. #[[lean_exe]] #name = "openAI_doc_check" -#srcDir = "scripts" \ No newline at end of file +#srcDir = "scripts" diff --git a/lean-toolchain b/lean-toolchain index d69d1ed..6a4259f 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1 +1 @@ -leanprover/lean4:v4.10.0-rc1 +leanprover/lean4:v4.10.0-rc2