exponent_pos — Mathlib

English

The exponent is positive iff there exists a global exponent: 0 < exponent(G) iff ExponentExists(G).

Русский

Экспонента положительна тогда и только тогда, когда существует экспонента: 0 < exponent(G) ⇔ ExponentExists(G).

LaTeX

$$$0 < \\operatorname{exponent}(G) \\iff \\operatorname{ExponentExists}(G)$$$

Lean4

@[to_additive]
theorem exponent_pos : 0 < exponent G ↔ ExponentExists G :=
  pos_iff_ne_zero.trans exponent_ne_zero

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