instMonoid — Mathlib

English

The grade-zero part A 0 inherits a Monoid structure from GradeZero.submonoid A.

Русский

Часть нулевой градации A 0 наследует структуру моноида от GradeZero.submonoid A.

LaTeX

$$$\\text{instMonoid} : \\text{Monoid}(A 0)$$$

Lean4

/-- The monoid `A 0` inherited from `R` in the presence of `SetLike.GradedMonoid A`. -/
instance instMonoid : Monoid (A 0) :=
  inferInstanceAs <|
    Monoid
      (GradeZero.submonoid A)
        -- TODO: it might be expensive to unify `A` in this instances in practice

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