addCommMonoid — Mathlib

English

Re-stating central scalar property for the AltMap space with the given scalar actions.

Русский

Повторное утверждение центральности скаляров для пространства AltMap при заданных действиях скаляров.

LaTeX

$$$ IsCentralScalar R' (ContinuousAlternatingMap A M N ι) $$$

Lean4

instance addCommMonoid : AddCommMonoid (M [⋀^ι]→L[R] N) :=
  toContinuousMultilinearMap_injective.addCommMonoid _ rfl (fun _ _ => rfl) fun _ _ => rfl

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