Merge pull request #98 from HEPLean/Update-versions
bump to v4.10.0-rc2
This commit is contained in:
Joseph Tooby-Smith
GitHub
commit
e9aefe3ea5
7 changed files with 27 additions and 28 deletions
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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. -/
|
||||
|
|
|
|||
32
README.md
32
README.md
|
|
@ -4,7 +4,7 @@
|
|||
[](https://github.com/HEPLean/HepLean/pulls)
|
||||
[](https://leanprover.zulipchat.com)
|
||||
[](https://heplean.github.io/HepLean/TODOList)
|
||||
[](https://github.com/leanprover/lean4/releases/tag/v4.10.0-rc1)
|
||||
[](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://heplean.github.io/HepLean/docs/HepLean/FlavorPhysics/CKMMatrix/Basic.html)
|
||||
[](https://heplean.github.io/HepLean/docs/HepLean/StandardModel/HiggsBoson/Basic.html)
|
||||
[](https://heplean.github.io/HepLean/docs/HepLean/BeyondTheStandardModel/TwoHDM/Basic.html)
|
||||
[](https://heplean.github.io/HepLean/docs/HepLean/SpaceTime/LorentzGroup/Basic.html)
|
||||
[](https://heplean.github.io/HepLean/docs/HepLean/AnomalyCancellation/Basic.html)
|
||||
[](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.
|
||||
|
|
|
|||
|
|
@ -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",
|
||||
|
|
|
|||
|
|
@ -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"
|
||||
#srcDir = "scripts"
|
||||
|
|
|
|||
|
|
@ -1 +1 @@
|
|||
leanprover/lean4:v4.10.0-rc1
|
||||
leanprover/lean4:v4.10.0-rc2
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue