sphere — Mathlib

English

Sphere(n,d,k) is the intersection of the box with the integer lattice points whose coordinate squares sum to k: sphere(n,d,k) = { x ∈ box(n,d) : ∑ i x(i)^2 = k }.

Русский

Сфера sphere(n,d,k) — пересечение ящика и целочисленной решетки точек, у которых сумма квадратов координат равна k: sphere(n,d,k) = { x ∈ box(n,d) : ∑ i x(i)^2 = k }.

LaTeX

$$$$ \mathrm{sphere}(n,d,k) = \{ x \in \mathrm{box}(n,d) : \sum_i x(i)^2 = k \} $$$$

Lean4

/-- The intersection of the sphere of radius `√k` with the integer points in the positive
quadrant. -/
def sphere (n d k : ℕ) : Finset (Fin n → ℕ) :=
  {x ∈ box n d | ∑ i, x i ^ 2 = k}

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