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

refactor: Lint

Browse source
This commit is contained in:
jstoobysmith 2024-11-15 10:52:06 +00:00
parent a1aec64a83
commit 6b0c69c9ff
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/Tensors/OverColor/Discrete.lean
View file

@ -112,7 +112,7 @@ lemma pairIsoSep_tmul {c1 c2 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (Discr
exact (LinearEquiv.eq_symm_apply _).mp rfl
lemma pairIsoSep_inv_tprod {c1 c2 : C} (fx : (i : (𝟭 Type).obj (OverColor.mk ![c1, c2]).left) →
CoeSort.coe (F.obj { as := (OverColor.mk ![c1, c2]).hom i })) :
CoeSort.coe (F.obj { as := (OverColor.mk ![c1, c2]).hom i })) :
(pairIsoSep F).inv.hom (PiTensorProduct.tprod k fx) = fx (0 : Fin 2) ⊗ₜ fx (1 : Fin 2) := by
simp [pairIsoSep]
erw [lift.map_tprod]