F : Type ?u.131282
α : Type u_1
β : Type ?u.131288
𝕜 : Type ?u.131291
E : Type ?u.131294
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t : Finset α
⊢ MulSalemSpencer ∅
F : Type ?u.131282
α : Type u_1
β : Type ?u.131288
𝕜 : Type ?u.131291
E : Type ?u.131294
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t : Finset α
⊢ MulSalemSpencer ↑∅
norm_cast
no goals
F : Type ?u.131282
α : Type u_1
β : Type ?u.131288
𝕜 : Type ?u.131291
E : Type ?u.131294
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t : Finset α
⊢ MulSalemSpencer ∅
exact mulSalemSpencer_empty