Powers of a norm-one element stay norm-one
Provedpell_unit_pownumber-theorypell-equation
Powers of a unit in a quadratic integer ring stay units: if then for all . This generates infinite Pell solution families from one unit.
Preamble
import Mathlib.NumberTheory.Zsqrtd.Basic
Formal statement
theorem pell_unit_pow {d : Int} (a : Zsqrtd d) (h : Zsqrtd.norm a = 1) (n : Nat) : Zsqrtd.norm (a ^ n) = 1 := by sorrySource