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

feat: update of Lean

Browse source
This commit is contained in:
jstoobysmith 2024-04-29 13:56:30 -04:00
parent cee60826d5
commit aa07e23ebd
5 changed files with 22 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

22
HepLean/FlavorPhysics/CKMMatrix/StandardParameterization/StandardParameters.lean
View file

@ -424,16 +424,16 @@ lemma on_param_cos_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.c
simp only [mul_zero, add_zero, neg_inj]
field_simp
ring
ring
ring_nf
field_simp
ring
ring_nf
change _ = _ + _ * 0
simp only [mul_zero, add_zero]
field_simp
ring
ring
ring_nf
field_simp
ring
lemma on_param_cos_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.cos (θ₂₃ ⟦V⟧) = 0) :
standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
@ -450,7 +450,7 @@ lemma on_param_cos_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.c
simp only [mul_zero, add_zero]
ring
field_simp
ring
lemma on_param_sin_θ₁₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₁₃ ⟦V⟧) = 0) :
standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) δ₁₃ ≈ standParam (θ₁₂ ⟦V⟧) (θ₁₃ ⟦V⟧) (θ₂₃ ⟦V⟧) 0 := by
@ -478,16 +478,16 @@ lemma on_param_sin_θ₁₂_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.s
simp only [mul_zero, add_zero, neg_inj]
ring
field_simp
ring
ring_nf
field_simp
ring
ring_nf
change _ = _ + _ * 0
simp only [mul_zero, add_zero, neg_inj]
ring
ring_nf
field_simp
ring
ring_nf
field_simp
ring
lemma on_param_sin_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.sin (θ₂₃ ⟦V⟧) = 0) :
@ -505,7 +505,7 @@ lemma on_param_sin_θ₂₃_eq_zero {V : CKMMatrix} (δ₁₃ : ℝ) (h : Real.s
ring
ring
field_simp
ring