mul_mem_closure_three_cycles — Mathlib

English

If σ and τ are swaps, then στ lies in the closure of the set of three-cycles.

Русский

Если σ и τ — транспозиции, то их произведение στ лежит в замыкании множества трёхциклов.

LaTeX

$$σ IsSwap ∧ τ IsSwap ⇒ σ τ ∈ closure {ρ : Perm α | IsThreeCycle ρ}$$

Lean4

theorem mul_mem_closure_three_cycles {σ τ : Perm α} (hσ : IsSwap σ) (hτ : IsSwap τ) :
    σ * τ ∈ closure {σ : Perm α | IsThreeCycle σ} :=
  by
  obtain ⟨a, b, ab, rfl⟩ := hσ
  obtain ⟨c, d, cd, rfl⟩ := hτ
  by_cases ac : a = c
  · subst ac
    exact swap_mul_swap_same_mem_closure_three_cycles ab cd
  have h' : swap a b * swap c d = swap a b * swap a c * (swap c a * swap c d) := by simp [swap_comm c a, mul_assoc]
  rw [h']
  exact
    mul_mem (swap_mul_swap_same_mem_closure_three_cycles ab ac)
      (swap_mul_swap_same_mem_closure_three_cycles (Ne.symm ac) cd)

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