mkPiRing_apply — Mathlib

English

For m: Fin n → A, the value of mkPiAlgebraFin is the product of the components of m: (List.ofFn m).prod.

Русский

Для m: Fin n → A, значение mkPiAlgebraFin равно произведению элементов m: (List.ofFn m).prod.

LaTeX

$$$$\mathrm{mkPiAlgebraFin}_R^{n,A}(m) = \prod_{i=1}^n m_i.$$$$

Lean4

@[simp]
theorem mkPiRing_apply [Fintype ι] (z : M₂) (m : ι → R) :
    (MultilinearMap.mkPiRing R ι z : (ι → R) → M₂) m = (∏ i, m i) • z :=
  rfl

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