natCast_add_one_cpow_ne_zero — Mathlib

English

For every natural n and every complex z, the value (n+1)^z is never zero.

Русский

Для любого натурального n и любого комплексного z выражение (n+1)^z не равно нулю.

LaTeX

$$$$ (n+1)^{z} \\neq 0\\quad \\text{for all } n \\in \\mathbb{N},\\ z \\in \\mathbb{C}. $$$$

Lean4

theorem natCast_add_one_cpow_ne_zero (n : ℕ) (z : ℂ) : (n + 1 : ℂ) ^ z ≠ 0 :=
  mt (cpow_eq_zero_iff ..).mp fun H ↦ by norm_cast at H; exact H.1

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