This is related to this conversation on the Lean Zulip.
In particular, it was noted that the definition of SpaceTime a what can be done with it is somewhat confusing and it would help to have documentation and a tutorial related to it.
The aim of this issue is to create part of 'PhysLean Notes' dedicated to SpaceTime.
This is related to this conversation on the Lean Zulip.
In particular, it was noted that the definition of SpaceTime a what can be done with it is somewhat confusing and it would help to have documentation and a tutorial related to it.
The aim of this issue is to create part of 'PhysLean Notes' dedicated to SpaceTime.