case intro
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
val✝ : Fintype G
⊢ exponent G ≠ 0
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
⊢ exponent G ≠ 0
cases nonempty_fintype G
no goals
case intro
G : Type u
inst✝¹ : LeftCancelMonoid G
inst✝ : Finite G
val✝ : Fintype G
⊢ exponent G ≠ 0
simpa [← lcm_order_eq_exponent, Finset.lcm_eq_zero_iff] using fun x => (orderOf_pos x).ne'