Pointwise set division

Stream: Is there code for X?

[Yaël Dillies]

We have docs#set.has_mul, docs#set.has_inv, docs#set.has_add and docs#set.has_neg. Should I define set.has_div and set.has_sub in the obvious way?

[Eric Wieser]

Do we also have docs#set.add_comm_monoid?

[Eric Wieser]

Oh no, that's a smul diamond vs with docs#set.has_scalar_set ... 2 • {1, 2} is either {2, 4} or {2, 3, 4} depending on which instance you find

[Yaël Dillies]

I must say that pointwise smul is the one I would expect here. Can we somehow override repeated addition?

[Yaël Dillies]

A simple way would be to turn docs#set.has_scalar_set in a definition set.smul : set α → set β → set β.

[Kevin Buzzard]

Whoever had the crazy idea that 2 • X = X + X? :laughing: