exp_coe — Mathlib

English

The exponential of a real scalar embedded as a scalar quaternion equals the real embedding of the real exponential: exp ℝ (r : ℍ[ℝ]) = ↑(exp ℝ r).

Русский

Экспонента вещественного числа, вложенного в ротационный квадрат, равна реальному вложению экспоненты: exp ℝ (r : ℍ[ℝ]) = ↑(exp ℝ r).

LaTeX

$$$\exp_{\mathbb{R}}(r) = \uparrow\big(\exp_{\mathbb{R}}(r)\big).$$$

Lean4

@[simp, norm_cast]
theorem exp_coe (r : ℝ) : exp ℝ (r : ℍ[ℝ]) = ↑(exp ℝ r) :=
  (map_exp ℝ (algebraMap ℝ ℍ[ℝ]) (continuous_algebraMap _ _) _).symm

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