English
For a nonzero polynomial P, the number of occurrences of X in the normalization of P as a power series equals the number of occurrences of X in the normalization of P as a polynomial.
Русский
Для ненулевого многочлена P число встреч X в нормализованных разложениях P как степенного ряда равно числу встреч X в нормализованном факторизационном представлении P как многочлена.
LaTeX
$$Multiset.count(\ PowerSeries.X)(normalizedFactors (P : k⟦X⟧)) = Multiset.count(Polynomial.X)(normalizedFactors P)$$
Lean4
theorem normalized_count_X_eq_of_coe {P : k[X]} (hP : P ≠ 0) :
Multiset.count PowerSeries.X (normalizedFactors (P : k⟦X⟧)) = Multiset.count Polynomial.X (normalizedFactors P) :=
by
apply eq_of_forall_le_iff
simp only [← Nat.cast_le (α := ℕ∞)]
rw [X_eq_normalize, PowerSeries.X_eq_normalizeX, ← emultiplicity_eq_count_normalizedFactors irreducible_X hP, ←
emultiplicity_eq_count_normalizedFactors X_irreducible] <;>
simp only [← pow_dvd_iff_le_emultiplicity, Polynomial.X_pow_dvd_iff, PowerSeries.X_pow_dvd_iff,
Polynomial.coeff_coe P, implies_true, ne_eq, coe_eq_zero_iff, hP, not_false_eq_true]
