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

Update Rows.lean

Browse source
This commit is contained in:
jstoobysmith 2024-11-02 07:57:22 +00:00
parent 3de17d1444
commit 2f2f2ff3d1
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -186,7 +186,7 @@ lemma rows_linearly_independent (V : CKMMatrix) : LinearIndependent ℂ (rows V)
· exact h1
· exact h2
lemma rows_card : Fintype.card (Fin 3) = FiniteDimensional.finrank ℂ (Fin 3 → ℂ) := by
lemma rows_card : Fintype.card (Fin 3) = Module.finrank ℂ (Fin 3 → ℂ) := by
simp
/-- The rows of a CKM matrix as a basis of `ℂ³`. -/