exp_inl — Mathlib

English

The exponential on the left component commutes with the left injection: exp𝕜(inl x) = inl(exp𝕜 x).

Русский

Экспонента слева отлагаемой компоненты сохраняется: exp𝕜(inl x) = inl(exp 𝕜 x).

LaTeX

$$$\\operatorname{exp}_{𝕜}(\\mathrm{inl}\\, x) = \\mathrm{inl}(\\operatorname{exp}_{𝕜}(x))$$$

Lean4

@[simp]
theorem exp_inl (x : R) : exp 𝕜 (inl x : tsze R M) = inl (exp 𝕜 x) :=
  by
  rw [exp_def_of_smul_comm, snd_inl, fst_inl, smul_zero, inr_zero, add_zero]
  rw [snd_inl, fst_inl, smul_zero, smul_zero]

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