eq_mul_inv_iff_mul_eq — Mathlib

English

Let φ1, φ2, φ3 be formal power series over a field k with constantCoeff φ3 ≠ 0. Then φ1 equals φ2 times the inverse of φ3 if and only if φ1 times φ3 equals φ2.

Русский

Пусть φ1, φ2, φ3 — степенные ряды над полем k и c0(φ3) ≠ 0. Тогда φ1 = φ2 φ3^{-1} тогда и только тогда, когда φ1 φ3 = φ2.

LaTeX

$$$ c_0(\phi_3) \neq 0 \Rightarrow (\phi_1 = \phi_2 \phi_3^{-1} \iff \phi_1 \phi_3 = \phi_2). $$$

Lean4

theorem eq_mul_inv_iff_mul_eq {φ₁ φ₂ φ₃ : k⟦X⟧} (h : constantCoeff φ₃ ≠ 0) : φ₁ = φ₂ * φ₃⁻¹ ↔ φ₁ * φ₃ = φ₂ :=
  MvPowerSeries.eq_mul_inv_iff_mul_eq h

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