eq_smul_exp_of_invertible — Mathlib

English

Polar form: for invertible x.fst, x = x.fst • exp 𝕜 (⅟ x.fst • inr x.snd).

Русский

Полярная форма: если x.fst обратимо, то x = x.fst • exp 𝕜 (⅟ x.fst • inr x.snd).

LaTeX

$$$x = x.fst \\cdot \\exp_{𝕜}(x.fst^{-1} \\cdot inr(x.snd))$$$

Lean4

/-- Polar form of trivial-square-zero extension. -/
theorem eq_smul_exp_of_invertible (x : tsze R M) [Invertible x.fst] : x = x.fst • exp 𝕜 (⅟x.fst • inr x.snd) := by
  rw [← inr_smul, exp_inr, smul_add, ← inl_one, ← inl_smul, ← inr_smul, smul_eq_mul, mul_one, smul_smul, mul_invOf_self,
    one_smul, inl_fst_add_inr_snd_eq]

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