exp_pi_ne_one

Mathlib.Analysis.Complex.Circle

URI: https://scilib.ai/kg/mathlib#Circle.exp_pi_ne_one

← MathLib Explorer

English

The unit circle exponential at π is not the identity: exp(π) ≠ 1.

Русский

Экспонента окружности в π не равна единице: exp(π) ≠ 1.

LaTeX

$$$$ \\exp(\\pi) \\neq 1. $$$$

Lean4

theorem exp_pi_ne_one : Circle.exp Real.pi ≠ 1 := by
  intro h
  have heq : (Circle.exp Real.pi : ℂ) = 1 := by simp [h]
  rw [Circle.coe_exp, exp_pi_mul_I] at heq
  norm_num at heq

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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