formalMultilinearSeries_geometric_eq_ofScalars

English

The geometric series is defined as a formal multilinear series by mapping n to the nth Pi-algebraic map.

Русский

Геометрический ряд определяется как формальная многочленная серия, сопоставляющая n-ю компоненту соответствующей алгебраической карты.

LaTeX

$$$\text{formalMultilinearSeries_geometric }\mathbb{K} A = \text{ContinuousMultilinearMap.mkPiAlgebraFin }\mathbb{K} n A$$$

Lean4

/-- The geometric series as an `ofScalars` series. -/
theorem formalMultilinearSeries_geometric_eq_ofScalars :
    formalMultilinearSeries_geometric 𝕜 A = FormalMultilinearSeries.ofScalars A fun _ ↦ (1 : 𝕜) := by
  simp_rw [FormalMultilinearSeries.ext_iff, FormalMultilinearSeries.ofScalars, formalMultilinearSeries_geometric,
    one_smul, implies_true]

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