English
The product of two transpositions sharing a point is a three-cycle: (a b)(a c) is a 3-cycle when a,b,c are distinct.
Русский
Произведение двух транспозиций с общей точкой образует трёхцикл: (a b)(a c) — трёхцикл, если a,b,c различны.
LaTeX
$$$\text{IsThreeCycle}( (a\ b) (a\ c) )$ when a,b,c distinct$$
Lean4
theorem isThreeCycle_swap_mul_swap_same {a b c : α} (ab : a ≠ b) (ac : a ≠ c) (bc : b ≠ c) :
IsThreeCycle (swap a b * swap a c) :=
by
suffices h : support (swap a b * swap a c) = { a, b, c }
by
rw [← card_support_eq_three_iff, h]
simp [ab, ac, bc]
apply le_antisymm ((support_mul_le _ _).trans fun x => _) fun x hx => ?_
· simp [ab, ac]
· simp only [Finset.mem_insert, Finset.mem_singleton] at hx
rw [mem_support]
simp only [Perm.coe_mul, Function.comp_apply, Ne]
obtain rfl | rfl | rfl := hx
· rw [swap_apply_left, swap_apply_of_ne_of_ne ac.symm bc.symm]
exact ac.symm
· rw [swap_apply_of_ne_of_ne ab.symm bc, swap_apply_right]
exact ab
· rw [swap_apply_right, swap_apply_left]
exact bc
