yz_sub — Mathlib

English

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

Русский

Для a > 1 и m ≥ n верно: yz(a, m−n) = xz(a, n) yz(a, m) − xz(a, m) yz(a, n).

LaTeX

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

Lean4

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

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