R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
φ ψ : PowerSeries R
⊢ multiplicity X (φ * ψ) = multiplicity X φ + multiplicity X ψ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
φ ψ : PowerSeries R
⊢ order (φ * ψ) = order φ + order ψ
simp_rw [order_eq_multiplicity_X]
no goals
R : Type u_1
inst✝¹ : CommRing R
inst✝ : IsDomain R
φ ψ : PowerSeries R
⊢ multiplicity X (φ * ψ) = multiplicity X φ + multiplicity X ψ
exact multiplicity.mul X_prime