coe_multilinearMap_injective — Mathlib

English

The map f ↦ f.toMultilinearMap is injective; different alternating maps give different multilinear maps.

Русский

Отображение f к f.toMultilinearMap инъективно; разные чередующиеся отображения порождают разные много-линейные отображения.

LaTeX

$$∀ {R} [Semiring R] {ι} (f g : AlternatingMap R M N ι), Function.Injective AlternatingMap.toMultilinearMap$$

Lean4

theorem coe_multilinearMap_injective :
    Function.Injective ((↑) : M [⋀^ι]→ₗ[R] N → MultilinearMap R (fun _ : ι => M) N) := fun _ _ h =>
  ext <| MultilinearMap.congr_fun h

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