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

fix typos in TODOs

Browse source
This commit is contained in:
Pietro Monticone 2025-01-23 00:22:30 +01:00
parent 3d909b357a
commit 0a93029436
2 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -11,7 +11,7 @@ import HepLean.Mathematics.SO3.Basic
This file describes the embedding of `SO(3)` into `LorentzGroup 3`.
-/
TODO "Generalize the inclusion of rotations into LorentzGroup to abitary dimension."
TODO "Generalize the inclusion of rotations into LorentzGroup to arbitrary dimension."
noncomputable section
namespace LorentzGroup