no goals
F : Type ?u.148022
α : Type u_1
β : Type ?u.148028
𝕜 : Type ?u.148031
E : Type ?u.148034
inst✝¹ : DecidableEq α
inst✝ : CancelCommMonoid α
s : Finset α
a : α
⊢ ↑mulRothNumber (map (mulRightEmbedding a) s) = ↑mulRothNumber s
rw [← mul_left_embedding_eq_mul_right_embedding, mulRothNumber_map_mul_left s a]