orderOf_dvd_card

Stream: mathlib4

[BANGJI HU]

I want to use the fact that the order of a subgroup divides the order of the group to prove that a|4, but there is a type mismatch.

import Mathlib.GroupTheory.OrderOfElement
import Mathlib.GroupTheory.SpecificGroups.Cyclic

open Group

variable (G : Type*) [Group G] [Fintype G] (hG : Fintype.card G = 4)

theorem group_of_order_four : IsCyclic G ∨ (∀ a : G, a^2 = 1) := by
  by_cases h : IsCyclic G
  · left; exact h
  · right
    intro a
    have h1 : orderOf a ∣ 4 := orderOf_dvd_card

[Jihoon Hyun]

That is because 4 is not Fintype.card G unless hG.
To make your intentions work:

import Mathlib.GroupTheory.OrderOfElement
import Mathlib.GroupTheory.SpecificGroups.Cyclic

open Group

variable (G : Type*) [Group G] [Fintype G]

theorem group_of_order_four (hG : Fintype.card G = 4) : IsCyclic G ∨ (∀ a : G, a^2 = 1) := by
  by_cases h : IsCyclic G
  · left; exact h
  · right
    intro a
    have h1 : orderOf a ∣ 4 := hG ▸ orderOf_dvd_card
    sorry

[Aaron Liu]

btw, we have docs#IsKleinFour

[BANGJI HU]

I think I can directly utilize the Klein four-group when it is not a cyclic group.

[BANGJI HU]

HOW TO COMBINE THEM TOGETHER

import Mathlib.GroupTheory.SpecificGroups.Cyclic

import Mathlib.GroupTheory.SpecificGroups.Dihedral

import Mathlib

/-- classify groups of order 4 by two cases-/

example (G : Type) [Group G] (card_four : Nat.card G = 4)

  : IsCyclic G ∨ IsKleinFour G :=

by

  by_cases H : IsCyclic G

  · exact Or.inl H

  · rw [not_isCyclic_iff_exponent_eq_prime Nat.prime_two card_four] at H

    exact Or.inr ⟨card_four, H⟩

/-- A Klein four-group is a group of cardinality four and exponent two. -/

class IsKleinFour1 (G : Type*) [Group G] : Prop where

  card_four : Nat.card G = 4

  exponent_two : Monoid.exponent G = 2