Theorem: WfDvdMonoid.multiplicity_eq_top_iff (FltRegular/CaseII/AuxLemmas.lean)

State before:
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✝¹ : WfDvdMonoid M
inst✝ : DecidableRel fun a b => a ∣ b
x y : M
⊢ multiplicity x y = ⊤ ↔ IsUnit x ∨ y = 0
Tactic:
rw [multiplicity.eq_top_iff_not_finite, WfDvdMonoid.multiplicity_finite_iff, or_iff_not_and_not]
State after:
no goals