exp_sub

Mathlib.Analysis.Complex.Circle

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

English

The substraction rule holds for circle exponential: exp(x - y) = exp x / exp y.

Русский

Правило вычитания верно для экспоненты окружности: exp(x − y) = exp x / exp y.

LaTeX

$$$$ \\exp(x - y) = \\frac{\\exp x}{\\exp y}. $$$$

Lean4

@[simp]
theorem exp_sub (x y : ℝ) : exp (x - y) = exp x / exp y :=
  expHom.map_sub x y

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

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

Разделы

Аффилиация

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