DibyashanuPati/PhysLean
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Update B3.lean

Browse source
This commit is contained in:
Pietro Monticone 2024-06-08 01:50:34 +02:00
parent 984e6f85d4
commit 6283d54e93
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
HepLean/AnomalyCancellation/MSSMNu/B3.lean
View file

@ -7,7 +7,7 @@ import HepLean.AnomalyCancellation.MSSMNu.Basic
/-!
# The definition of the solution B₃ and properties thereof
We define $B_3$ and show that it is a double point of the cubic.
We define `B₃` and show that it is a double point of the cubic.
# References
@ -24,7 +24,7 @@ open MSSMCharges
open MSSMACCs
open BigOperators
/-- $B_3$ is the charge which is $B-L$ in all families, but with the third
/-- `B₃` is the charge which is $B-L$ in all families, but with the third
family of the opposite sign. -/
def B₃AsCharge : MSSMACC.charges := toSpecies.symm
⟨fun s => fun i =>
@ -52,7 +52,7 @@ def B₃AsCharge : MSSMACC.charges := toSpecies.symm
| 0 => -3
| 1 => 3⟩
/-- $B_3$ as a solution. -/
/-- `B₃` as a solution. -/
def B₃ : MSSMACC.Sols :=
MSSMACC.AnomalyFreeMk B₃AsCharge (by rfl) (by rfl) (by rfl) (by rfl) (by rfl) (by rfl)