trunc_cycle_factors

Stream: Berkeley Lean Seminar

[Yakov Pechersky]

Would it make sense to refactor this to just output the finset of perm? Since they are disjoint, we know that the whole list is nodup. And since they are disjoint, we know that the order of prod doesn't matter, we know we can forget the order of the list.

[Thomas Browning]

Does it make it harder to state that the product of the cycle factors is the original permutation?

[Yakov Pechersky]

Do we even have that statement anywhere?

[Yakov Pechersky]

I guess it is part of the subtype