monoid — Mathlib

English

The grade-zero component A 0 forms a Monoid under the inherited structure from the graded monoid A.

Русский

Компонента нулевой грады A 0 образует моноид по унаследованной структуре от градуированного моноида A.

LaTeX

$$$\\text{Monoid}(A\\,0)$$$

Lean4

/-- The `Monoid` structure derived from `GMonoid A`. -/
instance monoid : Monoid (A 0) :=
  Function.Injective.monoid (mk 0) sigma_mk_injective rfl mk_zero_smul mk_zero_pow

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