@[reducible, inline]

abbrev DiscreteGroups.E2 : Type

@[reducible, inline]

abbrev DiscreteGroups.M₂ : Type

noncomputable def DiscreteGroups.translationPart (f : M₂) : E2

noncomputable def DiscreteGroups.linearPart (f : M₂) : E2 ≃ₗᵢ[ℝ] E2

def DiscreteGroups.IsPureTranslation (f : M₂) : Prop

noncomputable def DiscreteGroups.rotationAngle (f : M₂) : ℝ

def DiscreteGroups.IsDiscrete (G : Subgroup M₂) : Prop

def DiscreteGroups.pointGroupSet (G : Subgroup M₂) : Set (E2 ≃ₗᵢ[ℝ] E2)

def DiscreteGroups.translationLattice (G : Subgroup M₂) : Set E2

theorem DiscreteGroups.conj_translation (g : M₂) (v : E2) : g * AffineIsometryEquiv.constVAdd ℝ E2 v * g⁻¹ = AffineIsometryEquiv.constVAdd ℝ E2 ((AffineIsometryEquiv.linearIsometryEquiv g) v)

theorem DiscreteGroups.point_group_preserves_lattice (G : Subgroup M₂) (A : E2 ≃ₗᵢ[ℝ] E2) (hA : A ∈ pointGroupSet G) (v : E2) (hv : v ∈ translationLattice G) : A v ∈ translationLattice G

theorem DiscreteGroups.discrete_subgroup_R2_classification (G : AddSubgroup E2) [DiscreteTopology ↥G] : G = ⊥ ∨ (∃ (α : E2), α ≠ 0 ∧ G = AddSubgroup.zmultiples α) ∨ ∃ (a : E2) (b : E2), LinearIndependent ℝ ![a, b] ∧ G = AddSubgroup.zmultiples a ⊔ AddSubgroup.zmultiples b