xz_sub — Mathlib

English

For a > 1 and m ≥ n, xz(a, m−n) = xz(a, m) xz(a, n) − d(a) yz(a, m) yz(a, n).

Русский

Для a > 1 и m ≥ n выполняется: xz(a, m−n) = xz(a, m) xz(a, n) − d(a) yz(a, m) yz(a, n).

LaTeX

$$$\\text{xz}^{(a)}(m-n) = \\text{xz}^{(a)}(m) \\cdot \\text{xz}^{(a)}(n) - d(a)\\, yz^{(a)}(m)\\, yz^{(a)}(n).$$$

Lean4

theorem xz_sub {m n} (h : n ≤ m) : xz a1 (m - n) = xz a1 m * xz a1 n - d a1 * yz a1 m * yz a1 n :=
  by
  rw [sub_eq_add_neg, ← mul_neg]
  exact congr_arg Zsqrtd.re (pellZd_sub a1 h)

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