snd_pow

Mathlib.Algebra.GradedMonoid

URI: https://scilib.ai/kg/mathlib#GradedMonoid.snd_pow

English

For x in GradedMonoid A and n in N, the second component of x^n is GMonoid.gnpow n applied to x.snd.

Русский

Для x в GradedMonoid A и n в N вторая компонента x^n равна gnpow n applied к x.snd.

LaTeX

$$$\\mathrm{snd}(x^n) = \\mathrm{GMonoid.gnpow}\ n\\ x.\\mathrm snd$$$

Lean4

@[simp]
theorem snd_pow [AddMonoid ι] [GMonoid A] (x : GradedMonoid A) (n : ℕ) : (x ^ n).snd = GMonoid.gnpow n x.snd :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru