comp_assoc

Stream: Is there code for X?

[Yaël Dillies]

Do we not have associativity of composition somewhere?

@[simp] lemma comp_assoc {α β γ δ : Type*} (h : γ → δ) (g : β → γ) (f : α → β) :
  (h ∘ g) ∘ f = h ∘ (g ∘ f) := rfl

[Vincent Beffara]

docs#function.comp.assoc ?

[Yaël Dillies]

The dots in those names get me confused every time.

[Jireh Loreaux]

I've taken to just omitting . and _ when searching. It has saved me lots of these sorts of headaches.

[Yaël Dillies]

My keyboard was a bit too fiery :grinning: