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 2025-03-24 12:02:43 -04:00
parent 70ace79ccc
commit 1bbc9ac564
1 changed files with 2 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

3
PhysLean/Relativity/Tensors/OverColor/Discrete.lean
View file

@ -67,7 +67,8 @@ def pairIsoSep {c1 c2 : C} : F.obj (Discrete.mk c1) ⊗ F.obj (Discrete.mk c2)
rfl
lemma pairIsoSep_tmul {c1 c2 : C} (x : F.obj (Discrete.mk c1)) (y : F.obj (Discrete.mk c2)) :
((pairIsoSep F).hom.hom : (F.obj (Discrete.mk c1)).V ⊗ (F.obj (Discrete.mk c2)).V ⟶ _ ) (x ⊗ₜ[k] y) =
((pairIsoSep F).hom.hom :
(F.obj (Discrete.mk c1)).V ⊗ (F.obj (Discrete.mk c2)).V ⟶ _ ) (x ⊗ₜ[k] y) =
PiTensorProduct.tprod k (Fin.cases x (Fin.cases y (fun i => Fin.elim0 i))) := by
conv_lhs =>
simp only [Action.instMonoidalCategory_tensorObj_V, Nat.succ_eq_add_one, Nat.reduceAdd,