Skip to content

Commit 8097429

Browse files
committed
chore: fix implicit-reducible diamond in PrimeMultiset (#38303)
The following lemma fails in master, works in the PR: ```lean example : (instDistribLatticePrimeMultiset.toSemilatticeSup : SemilatticeSup PrimeMultiset) = instSemilatticeSupPrimeMultiset := by with_reducible_and_instances rfl ``` Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
1 parent fad2aee commit 8097429

1 file changed

Lines changed: 2 additions & 3 deletions

File tree

Mathlib/Data/PNat/Factors.lean

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -30,9 +30,8 @@ gives an equivalence between this set and ℕ+, as we will formalize
3030
below. -/
3131
def PrimeMultiset :=
3232
Multiset Nat.Primes
33-
deriving Inhabited, AddCommMonoid, DistribLattice,
34-
SemilatticeSup, Sub,
35-
IsOrderedCancelAddMonoid, CanonicallyOrderedAdd, OrderBot, OrderedSub
33+
deriving Inhabited, AddCommMonoid, SemilatticeSup, DistribLattice,
34+
Sub, IsOrderedCancelAddMonoid, CanonicallyOrderedAdd, OrderBot, OrderedSub
3635

3736
namespace PrimeMultiset
3837

0 commit comments

Comments
 (0)