orderOf_units — Mathlib

English

For a unit u ∈ Gˣ, the order of u considered in G equals the order of u in the group of units.

Русский

Порядок единицы u ∈ Gˣ, взятый как элемент G, равен порядку u в группе единиц.

LaTeX

$$$ \forall {G} [Monoid G] (u : Gˣ), ord(u : G) = ord(u)$$$

Lean4

@[to_additive (attr := norm_cast)]
theorem orderOf_units {y : Gˣ} : orderOf (y : G) = orderOf y :=
  orderOf_injective (Units.coeHom G) Units.val_injective y

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