constOfIsEmpty — Mathlib

English

If ι is empty, then the constant map with value m is an alternating multilinear map from M to N indexed by ι.

Русский

Если ι пусто, то константное отображение с фиксированным значением m является чередующимся мультилейновым отображением из M в N, индексируемым ι.

LaTeX

$$$ [IsEmpty ι] \Rightarrow \text{constOfIsEmpty}_R(M,N,ι)(m) \in \operatorname{AltMap}_R(M,N,ι) $$$

Lean4

/-- The constant map is alternating when `ι` is empty. -/
@[simps -fullyApplied]
def constOfIsEmpty [IsEmpty ι] (m : N) : M [⋀^ι]→ₗ[R] N :=
  { MultilinearMap.constOfIsEmpty R _ m with
    toFun := Function.const _ m
    map_eq_zero_of_eq' := fun _ => isEmptyElim }

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