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

style: Remove some extra spaces

Browse source
This commit is contained in:
jstoobysmith 2024-06-27 08:49:13 -04:00
parent fc6db7354b
commit 99a915d315
1 changed files with 0 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/FlavorPhysics/CKMMatrix/PhaseFreedom.lean
View file

@ -224,7 +224,6 @@ lemma ubOnePhaseCond_shift_solution {V : CKMMatrix} (h1 : a + f = - arg [V]ub)
subst hc
ring
-- rename
lemma fstRowThdColRealCond_holds_up_to_equiv (V : CKMMatrix) :
∃ (U : CKMMatrix), V ≈ U ∧ FstRowThdColRealCond U:= by
obtain ⟨τ, hτ⟩ := V.uRow_cross_cRow_eq_tRow
@ -319,7 +318,6 @@ lemma ubOnePhaseCond_hold_up_to_equiv_of_ub_one {V : CKMMatrix} (hb : ¬ ([V]ud
ring
rw [hcs, hUV, cs_of_ud_us_zero hb]
lemma cd_of_fstRowThdColRealCond {V : CKMMatrix} (hb : [V]ud ≠ 0 ∨ [V]us ≠ 0)
(hV : FstRowThdColRealCond V) :
[V]cd = (- VtbAbs ⟦V⟧ * VusAbs ⟦V⟧ / (VudAbs ⟦V⟧ ^2 + VusAbs ⟦V⟧ ^2)) +