instAddCommGroup — Mathlib

English

The family of left-invariant derivations forms an additive commutative group under pointwise addition.

Русский

Множество лево-инвариантных выводов образует аддитивную коммутативную группу по точечному сложению.

LaTeX

$$$ \mathrm{LeftInvariantDerivation}(I,G) \text{ is an additive commutative group under } +. $$$

Lean4

instance : AddCommGroup (LeftInvariantDerivation I G) :=
  coe_injective.addCommGroup _ coe_zero coe_add coe_neg coe_sub (fun _ _ => rfl) fun _ _ => rfl

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