orderOf_eq — Mathlib

English

A multiplicative equivalence preserves the order of elements: ord(e(x)) = ord(x).

Русский

Кратное эквивалентное отображение сохраняет порядок элементов: ord(e(x)) = ord(x).

LaTeX

$$$ \forall {G} [Monoid G] {H} [Monoid H] (e : G ≃* H) (x : G), ord(e(x)) = ord(x)$$$

Lean4

/-- A multiplicative equivalence preserves orders of elements. -/
@[to_additive (attr := simp) /-- An additive equivalence preserves orders of elements. -/
    ]
theorem orderOf_eq {H : Type*} [Monoid H] (e : G ≃* H) (x : G) : orderOf (e x) = orderOf x :=
  orderOf_injective e.toMonoidHom e.injective x

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