toAdd_pow

Mathlib.Algebra.Group.Nat.TypeTags

URI: https://scilib.ai/kg/mathlib#Nat.toAdd_pow

English

For a ∈ Multiplicative ℕ and b ∈ ℕ, (a^b).toAdd = a.toAdd * b.

Русский

Для a ∈ Multiplicative ℕ и b ∈ ℕ, (a^b).toAdd = a.toAdd · b.

LaTeX

$$$ (a^b).toAdd = a.toAdd \cdot b $$$

Lean4

theorem toAdd_pow (a : Multiplicative ℕ) (b : ℕ) : (a ^ b).toAdd = a.toAdd * b :=
  mul_comm _ _

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

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

Разделы

Аффилиация

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