nonneg_mul_lem — Mathlib

English

For any natural x,y and a ∈ Z√d, Nonneg a implies Nonneg (⟨x,y⟩ · a).

Русский

Для любых x,y ∈ ℕ и a ∈ Z√d, неотрицательность a сохраняется под умножением ⟨x,y⟩ · a.

LaTeX

$$$$\forall d \; \forall x,y \in \mathbb{N},\; \forall a \in \mathbb{Z}\sqrt{d},\; a \ge 0 \Rightarrow (\langle x,y\rangle \cdot a) \ge 0.$$$$

Lean4

theorem nonneg_mul_lem {x y : ℕ} {a : ℤ√d} (ha : Nonneg a) : Nonneg (⟨x, y⟩ * a) :=
  by
  have : (⟨x, y⟩ * a : ℤ√d) = (x : ℤ√d) * a + sqrtd * ((y : ℤ√d) * a) := by
    rw [decompose, right_distrib, mul_assoc, Int.cast_natCast, Int.cast_natCast]
  rw [this]
  exact (nonneg_smul ha).add (nonneg_muld <| nonneg_smul ha)

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