Inv_divided_by_X_pow_order_rightInv

English

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

Русский

Для любого непустого f ∈ k⟦X⟧ произведение divXPowOrder f и Inv_divided_by_X_pow_order hf равно единице.

LaTeX

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

Lean4

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

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