Commit 2022-10-23 13:05 a2a19634
View on Github →chore(data/finset/pointwise): {a} • t = a • t (#17072)
Change singleton_smul so that it uses the • spelling on the RHS.
chore(data/finset/pointwise): {a} • t = a • t (#17072)
Change singleton_smul so that it uses the • spelling on the RHS.