orderOf_eq_card_of_forall_mem_powers

English

If every element x lies in Submonoid.powers g, then orderOf g equals card α.

Русский

Если каждый элемент α лежит в Submonoid.powers g, то orderOf g = card α.

LaTeX

$$orderOf g = Nat.card α, если ∀ x, x ∈ Submonoid.powers g$$

Lean4

@[to_additive]
theorem orderOf_eq_card_of_forall_mem_powers {g : α} (hx : ∀ x, x ∈ Submonoid.powers g) : orderOf g = Nat.card α :=
  by
  rw [orderOf_eq_card_of_forall_mem_zpowers]
  exact fun x ↦ Submonoid.powers_le_zpowers _ (hx _)

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