coe_pi — Mathlib

English

The linear map π f has linear map form equal to the product of the component maps, i.e., (pi f).toLinearMap = LinearMap.pi (i ↦ f_i).

Русский

Линейное отображение π f имеет вид произведения компонентных отображений: (pi f).toLinearMap = LinearMap.pi (i ↦ f_i).

LaTeX

$$$(\\pi f).toLinearMap = \\mathrm{LinearMap.pi}\\bigl( i \\mapsto f_i \\bigr)$$$

Lean4

@[simp]
theorem coe_pi (f : ∀ i, M →L[R] φ i) : (pi f : M →ₗ[R] ∀ i, φ i) = LinearMap.pi fun i => f i :=
  rfl

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