instSMulForallFinOfNatNat — Mathlib

English

For any P: Fin 3 → R and u ∈ R, the scalar multiplication is coordinatewise with powers: (u • P) x = u^2 P x, (u • P) y = u^3 P y, (u • P) z = u P z.

Русский

Для любого P: Fin 3 → R и любого u ∈ R скалярное умножение действует по координатам: (u • P) x = u^2 P x, (u • P) y = u^3 P y, (u • P) z = u P z.

LaTeX

$$$(u \cdot P)_x = u^2 P_x$, $(u \cdot P)_y = u^3 P_y$, $(u \cdot P)_z = u P_z$$$

Lean4

/-- The scalar multiplication for a Jacobian point representative on a Weierstrass curve. -/
scoped instance : SMul R <| Fin 3 → R :=
  ⟨fun u P => ![u ^ 2 * P x, u ^ 3 * P y, u * P z]⟩

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