isPell_mul — Mathlib

English

If b and c are Pell solutions, then their product bc is also a Pell solution.

Русский

Если b и c — решения Пелля, то их произведение bc тоже является решением Пелля.

LaTeX

$$$\forall d,\; (\forall b,c:\\mathbb{Z}\sqrt{d},\; \text{IsPell}(b) \to \text{IsPell}(c) \to \text{IsPell}(b c)).$$$

Lean4

theorem isPell_mul {b c : ℤ√d} (hb : IsPell b) (hc : IsPell c) : IsPell (b * c) :=
  isPell_norm.2 (by simp [mul_comm, mul_left_comm c, mul_assoc, star_mul, isPell_norm.1 hb, isPell_norm.1 hc])

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