eq_smul_exp_of_ne_zero — Mathlib

English

If x.fst ≠ 0, then x equals the scalar x.fst times the exponential with ⅟ x.fst multiplying inr x.snd.

Русский

Если x.fst ≠ 0, то x = x.fst • exp 𝕜 (⅟ x.fst • inr x.snd).

LaTeX

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

Lean4

/-- More convenient version of `TrivSqZeroExt.eq_smul_exp_of_invertible` for when `R` is a
field. -/
theorem eq_smul_exp_of_ne_zero (x : tsze R M) (hx : x.fst ≠ 0) : x = x.fst • exp 𝕜 (x.fst⁻¹ • inr x.snd) :=
  letI : Invertible x.fst := invertibleOfNonzero hx
  eq_smul_exp_of_invertible _ _

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