not_iff — Mathlib

English

¬IsPrimitiveRoot ζ k is equivalent to orderOf ζ ≠ k.

Русский

Не является примитивным корнем ζ k эквивалентно тому, что orderOf ζ ≠ k.

LaTeX

$$$$\neg \mathrm{IsPrimitiveRoot}(\zeta,k) \iff \mathrm{orderOf}\zeta \neq k.$$$$

Lean4

protected theorem not_iff : ¬IsPrimitiveRoot ζ k ↔ orderOf ζ ≠ k :=
  ⟨fun h hk ↦ h <| hk ▸ IsPrimitiveRoot.orderOf ζ, fun h hk ↦ h.symm <| hk.unique <| IsPrimitiveRoot.orderOf ζ⟩

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