map_exp — Mathlib

English

Let ha be a nilpotent element of A and f be a structure-preserving map (e.g., an algebra homomorphism) between appropriate algebras. Then f(exp(a)) = exp(f(a)) for nilpotent a.

Русский

Пусть a ∈ A нильпотентен и есть отображение f, сохраняющее структуру алгебр. Тогда f(exp(a)) = exp(f(a)).

LaTeX

$$$f(\exp(a)) = \exp(f(a))$$$

Lean4

theorem map_exp {B F : Type*} [Ring B] [FunLike F A B] [RingHomClass F A B] [Module ℚ B] {a : A} (ha : IsNilpotent a)
    (f : F) : f (exp a) = exp (f a) := by
  obtain ⟨k, hk⟩ := ha
  have hk' : (f a) ^ k = 0 := by simp [← map_pow, hk]
  simp [exp_eq_sum hk, exp_eq_sum hk', map_rat_smul]

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