instAddCommGroup — Mathlib

English

The AEval construction inherits an additive monoid structure from M when M is an AddCommMonoid.

Русский

AEval наследует моноидную структуру по сложению от M, если M является аддитивным коммутативным моноидом.

LaTeX

$$$ \\text{AddMonoid}(AEval\\,R\\,M\\,a) \\cong \\text{AddMonoid}(M) $$$

Lean4

instance instAddCommGroup {R A M} [CommSemiring R] [Semiring A] (a : A) [Algebra R A] [AddCommGroup M] [Module A M]
    [Module R M] [IsScalarTower R A M] : AddCommGroup <| AEval R M a :=
  inferInstanceAs (AddCommGroup M)

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