cpow_zero

Mathlib.Analysis.SpecialFunctions.Pow.Complex

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

English

For any x, x^0 = 1.

Русский

Для любого x: x^0 = 1.

LaTeX

$$$$ x^{0} = 1. $$$$

Lean4

@[simp]
theorem cpow_zero (x : ℂ) : x ^ (0 : ℂ) = 1 := by simp [cpow_def]

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

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

Разделы

Аффилиация

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