power_mul

Mathlib.SetTheory.Cardinal.Order

URI: https://scilib.ai/kg/mathlib#Cardinal.power_mul

← MathLib Explorer

English

For all cardinals a, b, c, one has a^(b·c) = (a^b)^c.

Русский

Для всех кардиналов a, b, c выполняется a^(b·c) = (a^b)^c.

LaTeX

$$$a^{\,b \cdot c} = (a^{\,b})^{\,c}$$$

Lean4

theorem power_mul {a b c : Cardinal} : a ^ (b * c) = (a ^ b) ^ c :=
  by
  rw [mul_comm b c]
  exact inductionOn₃ a b c fun α β γ => mk_congr <| Equiv.curry γ β α

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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