swap_mul_swap_same_mem_closure_three_cycles

English

The product of two swaps lies in the closure of the set of three-cycles.

Русский

Произведение двух транспозиций принадлежит замыканию множества трёхциклов.

LaTeX

$$swap a b * swap a c ∈ closure {σ : Perm α | IsThreeCycle σ}$$

Lean4

theorem swap_mul_swap_same_mem_closure_three_cycles {a b c : α} (ab : a ≠ b) (ac : a ≠ c) :
    swap a b * swap a c ∈ closure {σ : Perm α | IsThreeCycle σ} :=
  by
  by_cases bc : b = c
  · subst bc
    simp [one_mem]
  exact subset_closure (isThreeCycle_swap_mul_swap_same ab ac bc)

Похожие утверждения