English
An injective monoid homomorphism preserves the order of elements: ord(f(x)) = ord(x).
Русский
Инъективный гомоморфизм моноидов сохраняет порядок элементов: ord(f(x)) = ord(x).
LaTeX
$$$ \forall {G H} [Monoid G][Monoid H] (f : G \to_* H) (hf : Function.Injective f) (x : G), ord(f(x)) = ord(x)$$$
Lean4
/-- An injective homomorphism of monoids preserves orders of elements. -/
@[to_additive /-- An injective homomorphism of additive monoids preserves orders of elements. -/
]
theorem orderOf_injective {H : Type*} [Monoid H] (f : G →* H) (hf : Function.Injective f) (x : G) :
orderOf (f x) = orderOf x := by simp_rw [orderOf_eq_orderOf_iff, ← f.map_pow, ← f.map_one, hf.eq_iff, forall_const]
