exponent_toSubmonoid — Mathlib

English

For a subgroup H of a group G, the exponent of H considered as a submonoid equals the exponent of H as a subgroup.

Русский

Для подгруппы H группы G экспонента как подмножество равна экспоненте H как подгруппы.

LaTeX

$$$\operatorname{exponent}(H_{\text{toSubmonoid}}) = \operatorname{exponent}(H)$$$

Lean4

@[to_additive]
theorem exponent_toSubmonoid (H : Subgroup G) : Monoid.exponent H.toSubmonoid = Monoid.exponent H :=
  Monoid.exponent_eq_of_mulEquiv (MulEquiv.subgroupCongr rfl)

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