ne_zero — Mathlib

English

If IsPrimitiveRoot ζ k holds with a nontrivial monoid-with-zero, and k ≠ 0, then ζ ≠ 0.

Русский

Если IsPrimitiveRoot ζ k верно в ненулевом моноиде, и k ≠ 0, тогда ζ ≠ 0.

LaTeX

$$$$\text{If } IsPrimitiveRoot(\zeta,k) \land k \neq 0, \text{ then } \zeta \neq 0.$$$$

Lean4

protected theorem ne_zero [Nontrivial M₀] {ζ : M₀} (h : IsPrimitiveRoot ζ k) : k ≠ 0 → ζ ≠ 0 :=
  mt fun hn ↦ h.unique (hn.symm ▸ IsPrimitiveRoot.zero)

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