# Zulip Chat Archive

## Stream: maths

### Topic: Adjacent Transpositions

#### Thomas Browning (Dec 25 2020 at 02:11):

Transpositions are easy: `is_swap`

What's the best way to talk about adjacent transpositions? (context: we want to prove that S_n is generated by adjacent transpositions, which I don't think is in mathlib yet).

One consideration is that you might want to talk about adjacent transpositions in S_N or S_Z (or maybe not?)

If you do, then one option would be to define an instance extending `linear_order`

stating that every element has a unique element directly below it and a unique element directly above it. Is this notion in mathlib anywere?

#### Thomas Browning (Dec 25 2020 at 02:13):

Or maybe in general an adjacent transposition is a swap between two elements with no element between them?

#### Kevin Buzzard (Dec 25 2020 at 02:35):

It's not true that every element has a unique element directly below it of course, I guess the theorem is that you have a unique element directly below you iff you're not bot, and you have a subsingleton of things directly below you in general

#### Eric Wieser (Dec 25 2020 at 08:25):

Adjacent swaps on `fin n`

are in #3770

#### Eric Wieser (Dec 25 2020 at 08:26):

And on `nat`

in #4739

#### Eric Wieser (Dec 25 2020 at 08:27):

But your point about wanting a typeclass is salient

Last updated: May 09 2021 at 09:11 UTC