cycleType_ofSubtype — Mathlib

English

The cycle-type of the permutation on a subtype corresponds to the original cycle-type.

Русский

Тип цикла перестановки на подтипе равен исходному cycleType.

LaTeX

$$$$\mathrm{cycleType}(\mathrm{ofSubtype}(g)) = \mathrm{cycleType}(g).$$$$

Lean4

theorem cycleType_ofSubtype {p : α → Prop} [DecidablePred p] {g : Perm (Subtype p)} :
    cycleType (ofSubtype g) = cycleType g :=
  cycleType_extendDomain (Equiv.refl (Subtype p))

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