instMul — Mathlib

English

Multiplication in ℤ√d is given by: (x + y√d)(u + v√d) = (xu + d y v) + (xv + yu)√d, i.e., (x,y)(u,v) = (xu + d y v, xv + yu).

Русский

Умножение в ℤ√d задано: (x + y√d)(u + v√d) = (xu + d y v) + (xv + yu)√d, то есть (x,y)(u,v) = (xu + d y v, xv + yu).

LaTeX

$$$ (x,y)\\cdot(u,v) = (xu + d\\,yv,\, xv + yu). $$$

Lean4

/-- Multiplication in `ℤ√d` -/
instance : Mul (ℤ√d) :=
  ⟨fun z w => ⟨z.1 * w.1 + d * z.2 * w.2, z.1 * w.2 + z.2 * w.1⟩⟩

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