Finite_Subgroup_Test
Provedgroup-theoryproofwikisubgroup
Let G be a group and H a nonempty finite subset of G. If H is closed under the group operation, then H is also closed under inverses (and hence is a subgroup).
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
theorem Finite_Subgroup_Test {G : Type _} [Group G] (H : Set G) (hne : H.Nonempty) (hfin : H.Finite) (hclosed : ∀ a ∈ H, ∀ b ∈ H, a * b ∈ H) : ∀ a ∈ H, a⁻¹ ∈ H := by sorrySource