Function.comp.assoc

Stream: mathlib4

[Ruben Van de Velde]

I completely failed to find docs#Function.comp.assoc just now, because I expected it to be called comp_assoc with an underscore. Should we rename it?

[Ruben Van de Velde]

#17098

[Floris van Doorn]

Should we also rename docs#Function.comp.left_id and docs#Function.comp.right_id ?

[Floris van Doorn]

Oh never mind, they are already deprecated.