const_pow — Mathlib

English

If M has a Monoid structure, then Germ_l M inherits a Monoid structure, i.e., multiplication and one are defined consistently via representatives.

Русский

Если у M есть структура моноида, то Germ_l M наследует моноидную структуру; умножение и единица задаются согласованно через представителей.

LaTeX

$$$[Monoid\\ M] \\Rightarrow Monoid(\\mathrm{Germ}_l M).$$$

Lean4

@[to_additive (attr := simp, norm_cast)]
theorem const_pow [Pow G M] (a : G) (n : M) : (↑(a ^ n) : Germ l G) = (↑a : Germ l G) ^ n :=
  rfl

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