fst_exp — Mathlib

English

If x.fst ≠ 0, then the same polar decomposition holds with x = x.fst • exp 𝕜 (x.fst⁻¹ • 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

@[simp]
theorem fst_exp (x : tsze R M) : fst (exp 𝕜 x) = exp 𝕜 x.fst := by rw [exp_def, fst_add, fst_inl, fst_inr, add_zero]

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