fg_of_addMonoid_fg — Mathlib

English

There is an instance that transforms AddMonoid.FG M into Monoid.FG (Multiplicative M).

Русский

Существует экземпляр перехода AddMonoid.FG M в Monoid.FG (Multiplicative M).

LaTeX

$$$\\text{instance } fg_of_addMonoid_fg : AddMonoid.FG M \\Rightarrow Monoid.FG (Multiplicative M)$$$

Lean4

instance fg_of_addMonoid_fg {M : Type*} [AddMonoid M] [AddMonoid.FG M] : Monoid.FG (Multiplicative M) :=
  AddMonoid.fg_iff_mul_fg.1
    ‹_›
      -- This was previously a global instance,
      -- but it doesn't appear to be used and has been implicated in slow typeclass resolutions.

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