neg_prod_neg — Mathlib

English

Negation distributes over the product of two continuous multilinear maps: (−f).prod (−g) = −(f.prod g).

Русский

Отрицание распространяется на произведение: (−f).prod (−g) = −(f.prod g).

LaTeX

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

Lean4

theorem neg_prod_neg [AddCommGroup M₃] [Module R M₃] [TopologicalSpace M₃] [IsTopologicalAddGroup M₃]
    (f : ContinuousMultilinearMap R M₁ M₂) (g : ContinuousMultilinearMap R M₁ M₃) : (-f).prod (-g) = -f.prod g :=
  rfl

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