cycleFactorsFinset_injective — Mathlib

English

The map f ↦ cycleFactorsFinset f is injective; cycle factors determine the permutation.

Русский

Отображение f ↦ cycleFactorsFinset f инъективно; фрагменты цикла полностью определяют перестановку.

LaTeX

$$Function.Injective (cycleFactorsFinset : Perm α → Finset (Perm α))$$

Lean4

/-- Two permutations `f g : Perm α` have the same cycle factors iff they are the same. -/
theorem cycleFactorsFinset_injective : Function.Injective (@cycleFactorsFinset α _ _) :=
  by
  intro f g h
  rw [← cycleFactorsFinset_noncommProd f]
  simpa [h] using cycleFactorsFinset_noncommProd g

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