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

Update Boosts.lean

Browse source
This commit is contained in:
Pietro Monticone 2025-01-23 01:16:02 +01:00
parent 291f97eaed
commit 06de6fe570
1 changed files with 1 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

2
HepLean/Lorentz/Group/Boosts.lean
View file

@ -150,7 +150,7 @@ lemma toMatrix_apply (u v : FuturePointing d) (μ ν : Fin 1 ⊕ Fin d) :
Action.instMonoidalCategory_tensorUnit_V, CategoryTheory.Equivalence.symm_inverse,
Action.functorCategoryEquivalence_functor, Action.FunctorCategoryEquivalence.functor_obj_obj,
Pi.smul_apply, smul_eq_mul, Pi.sub_apply, Pi.neg_apply]
apply Or.inl
left
ring
open minkowskiMatrix in