instAddCommGroup — Mathlib

English

The generalized coe_sub holds for the generalized Sub operation on alternating maps.

Русский

Обобщённое соотношение coe_sub сохраняется для обобщённой операции Sub над чередующимися отображениями.

LaTeX

$$$ (\text{Sub}(g,g2)).toMultilinearMap = g.toMultilinearMap - g2.toMultilinearMap. $$$

Lean4

instance instAddCommGroup : AddCommGroup (M [⋀^ι]→ₗ[R] N') :=
  fast_instance%coe_injective.addCommGroup _ rfl (fun _ _ => rfl) (fun _ => rfl) (fun _ _ => rfl)
      (fun _ _ => coeFn_smul _ _) fun _ _ => coeFn_smul _ _

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