formalMultilinearSeries_geometric

English

The geometric series 1 + x + x^2 + ... forms a formal multilinear series.

Русский

Геометрический ряд 1 + x + x^2 + ... образует формальную многочленную серию.

LaTeX

$$$\text{formalMultilinearSeries_geometric }\mathbb{K} A : \text{FormalMultilinearSeries}_{\mathbb{K}}(A,A)$$$

Lean4

/-- The geometric series `1 + x + x ^ 2 + ...` as a `FormalMultilinearSeries`. -/
def formalMultilinearSeries_geometric : FormalMultilinearSeries 𝕜 A A := fun n ↦
  ContinuousMultilinearMap.mkPiAlgebraFin 𝕜 n A

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