English
Let a > 1 and m ≥ n. Then pellZd(a, m−n) = pellZd(a, m) · star(pellZd(a, n)), where star denotes conjugation in the appropriate quadratic ring.
Русский
Пусть a > 1 и m ≥ n. Тогда pellZd(a, m−n) = pellZd(a, m) · star(pellZd(a, n)), где star обозначает сопряжение в соответствующей квадратно-зональной кольцевой структуре.
LaTeX
$$$\\text{pellZd}(a, m-n) = \\text{pellZd}(a, m) \\cdot \\text{star}(\\text{pellZd}(a, n)).$$$
Lean4
theorem pellZd_sub {m n} (h : n ≤ m) : pellZd a1 (m - n) = pellZd a1 m * star (pellZd a1 n) :=
by
let t := pellZd_add a1 n (m - n)
rw [add_tsub_cancel_of_le h] at t
rw [t, mul_comm (pellZd _ n) _, mul_assoc, isPell_norm.1 (isPell_pellZd _ _), mul_one]
