How to name this lemma?

Stream: lean4

[François G. Dorais]

What would be a good name for this lemma?

import Std
open Ordering

theorem name_me {x y : Ordering} : swap x = y ↔ swap y = x := sorry

[Kyle Miller]

I think this would usually be phrased as swap x = y ↔ x = swap y and be named something like swap_eq_iff

[Kyle Miller]

That's shorting the longer name swap_eq_iff_eq_swap. An analogue in mathlib is docs#inv_eq_iff_eq_inv

[Kyle Miller]

Then there's also swap x = swap y ↔ x = y, which would be named swap_inj

[François G. Dorais]

Ah! Yes, it's like an adjunction. I like this!