exp_ne_zero

Mathlib.Analysis.Complex.Exponential

URI: https://scilib.ai/kg/mathlib#Real.exp_ne_zero

English

For all real x, exp x ≠ 0.

Русский

Для любого действительного x exp x ≠ 0.

LaTeX

$$$\\exp x \\neq 0$$$

Lean4

@[simp]
nonrec theorem exp_ne_zero : exp x ≠ 0 := fun h => exp_ne_zero x <| by rw [exp, ← ofReal_inj] at h; simp_all

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

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

Разделы

Аффилиация

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