pellZd_add — Mathlib

English

The Pell Z-sequence is multiplicative: pellZd(a1, m+n) = pellZd(a1, m) · pellZd(a1, n).

Русский

Последовательность Pell Z является мультипликативной: pellZd(a1, m+n) = pellZd(a1, m) · pellZd(a1, n).

LaTeX

$$$ pellZd(a1, m+n) = pellZd(a1, m) \cdot pellZd(a1, n) $$$

Lean4

theorem pellZd_add (m) : ∀ n, pellZd a1 (m + n) = pellZd a1 m * pellZd a1 n
  | 0 => (mul_one _).symm
  | n + 1 => by rw [← add_assoc, pellZd_succ, pellZd_succ, pellZd_add _ n, ← mul_assoc]

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