rw [multiplicity.mul hp]
K : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p✝} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
b : M
hb : ¬b = 0
a q : M
a✝ : a ≠ 0
hq : Prime q
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b) → a ∣ b
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p b
ha : ¬q = 0 ∧ ¬a = 0
p : M
hp : Prime p
⊢ multiplicity p a ≤ multiplicity p (q * a)
K : Type u_1
p✝ : ℕ+
hpri : Fact p✝.Prime
inst✝⁵ : Field K
inst✝⁴ : CharZero K
inst✝³ : IsCyclotomicExtension {p✝} ℚ K
ζ : K
hζ : IsPrimitiveRoot ζ ↑p✝
M : Type u_2
inst✝² : CancelCommMonoidWithZero M
inst✝¹ : DecidableRel fun a b => a ∣ b
inst✝ : UniqueFactorizationMonoid M
b : M
hb : ¬b = 0
a q : M
a✝ : a ≠ 0
hq : Prime q
IH : a ≠ 0 → (∀ (p : M), Prime p → multiplicity p a ≤ multiplicity p b) → a ∣ b
H : ∀ (p : M), Prime p → multiplicity p (q * a) ≤ multiplicity p b
ha : ¬q = 0 ∧ ¬a = 0
p : M
hp : Prime p
⊢ multiplicity p a ≤ multiplicity p q + multiplicity p a