Units are closed under composition
Provedpell_unit_mulnumber-theorypell-equation
Norm-one elements compose to norm-one elements: the product of two units in a quadratic integer ring is a unit. Gives the unit group its closure.
Preamble
import Mathlib.Tactic
Formal statement
theorem pell_unit_mul {D a b c d : Int} (h1 : a ^ 2 - D * b ^ 2 = 1) (h2 : c ^ 2 - D * d ^ 2 = 1) : (a * c + D * b * d) ^ 2 - D * (b * c + a * d) ^ 2 = 1 := by sorrySource