coe_pi — Mathlib

English

A formalization detail: the same equality as above holds in the generalized setting with indexed families.

Русский

Детали формализации: такое же равенство сохраняется и в обобщенном виде с индексированной семью.

LaTeX

$$$ (\pi f) = \operatorname{MultilinearMap}.pi (\lambda a. (f(a)).toMultilinearMap). $$$

Lean4

@[simp]
theorem coe_pi {ι' : Type*} {N : ι' → Type*} [∀ i, AddCommMonoid (N i)] [∀ i, Module R (N i)]
    (f : ∀ i, M [⋀^ι]→ₗ[R] N i) :
    (pi f : MultilinearMap R (fun _ : ι => M) (∀ i, N i)) = MultilinearMap.pi fun a => f a :=
  rfl

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