constantCoeff_divXPowOrder_eq_zero_iff

English

The equality constantCoeff(divXPowOrder f) = 0 holds if and only if f = 0.

Русский

Равенство постоянного коэффициента divXPowOrder f = 0 эквивалентно f = 0.

LaTeX

$$$\operatorname{constantCoeff}(\operatorname{divXPowOrder} f) = 0 \iff f = 0$$$

Lean4

theorem constantCoeff_divXPowOrder_eq_zero_iff {f : R⟦X⟧} : constantCoeff (divXPowOrder f) = 0 ↔ f = 0 :=
  by
  by_cases h : f = 0
  · simp [h]
  · simp [constantCoeff_divXPowOrder, coeff_order h, h]

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