orderOf_submonoid — Mathlib

English

For any isomorphism-like relation between a Submonoid H and its ambient G, the order of an element y ∈ H computed in H equals its order in G.

Русский

Порядок элемента y, взятого в Submonoid H, равен порядку того же элемента в G.

LaTeX

$$$ \forall {G} [Monoid G] {H : Submonoid G} (y : H), ord(y)_{G} = ord(y)_{H}$$$

Lean4

@[to_additive (attr := norm_cast, simp)]
theorem orderOf_submonoid {H : Submonoid G} (y : H) : orderOf (y : G) = orderOf y :=
  orderOf_injective H.subtype Subtype.coe_injective y

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