mul_star — Mathlib

English

Let d be an integer. For all integers x and y, the product of the element x + y√d with its conjugate equals x^2 − d y^2.

Русский

Пусть d — целое. Для любых целых x и y элемент x + y√d, умноженный на свой сопряжённый, равен x^2 − d y^2.

LaTeX

$$$(x + y\sqrt{d})(x - y\sqrt{d}) = x^2 - d y^2$$$

Lean4

theorem mul_star {x y : ℤ} : (⟨x, y⟩ * star ⟨x, y⟩ : ℤ√d) = x * x - d * y * y := by
  ext <;> simp [sub_eq_add_neg, mul_comm]

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