y_mul_pos — Mathlib

English

The set of Pell solutions with x and y positive is closed under multiplication.

Русский

Набор решений Пелля с x > 0 и y > 0 замкнут относительно умножения.

LaTeX

$$$\forall a,b\in \mathrm{Solution}_1(d),\; (0 < a_x) \land (0 < a_y) \land (0 < b_x) \land (0 < b_y) \rightarrow 0 < (a\cdot b)_y$$$

Lean4

/-- The set of solutions with `x` and `y` positive is closed under multiplication. -/
theorem y_mul_pos {a b : Solution₁ d} (hax : 0 < a.x) (hay : 0 < a.y) (hbx : 0 < b.x) (hby : 0 < b.y) : 0 < (a * b).y :=
  by
  simp only [y_mul]
  positivity

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