English
Let φ1, φ2, φ3 be multivariate power series with coefficients in a field k, indexed by σ. If the constant coefficient of φ3 is nonzero, then φ1 equals φ2 times the inverse of φ3 if and only if φ1 times φ3 equals φ2.
Русский
Пусть φ1, φ2, φ3 — многочлены по многим переменным над полем k, индексируемые σ. Если константный коэффициент φ3 не равен нулю, то φ1 = φ2 φ3⁻¹ тогда и только тогда, когда φ1 φ3 = φ2.
LaTeX
$$$\forall \phi_1, \phi_2, \phi_3 \in \mathrm{MvPowerSeries}(\sigma,k),\; \operatorname{constantCoeff}(\phi_3) \neq 0 \Rightarrow (\phi_1 = \phi_2 \phi_3^{-1} \iff \phi_1 \phi_3 = \phi_2)$$$
Lean4
protected theorem eq_mul_inv_iff_mul_eq {φ₁ φ₂ φ₃ : MvPowerSeries σ k} (h : constantCoeff φ₃ ≠ 0) :
φ₁ = φ₂ * φ₃⁻¹ ↔ φ₁ * φ₃ = φ₂ :=
⟨fun k => by simp [k, mul_assoc, MvPowerSeries.inv_mul_cancel _ h], fun k => by
simp [← k, mul_assoc, MvPowerSeries.mul_inv_cancel _ h]⟩
