API: Euclidean group

[jstoobysmith]

Details

Key data structure

The isometry group of Euclidean space, this is the Euclidean group.

• is defined.

Need

This is needed for symmetries of Euclidean space, it contains rotations, reflections and translations.

Requirements

• The API shall contain the inclusion of the special Euclidean group.
• The API shall contain the inclusion of translations.
• The API shall contain the inclusion of rotations about each spatial point.
• The API shall contain a specification of a group element from a translation and rotation.
• The API shall contain the inclusion of the Euclidean group into the Affine group.

Corresponding file system

There is no corresponding part of PhysLean for this API yet.

References

There is some coverage of this in:

• https://github.com/mrdouglasny/OSforGFF/tree/main

See the discussion here about the definition of the Euclidean Space:

• https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/topic/Space.20vs.20EuclideanSpace/with/575936453