zpow_eq_one_iff — Mathlib

English

For a fundamental Pell solution a, a^n = 1 iff n = 0.

Русский

Для фундаментального решения a: a^n = 1 тогда и только тогда, когда n = 0.

LaTeX

$$$\forall a\in \mathrm{Solution}_1(d), \text{IsFundamental}(a) \rightarrow \forall n\in \mathbb{Z}, a^n = 1 \iff n = 0$$$

Lean4

/-- The `n`th power of a fundamental solution is trivial if and only if `n = 0`. -/
theorem zpow_eq_one_iff {a : Solution₁ d} (h : IsFundamental a) (n : ℤ) : a ^ n = 1 ↔ n = 0 :=
  by
  rw [← zpow_zero a]
  exact ⟨fun H => h.y_strictMono.injective (congr_arg Solution₁.y H), fun H => H ▸ rfl⟩

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