instMonoid — Mathlib

English

The Monoid instance on Germ_l M is determined by the Monoid structure on M, via the germ construction.

Русский

Экземпляр моноида на Germ_l M задаётся структурой моноида на M через конструкцию жермов.

LaTeX

$$$\\text{Monoid}(M) \\Rightarrow \\text{Germ}_lM\\text{ is a Monoid with the induced operations.}$$$

Lean4

@[to_additive]
instance instMonoid [Monoid M] : Monoid (Germ l M) :=
  {
    Function.Surjective.monoid ofFun Quot.mk_surjective (by rfl) (fun _ _ => by rfl) fun _ _ => by
      rfl with
    toSemigroup := instSemigroup
    toOne := instOne
    npow := fun n a => a ^ n }

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