ofAdd_mul

Mathlib.Algebra.Group.Nat.TypeTags

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

English

ofAdd (a*b) = ofAdd a ^ b for natural numbers a,b.

Русский

ofAdd (a·b) = (ofAdd a)^b для натуральных a,b.

LaTeX

$$$ ofAdd (a \cdot b) = ofAdd a ^ b $$$

Lean4

@[simp]
theorem ofAdd_mul (a b : ℕ) : ofAdd (a * b) = ofAdd a ^ b :=
  (toAdd_pow _ _).symm

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

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

Разделы

Аффилиация

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