one_cpow

Mathlib.Analysis.SpecialFunctions.Pow.Complex

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

English

The base 1 raised to any exponent equals 1: 1^x = 1.

Русский

База 1 в любой показатель равна 1: 1^x = 1.

LaTeX

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

Lean4

@[simp]
theorem one_cpow (x : ℂ) : (1 : ℂ) ^ x = 1 := by
  rw [cpow_def]
  split_ifs <;> simp_all [one_ne_zero]

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

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

Разделы

Аффилиация

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