exponent_eq_zero_iff — Mathlib

English

Exponent equals zero iff there is no global exponent: exponent(G) = 0 ⇔ ¬ExponentExists(G).

Русский

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

LaTeX

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

Lean4

@[to_additive]
theorem exponent_eq_zero_iff : exponent G = 0 ↔ ¬ExponentExists G :=
  exponent_ne_zero.not_right

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