The linear part homomorphism of a group of Euclidean isometries

import Mathlib
import Definitions.Def_LeanEval_SpaceGroups_Definitions
import Definitions.Def_SpaceGroupsPointGroupDefs

/-!
# The linear part homomorphism of a group of Euclidean isometries

For a subgroup `G` of the Euclidean motion group `E_d`, the map sending an element of `G` to
its linear part is a group homomorphism `G →* O(d)`. Its range is the point group of `G` and
its kernel is the subgroup of translations belonging to `G`.
-/

namespace LeanEval
namespace Geometry
namespace SpaceGroupsProblem

variable {d : ℕ}

/-- The linear part homomorphism of a group of Euclidean isometries. -/
noncomputable def linPartHom (G : Subgroup (EuclideanIsom d)) : G →* (E d ≃ₗᵢ[ℝ] E d) where
  toFun g := linPart g.1
  map_one' := rfl
  map_mul' _ _ := rfl

@[simp] lemma linPartHom_apply (G : Subgroup (EuclideanIsom d)) (g : G) :
    linPartHom G g = linPart g.1 := rfl

end SpaceGroupsProblem
end Geometry
end LeanEval