exponent_eq_zero_of_infinite — Mathlib

English

If α is an infinite cyclic group, then exponent α = 0.

Русский

Если группа α бесконечна и циклическая, то экспонента равна нулю.

LaTeX

$$exponent α = 0$$

Lean4

@[to_additive]
theorem exponent_eq_zero_of_infinite [Group α] [IsCyclic α] [Infinite α] : exponent α = 0 :=
  let ⟨_, hg⟩ := IsCyclic.exists_generator (α := α)
  exponent_eq_zero_of_order_zero <| Infinite.orderOf_eq_zero_of_forall_mem_zpowers hg

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