log_algebraMap

Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog

URI: https://scilib.ai/kg/mathlib#CFC.log_algebraMap

English

For real r, log(algebraic map of r) equals the algebraic map of log r: log(algebraMap r) = algebraMap(log r).

Русский

Для реально числа r выполняется log(algebraMap r) = algebraMap(log r).

LaTeX

$$$\log(\operatorname{algebraMap}_{\mathbb{R} A}(r)) = \operatorname{algebraMap}_{\mathbb{R} A}(\log r)$$$

Lean4

@[simp, grind =]
theorem log_algebraMap {r : ℝ} : log (algebraMap ℝ A r) = algebraMap ℝ A (Real.log r) := by simp [log]

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

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

Разделы

Аффилиация

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