mk_zero_pow

Mathlib.Algebra.GradedMonoid

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

English

For a ∈ A 0 and n ∈ N, mk 0 (a^n) = mk 0 a^n.

Русский

Для a ∈ A 0 и n ∈ N верно mk 0 (a^n) = mk 0 a^n.

LaTeX

$$$\\mathrm{mk}\\ 0\$a^n\$ = \\mathrm{mk}\\ 0\\ a^n$$$

Lean4

@[simp]
theorem mk_zero_pow (a : A 0) (n : ℕ) : mk _ (a ^ n) = mk _ a ^ n :=
  Sigma.ext (nsmul_zero n).symm <| eqRec_heq _ _

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

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

Разделы

Аффилиация

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