instCommRing — Mathlib

English

If R is a commutative ring, then SymmetricAlgebra R M carries a commutative ring structure extending the base ring structure.

Русский

Если R — коммутативное кольцо, то SymmetricAlgebra R M имеет структуру коммутативного кольца, расширяющую структуру базового кольца.

LaTeX

$$instance : CommRing (SymmetricAlgebra R M)$$

Lean4

instance (R M) [CommRing R] [AddCommMonoid M] [Module R M] : CommRing (SymmetricAlgebra R M)
    where
  __ := inferInstanceAs (CommSemiring (SymmetricAlgebra R M))
  __ := inferInstanceAs (Ring (RingQuot (SymRel R M)))

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