cosh_zero

Mathlib.Analysis.Complex.Trigonometric

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

English

The complex cosh at zero is one: cosh(0) = 1.

Русский

Комплексный cosh в нуле равен единице: cosh(0) = 1.

LaTeX

$$$$ \cosh 0 = 1 $$$$

Lean4

@[simp]
theorem cosh_zero : cosh 0 = 1 := by simp [cosh]

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

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

Разделы

Аффилиация

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