exp_def — Mathlib

English

If the left component of x is invertible, then x is x.fst times the exponential of x.fst⁻¹ times inr x.snd.

Русский

Если x.fst обратимо, то x = x.fst • exp 𝕜 (⅟ x.fst • inr x.snd).

LaTeX

$$$\\text{If } x.fst \\text{ is invertible, then } x = x.fst \\cdot \\exp_{𝕜}(x.fst^{-1} \\cdot \\mathrm{inr}(x.snd))$$$

Lean4

theorem exp_def (x : tsze R M) : exp 𝕜 x = inl (exp 𝕜 x.fst) + inr (exp 𝕜 x.fst • x.snd) :=
  exp_def_of_smul_comm 𝕜 x (op_smul_eq_smul _ _)

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