associativity of `∘L`

Stream: mathlib4

[Jireh Loreaux]

The infix notation ∘L for continuous linear maps is declared to be right associative, which conflicts with the fact that * is declared left associative.

Consequently, f₁ ∘L f₂ ∘L f₃ = f₁ * f₂ * f₃ is not defeq, which is super annoying. Is there a reason we've caused ourselves this headache?

[Aaron Liu]

That looks like it should be defeq

[Jireh Loreaux]

Oh nevermind, I'm an idiot

[Jireh Loreaux]

I was having a different problem and misdiagnosed.

[Aaron Liu]

I imagine the reason is because comp is also declared to be right associative.