ring — Mathlib

English

CauSeq β abv forms a ring under pointwise addition and multiplication: (f+g)(i) = f(i) + g(i) and (f g)(i) = f(i) g(i) for all i.

Русский

CauSeq β abv образует кольцо: сложение и умножение определены покомпонентно: (f+g)(i) = f(i) + g(i) и (f g)(i) = f(i) g(i) для всех i.

LaTeX

$$$\forall f,g \in CauSeq(\beta, abv), \ \forall i,\ (f+g)(i) = f(i) + g(i) \ \wedge \ (f g)(i) = f(i) g(i)$$$

Lean4

instance ring : Ring (CauSeq β abv) :=
  Function.Injective.ring Subtype.val Subtype.val_injective rfl rfl coe_add coe_mul coe_neg coe_sub
    (fun _ _ => coe_smul _ _) (fun _ _ => coe_smul _ _) coe_pow (fun _ => rfl) fun _ => rfl

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