exp_neg_mul_exp_self — Mathlib

English

Let A be a ring (with a rational-scale module structure) and a ∈ A be nilpotent. Then the exponential satisfies exp(−a) · exp(a) = 1, i.e., exp(a) is invertible with inverse exp(−a).

Русский

Пусть A — кольцо с дополнительной структурой модуля над полем ℚ, и a ∈ A нильпотентен. Тогда exp(−a) · exp(a) = 1, то есть exp(a) обратимо и его обратное равно exp(−a).

LaTeX

$$$\exp(-a) \cdot \exp(a) = 1$$$

Lean4

theorem exp_neg_mul_exp_self {a : A} (h : IsNilpotent a) : exp (-a) * exp a = 1 := by
  simp [← exp_add_of_commute (Commute.neg_left rfl) h.neg h]

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