exponent_additive — Mathlib

English

The exponent of the multiplicative form equals that of the additive form: exponent(Multiplicative G) = exponent G.

Русский

Экспонента умноженной формы равна экспоненте исходной формы: exponent(Multiplicative G) = exponent G.

LaTeX

$$$\\operatorname{exponent}(\\mathrm{Multiplicative}\\,G)=\\operatorname{exponent}(G)$$$

Lean4

@[simp]
theorem _root_.AddMonoid.exponent_additive : AddMonoid.exponent (Additive G) = exponent G :=
  rfl

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