exponent_eq_zero_iff_range_orderOf_infinite

English

Exponent equals zero iff the range of orderOf is infinite, assuming every g has positive order.

Русский

Экспонента равна нулю тогда и только тогда, когда диапазон orderOf бесконечен, при условии, что каждый элемент имеет положительный порядок.

LaTeX

$$$\\\\operatorname{exponent} G = 0 \\\\iff \\\\operatorname{Set.range}(\\\\operatorname{orderOf} : G \\\\to \\\\mathbb{N}).\\\\Infinite$$$

Lean4

@[to_additive]
theorem exponent_eq_zero_iff_range_orderOf_infinite (h : ∀ g : G, 0 < orderOf g) :
    exponent G = 0 ↔ (Set.range (orderOf : G → ℕ)).Infinite :=
  by
  have := exponent_ne_zero_iff_range_orderOf_finite h
  rwa [Ne, not_iff_comm, Iff.comm] at this

Похожие утверждения