Intersection_of_Subgroups_of_Prime_Order
Provedgroup-theoryprime-orderproofwikisubgroup
Let G be a group and H, K subgroups of prime order p with H ≠ K. Then H ∩ K = {e}.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.Data.Nat.Prime.Basic
Formal statement
import Mathlib.Analysis.Complex.Basic
import Mathlib.Data.Nat.Prime.Basic
theorem Intersection_of_Subgroups_of_Prime_Order {G : Type _} [Group G] (H K : Subgroup G) [Fintype H] [Fintype K] (p : ℕ) (hp : Nat.Prime p) (hH : Fintype.card H = p) (hK : Fintype.card K = p) (hne : H ≠ K) : H ⊓ K = ⊥ := by sorrySource