exp_unop — Mathlib

English

Exponential commutes with the unop (the inverse of op): exp(unop x) = unop(exp x).

Русский

Экспонента commuting с обратной операцией: exp(unop x) = unop(exp x).

LaTeX

$$$\\exp 𝕂 (\\operatorname{MulOpposite.unop} x) = \\operatorname{MulOpposite.unop} (\\exp 𝕂 x).$$$

Lean4

@[simp]
theorem exp_unop [T2Space 𝔸] (x : 𝔸ᵐᵒᵖ) : exp 𝕂 (MulOpposite.unop x) = MulOpposite.unop (exp 𝕂 x) := by
  simp_rw [exp, expSeries_sum_eq, ← MulOpposite.unop_pow, ← MulOpposite.unop_smul, tsum_unop]

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