exp_inr — Mathlib

English

The first component of the exponential equals the exponential of the first component.

Русский

Первая компонента экспоненты равна экспоненте от первой компоненты.

LaTeX

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

Lean4

@[simp]
theorem exp_inr (m : M) : exp 𝕜 (inr m : tsze R M) = 1 + inr m :=
  by
  rw [exp_def_of_smul_comm, snd_inr, fst_inr, exp_zero, one_smul, inl_one]
  rw [snd_inr, fst_inr, MulOpposite.op_zero, zero_smul, zero_smul]

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