compLinearMap — Mathlib

English

The composed linear map corresponds to the composition of the underlying functions.

Русский

Скомпонование линейного отображения соответствует композиции базовых функций.

LaTeX

$$$ \text{coe}(f) = f \circ (g \circ \cdot) $$$

Lean4

/-- Composing an alternating map with the same linear map on each argument gives again an
alternating map. -/
def compLinearMap (f : M [⋀^ι]→ₗ[R] N) (g : M₂ →ₗ[R] M) : M₂ [⋀^ι]→ₗ[R] N :=
  { (f : MultilinearMap R (fun _ : ι => M) N).compLinearMap fun _ => g with
    map_eq_zero_of_eq' := fun _ _ _ h hij => f.map_eq_zero_of_eq _ (LinearMap.congr_arg h) hij }

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