G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
⊢ exponent G ∣ Finset.lcm Finset.univ orderOf
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
⊢ Finset.lcm Finset.univ orderOf = exponent G
apply Nat.dvd_antisymm (lcm_orderOf_dvd_exponent G)
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
g : G
⊢ g ^ Finset.lcm Finset.univ orderOf = 1
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
⊢ exponent G ∣ Finset.lcm Finset.univ orderOf
refine' exponent_dvd_of_forall_pow_eq_one G _ fun g => _
case intro
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
g : G
m : ℕ
hm : Finset.lcm Finset.univ orderOf = orderOf g * m
⊢ g ^ Finset.lcm Finset.univ orderOf = 1
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
g : G
⊢ g ^ Finset.lcm Finset.univ orderOf = 1
obtain ⟨m, hm⟩ : orderOf g ∣ Finset.univ.lcm orderOf := Finset.dvd_lcm (Finset.mem_univ g)
no goals
case intro
G : Type u
inst✝¹ : Monoid G
inst✝ : Fintype G
g : G
m : ℕ
hm : Finset.lcm Finset.univ orderOf = orderOf g * m
⊢ g ^ Finset.lcm Finset.univ orderOf = 1
rw [hm, pow_mul, pow_orderOf_eq_one, one_pow]