instAddCommGroupR — Mathlib

English

If K is a commutative ring, then R(σ, K) has the structure of an additive abelian group.

Русский

Если K — коммутативное кольцо, то R(σ, K) наделено структурой аддитивной абелевой группы.

LaTeX

$$$R(\\\\sigma, K) \\text{ is an additive abelian group.}$$$

Lean4

noncomputable instance [CommRing K] : AddCommGroup (R σ K) :=
  inferInstanceAs (AddCommGroup (restrictDegree σ K (Fintype.card K - 1)))

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