orderOf_piMulSingle — Mathlib

English

For any index i and element g in M(i), the order of the embedded element Pi.mulSingle i g equals the order of g.

Русский

Пусть i — индекс, a g ∈ M(i); порядок элемента Pi.mulSingle i g равен порядку g.

LaTeX

$$ \operatorname{order}(\Pi \mathrm{mulSingle} \, i \, g) = \operatorname{order}(g) $$

Lean4

theorem orderOf_piMulSingle {ι : Type*} [DecidableEq ι] {M : ι → Type*} [(i : ι) → Monoid (M i)] (i : ι) (g : M i) :
    orderOf (Pi.mulSingle i g) = orderOf g :=
  orderOf_injective (MonoidHom.mulSingle M i) (Pi.mulSingle_injective i) g

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