natCast_mul_natCast_cpow

Mathlib.Analysis.SpecialFunctions.Pow.Complex

URI: https://scilib.ai/kg/mathlib#Complex.natCast_mul_natCast_cpow

← MathLib Explorer

English

For m,n ∈ ℕ and s ∈ ℂ, (m n)^s = m^s n^s.

Русский

Для m,n ∈ ℕ и s ∈ ℂ верно (m n)^s = m^s n^s.

LaTeX

$$$((m n) : \mathbb{C})^{s} = (m : \mathbb{C})^{s} (n : \mathbb{C})^{s}$$$

Lean4

theorem natCast_mul_natCast_cpow (m n : ℕ) (s : ℂ) : (m * n : ℂ) ^ s = m ^ s * n ^ s :=
  ofReal_natCast m ▸ ofReal_natCast n ▸ mul_cpow_ofReal_nonneg m.cast_nonneg n.cast_nonneg s

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

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

Разделы

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

Аффилиация

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