Inv_divided_by_X_pow_order_leftInv

English

For any nonzero f ∈ k⟦X⟧, Inv_divided_by_X_pow_order hf multiplied by divXPowOrder f equals 1.

Русский

Для любого непустого f ∈ k⟦X⟧ Inv_divided_by_X_pow_order hf умноженное на divXPowOrder f даёт 1.

LaTeX

$$$ Inv\_divided\_by\_X\_pow\_order(hf) \cdot divXPowOrder(f) = 1. $$$

Lean4

@[simp]
theorem Inv_divided_by_X_pow_order_leftInv {f : k⟦X⟧} (hf : f ≠ 0) :
    Inv_divided_by_X_pow_order hf * divXPowOrder f = 1 :=
  by
  rw [mul_comm]
  exact mul_invOfUnit (divXPowOrder f) (firstUnitCoeff hf) rfl

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