ofSubsingletonₗ — Mathlib

English

Repeated composition laws hold similarly to the basic associativity: (g.comp g').compMultilinearMap f = g.compMultilinearMap (g'.compMultilinearMap f).

Русский

Повторные законы композиции аналогичны базовой ассоциации: (g.comp g').compMultilinearMap f = g.compMultilinearMap (g'.compMultilinearMap f).

LaTeX

$$$$ (g.comp g').compMultilinearMap f = g.compMultilinearMap (g'.compMultilinearMap f). $$$$

Lean4

/-- Linear equivalence between linear maps `M₂ →ₗ[R] M₃`
and one-multilinear maps `MultilinearMap R (fun _ : ι ↦ M₂) M₃`. -/
@[simps +simpRhs]
def ofSubsingletonₗ [Subsingleton ι] (i : ι) : (M₂ →ₗ[R] M₃) ≃ₗ[S] MultilinearMap R (fun _ : ι ↦ M₂) M₃ :=
  { ofSubsingleton R M₂ M₃ i with
    map_add' := fun _ _ ↦ rfl
    map_smul' := fun _ _ ↦ rfl }

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