No instance of `Mul` for the type of endofunctions

Stream: mathlib4

[Sina Hazratpour 𓃵]

I was hoping to use IsIdempotentElem f to say f ∘ f = f, but apparently there is no instance of Mul (A → A) in mathlib.

variable {A : Type*} {f : A -> A}
#check IsIdempotentElem
#check IsIdempotentElem f
#synth Mul (A → A)

Would there be a problem adding the following instance to mathlib?

instance mul {A : Type*} : Mul (A → A) := ⟨Function.comp⟩

In my case I can also just use f ∘ f = f instead but was wondering if there are reasons why adding such instance might not be a good idea?

[Kevin Buzzard]

I suspect that if A has a Mul then X -> A has a Mul defined pointwise, and so yes I should think that your suggestion might create problems.

[Sina Hazratpour 𓃵]

Thanks, that makes sense! Indeed, the instance you refer to is, I believe, Pi.instMul. In Lean 3 sometimes we used to provide multiple instances with different instance priorities -- not sure if we still do this in Lean 4, and even if that is the case, I am not sure if this case is worth the trouble? That's why I asked just to get a better sense of multiple instance issues.

[Eric Wieser]

If you want multiplication as composition, you want docs#Function.End

[Sina Hazratpour 𓃵]

Eric Wieser said:

If you want multiplication as composition, you want docs#Function.End

Thanks, that helps!