@[reducible, inline]

abbrev Isometries.Plane : Type

noncomputable def Isometries.linearDet (f : Plane ≃ᵃⁱ[ℝ] Plane) : ℝ

def Isometries.IsTranslation (f : Plane ≃ᵃⁱ[ℝ] Plane) : Prop

def Isometries.IsRotation (f : Plane ≃ᵃⁱ[ℝ] Plane) : Prop

def Isometries.IsReflection (f : Plane ≃ᵃⁱ[ℝ] Plane) : Prop

def Isometries.IsGlideReflection (f : Plane ≃ᵃⁱ[ℝ] Plane) : Prop

theorem Isometries.affine_decomp_aux (f : Plane ≃ᵃⁱ[ℝ] Plane) (x : Plane) : f x = f.linearIsometryEquiv x + f 0

theorem Isometries.plane_isometry_classification (f : Plane ≃ᵃⁱ[ℝ] Plane) : IsTranslation f ∨ IsRotation f ∨ IsReflection f ∨ IsGlideReflection f

theorem Isometries.isometry_map_zero_isLinearMap {n : ℕ} (f : EuclideanSpace ℝ (Fin n) → EuclideanSpace ℝ (Fin n)) (hf : Isometry f) (hf0 : f 0 = 0) : IsLinearMap ℝ f