exponent_top — Mathlib

English

The exponent of the top submonoid equals the exponent of the ambient monoid.

Русский

Экспонента верхнего подмоноида равна экспоненте исходного моноида.

LaTeX

$$$\\operatorname{exponent}(\\top : \\mathrm{Submonoid} G) = \\operatorname{exponent} G$$$

Lean4

@[to_additive (attr := simp)]
theorem _root_.Submonoid.exponent_top : Monoid.exponent (⊤ : Submonoid G) = Monoid.exponent G :=
  exponent_eq_of_mulEquiv Submonoid.topEquiv

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