Products of real exponentials at half arguments

Mathlib records Real.exp_half : exp (x / 2) = √(exp x), but not the product forms of the half-argument identities that arise when computing with the diagonal matrix !![exp (r / 2), 0; 0, exp (-(r / 2))]. This file supplies them.

Main declarations

• Real.exp_half_mul_exp_half, Real.exp_neg_half_mul_exp_neg_half, Real.exp_half_mul_exp_neg_half: the products of exp (± r / 2).

theorem Real.exp_half_mul_exp_half (r : ℝ) : exp (r / 2) * exp (r / 2) = exp r

exp (r / 2) * exp (r / 2) = exp r.

theorem Real.exp_neg_half_mul_exp_neg_half (r : ℝ) : exp (-(r / 2)) * exp (-(r / 2)) = exp (-r)

exp (-(r / 2)) * exp (-(r / 2)) = exp (-r).

theorem Real.exp_half_mul_exp_neg_half (r : ℝ) : exp (r / 2) * exp (-(r / 2)) = 1

exp (r / 2) * exp (-(r / 2)) = 1.