instCommRing — Mathlib

English

The degree-zero component A(0) is endowed with a commutative ring structure inherited from R.

Русский

Компонента нулевой степени A(0) несёт структуру коммутативного кольца, унаследованную от R.

LaTeX

$$A_0 is a commutative ring with operations inherited from R.$$

Lean4

/-- The commutative ring `A 0` inherited from `R` in the presence of `SetLike.GradedMonoid A`. -/
instance instCommRing : CommRing (A 0) :=
  (subring A).toCommRing

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