coe_neg — Mathlib

English

Scalar multiplication on the space of alternating maps acts by multiplying the values of f by the scalar.

Русский

Скалярное умножение на пространство чередующихся отображений действует умножением значений отображения на скаляр.

LaTeX

$$$ (s \cdot f)(v) = s \cdot (f(v)). $$$

Lean4

@[norm_cast]
theorem coe_neg : ((-g : M [⋀^ι]→ₗ[R] N') : MultilinearMap R (fun _ : ι => M) N') = -g :=
  rfl

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