coe_gnpow — Mathlib

English

The lemma asserts that the coercion of graded gnpow equals the pow in the underlying type.

Русский

Лемма утверждает, что приведение gnpow через градуированные элементы равняется обычной степени в базовом типе.

LaTeX

$$$\\uparrow(\\mathrm{GMonoid.Gnpow}\ n\ x) = (\\uparrow x)^n$$$

Lean4

@[simp]
theorem coe_gnpow {S : Type*} [SetLike S R] [Monoid R] [AddMonoid ι] (A : ι → S) [SetLike.GradedMonoid A] {i : ι}
    (x : A i) (n : ℕ) : ↑(@GradedMonoid.GMonoid.gnpow _ (fun i => A i) _ _ n _ x) = (x : R) ^ n :=
  rfl

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