exp_op — Mathlib

English

Exponential is compatible with the opposite operation: applying exp to the opposite of x equals the opposite of exp(x).

Русский

Экспонента совместима с операцией противоположного: exp(op x) = op(exp x).

LaTeX

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

Lean4

@[simp]
theorem exp_op [T2Space 𝔸] (x : 𝔸) : exp 𝕂 (MulOpposite.op x) = MulOpposite.op (exp 𝕂 x) := by
  simp_rw [exp, expSeries_sum_eq, ← MulOpposite.op_pow, ← MulOpposite.op_smul, tsum_op]

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