exp_pow_eq_rescale_exp — Mathlib

English

The identity exp_mul_exp_add expresses that e^{aX} e^{bX} = e^{(a+b)X} and compatible rescalings commute with exp.

Русский

Правило умножения экспоненты: e^{aX} e^{bX} = e^{(a+b)X} и сопряжённость с масштабированием сохраняется.

LaTeX

$$$$ \exp\_mul\_exp\_eq\_exp\_add $$$$

Lean4

/-- Shows that $(e^{X})^k = e^{kX}$. -/
theorem exp_pow_eq_rescale_exp [Algebra ℚ A] (k : ℕ) : exp A ^ k = rescale (k : A) (exp A) := by
  induction k with
  | zero =>
    simp only [rescale_zero, constantCoeff_exp, Function.comp_apply, map_one, cast_zero, pow_zero (exp A), coe_comp]
  | succ k h =>
    simpa only [succ_eq_add_one, cast_add, ← exp_mul_exp_eq_exp_add (k : A), ← h, cast_one, id_apply, rescale_one] using
      pow_succ (exp A) k

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