Decomposition of the symmetry group of euclidean space

Stream: Is there code for X?

[Youjack]

Is there any theorem stating that the symmetry group of euclidean space (as a metric space) can be decomposed into translations, rotations and reflections?
And, is there theorem stating that isometries of euclidean space are diffeomorphisms? Maybe this should be a theorem in Riemannian geometry, which is not yet formalized in mathlib as far as I know.

[Johan Commelin]

I think in both cases the answer is "nope, we don't have it"

[Johan Commelin]

But certainly (1) should be well within reach.