mkPiRing_apply_one_eq_self — Mathlib

English

If f is a multilinear map from R^ι to M2, then mkPiRing applied to the constant-1 vector equals f.

Русский

Если f — мультиленейное отображение от R^ι к M2, то mkPiRing применённый к константе 1 равен f.

LaTeX

$$$$\mathrm{mkPiRing}_R^{ι}(\,f(1,1,\dots,1)\,) = f.$$$$

Lean4

theorem mkPiRing_apply_one_eq_self [Fintype ι] (f : MultilinearMap R (fun _ : ι => R) M₂) :
    MultilinearMap.mkPiRing R ι (f fun _ => 1) = f := by
  ext
  simp

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