equiv.symm_trans_rev

Stream: Is there code for X?

[Chris Hughes]

Do we actually not have this? I couldn't find it and nor could library_search

example (α β γ : Type) (e₁ : α ≃ β) (e₂ : β ≃ γ) :
  (e₁.trans e₂).symm = e₂.symm.trans e₁.symm :=

[Eric Wieser]

Do we have it for other equivs?

[Eric Wieser]

docs#ring_equiv.symm_trans, docs#linear_equiv.symm_trans maybe?