exponent_ne_zero — Mathlib

English

The exponent is nonzero iff there exists a global exponent: exponent(G) ≠ 0 iff ExponentExists(G).

Русский

Экспонента не равна нулю тогда и только тогда, когда существует экспонента глобального масштаба.

LaTeX

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

Lean4

@[to_additive]
theorem exponent_ne_zero : exponent G ≠ 0 ↔ ExponentExists G :=
  by
  rw [exponent]
  split_ifs with h
  ·
    simp [h]
      --if this isn't done this way, `to_additive` freaks

  · tauto

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