instNeg — Mathlib

English

The alternating maps carry an additive commutative group structure, defined pointwise.

Русский

Чередующиеся отображения образуют добавочную коммутативную группу, определяемую по точкам.

LaTeX

$$$\operatorname{AlternatingMap}(R,M,N,\iota) \text{ is an AddCommGroup under addition and negation.}$$$

Lean4

instance instNeg : Neg (M [⋀^ι]→ₗ[R] N') :=
  ⟨fun f =>
    { -(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] }⟩

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