addGroup — Mathlib

English

CauSeq β abv carries an additive group structure, defined pointwise, compatible with the underlying sequence operations.

Русский

CauSeq β abv обладает структурой аддитивной группы, определяемой по координатам и совместимой с операциями последовательности.

LaTeX

$$$$ \mathrm{CauSeq} \\, β \\, abv \text{ is an additive group under pointwise operations.} $$$$

Lean4

instance addGroup : AddGroup (CauSeq β abv) :=
  Function.Injective.addGroup Subtype.val Subtype.val_injective rfl coe_add coe_neg coe_sub (fun _ _ => coe_smul _ _)
    fun _ _ => coe_smul _ _

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