diff --git a/Mathlib/Data/PNat/Factors.lean b/Mathlib/Data/PNat/Factors.lean index 2e0a02f217bd62..41551af1fb2f77 100644 --- a/Mathlib/Data/PNat/Factors.lean +++ b/Mathlib/Data/PNat/Factors.lean @@ -30,9 +30,8 @@ gives an equivalence between this set and ℕ+, as we will formalize below. -/ def PrimeMultiset := Multiset Nat.Primes -deriving Inhabited, AddCommMonoid, DistribLattice, - SemilatticeSup, Sub, - IsOrderedCancelAddMonoid, CanonicallyOrderedAdd, OrderBot, OrderedSub +deriving Inhabited, AddCommMonoid, SemilatticeSup, DistribLattice, + Sub, IsOrderedCancelAddMonoid, CanonicallyOrderedAdd, OrderBot, OrderedSub namespace PrimeMultiset