Inv_divided_by_X_pow_order — Mathlib

English

For any nonzero f ∈ k⟦X⟧, the inverse of divXPowOrder f is Inv_divided_by_X_pow_order hf, making divXPowOrder f a unit with that inverse.

Русский

Для любого непустого f ∈ k⟦X⟧ обратное к divXPowOrder f задаётся Inv_divided_by_X_pow_order hf, что делает divXPowOrder f единицей с таким обратным.

LaTeX

$$$ divXPowOrder(f)^{-1} = Inv\_divided\_by\_X\_pow\_order\_hf. $$$

Lean4

/-- `Inv_divided_by_X_pow_order` is the inverse of the element obtained by diving a non-zero power
series by the largest power of `X` dividing it. Useful to create a term of type `Units`, done in
`Unit_divided_by_X_pow_order` -/
def Inv_divided_by_X_pow_order {f : k⟦X⟧} (hf : f ≠ 0) : k⟦X⟧ :=
  invOfUnit (divXPowOrder f) (firstUnitCoeff hf)

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