G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
this : exponent G ≠ 0 ↔ Set.Finite (Set.range orderOf)
⊢ exponent G = 0 ↔ Set.Infinite (Set.range orderOf)
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
⊢ exponent G = 0 ↔ Set.Infinite (Set.range orderOf)
have := exponent_ne_zero_iff_range_orderOf_finite h
no goals
G : Type u
inst✝ : Monoid G
h : ∀ (g : G), 0 < orderOf g
this : exponent G ≠ 0 ↔ Set.Finite (Set.range orderOf)
⊢ exponent G = 0 ↔ Set.Infinite (Set.range orderOf)
rwa [Ne.def, not_iff_comm, Iff.comm] at this