instSub — Mathlib

English

The subtraction of alternating maps is defined pointwise: (f - g)(v) = f(v) - g(v).

Русский

Разность чередующихся отображений определяется по точкам: (f - g)(v) = f(v) - g(v).

LaTeX

$$$ (f - g)(v) = f(v) - g(v). $$$

Lean4

instance instSub : Sub (M [⋀^ι]→ₗ[R] N') :=
  ⟨fun f g =>
    { (f - g : 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, g.map_eq_zero_of_eq v h hij] }⟩

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