proposition: Theorem phi_zq_eq_z_sub_c₁_psi : ∀ f L c₁ r Ψ, r = root_multiplicity acf c₁ (Φq f L) → Ψ = quotient_phi_x_sub_c_pow_r (Φq f L) c₁ r → (Φq f L = POL [(- c₁)%K; 1%K … []] ^ r * Ψ)%pol.
proof: Proof. intros f L c r Ψ Hr HΨ. subst Ψ; simpl. eapply list_root_mul_power_quotient. symmetry; eassumption. Qed.
imports: Utf8 QArith NPeano ArithRing Misc Field2 ConvexHull Newton Fsummation Fpolynomial Puiseux_base Puiseux_series CharactPolyn