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

Update Basic.lean

Browse source
This commit is contained in:
Pietro Monticone 2024-06-08 03:56:15 +02:00
parent 776bce19fe
commit f259183222
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
HepLean/StandardModel/HiggsBoson/Basic.lean
View file

@ -75,10 +75,10 @@ lemma toHiggsVec_smooth (φ : higgsField) : Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ
exact h1
lemma toField_toHiggsVec_apply (φ : higgsField) (x : spaceTime) :
(φ.toHiggsVec x).toField x = φ x := rfl
(φ.toHiggsVec x).toField x = φ x := rfl
lemma higgsVecToFin2ℂ_toHiggsVec (φ : higgsField) :
higgsVecToFin2ℂ ∘ φ.toHiggsVec = φ := rfl
higgsVecToFin2ℂ ∘ φ.toHiggsVec = φ := rfl
lemma toVec_smooth (φ : higgsField) : Smooth 𝓘(ℝ, spaceTime) 𝓘(ℝ, Fin 2 → ℂ) φ :=
smooth_higgsVecToFin2ℂ.comp φ.toHiggsVec_smooth