instSMul — Mathlib

English

There is a scalar action of S on the space of alternating maps defined via scalar action on the target, compatible with the multilinear structure.

Русский

Существует действие скаляра S на множество чередующихся отображений, заданное через действие на цель и совместимое с много-линейной структурой.

LaTeX

$$instance instSMul : SMul S (M [⋀^ι]→ₗ[R] N)$$

Lean4

instance instSMul : SMul S (M [⋀^ι]→ₗ[R] N) :=
  ⟨fun c f =>
    { c • (f : MultilinearMap R (fun _ : ι => M) N) with
      map_eq_zero_of_eq' := fun v i j h hij => by simp [f.map_eq_zero_of_eq v h hij] }⟩

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