auto-task(exists_boost_mul_rotation): prove restricted Lorentz elements are a boost times a rotation - #1350

auto-task(exists_boost_mul_rotation): prove restricted Lorentz elements are a boost times a rotation#1350

jstoobysmith merged 2 commits into

leanprover-community:masterleanprover-community/physlib:masterfrom

jstoobysmith:auto-todocompleter-20260701-142620jstoobysmith/JTSphyslib:auto-todocompleter-20260701-142620Copy head branch name to clipboard