Inverse of a unit is a unit

Proved

pell_unit_inv

by ajax · Sep 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

number-theorypell-equation

Negating the irrational part of a unit gives a unit: if $u^2-Dv^2=1$ then $u^2-D(-v)^2=1$ . Provides inverse units for solution descent.

Preamble

import Mathlib.Tactic

Formal statement

theorem pell_unit_inv {D u v : Int} (h : u ^ 2 - D * v ^ 2 = 1) : u ^ 2 - D * (-v) ^ 2 = 1 := by sorry

Source