F : Type ?u.135470
α : Type u_1
β : Type ?u.135476
𝕜 : Type ?u.135479
E : Type ?u.135482
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t : Finset α
n : ℕ
a : α
⊢ MulSalemSpencer ↑{a}
F : Type ?u.135470
α : Type u_1
β : Type ?u.135476
𝕜 : Type ?u.135479
E : Type ?u.135482
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t : Finset α
n : ℕ
a : α
⊢ ↑mulRothNumber {a} = 1
refine' MulSalemSpencer.roth_number_eq _
F : Type ?u.135470
α : Type u_1
β : Type ?u.135476
𝕜 : Type ?u.135479
E : Type ?u.135482
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t : Finset α
n : ℕ
a : α
⊢ MulSalemSpencer {a}
F : Type ?u.135470
α : Type u_1
β : Type ?u.135476
𝕜 : Type ?u.135479
E : Type ?u.135482
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t : Finset α
n : ℕ
a : α
⊢ MulSalemSpencer ↑{a}
rw [coe_singleton]
no goals
F : Type ?u.135470
α : Type u_1
β : Type ?u.135476
𝕜 : Type ?u.135479
E : Type ?u.135482
inst✝³ : DecidableEq α
inst✝² : Monoid α
inst✝¹ : DecidableEq β
inst✝ : Monoid β
s t : Finset α
n : ℕ
a : α
⊢ MulSalemSpencer {a}
exact mulSalemSpencer_singleton a