eq_zero_cpow_iff

Mathlib.Analysis.SpecialFunctions.Pow.Complex

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

English

Equivalently, a = 0^x holds exactly in the cases described above.

Русский

Эквивалентно, равенство a = 0^x выполняется только в указанных выше случаях.

LaTeX

$$$$ a = 0^{x} \iff (x \neq 0 \land a = 0) \lor (x = 0 \land a = 1). $$$$

Lean4

theorem eq_zero_cpow_iff {x : ℂ} {a : ℂ} : a = (0 : ℂ) ^ x ↔ x ≠ 0 ∧ a = 0 ∨ x = 0 ∧ a = 1 := by
  rw [← zero_cpow_eq_iff, eq_comm]

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

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

Разделы

Аффилиация

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