sign): Order of product of disjoint permutations (#6998)

Commit

5 years ago

feat(group_theory/perm/sign): Order of product of disjoint permutations (#6998) The order of the product of disjoint permutations is the lcm of the orders.

Author

tb65536

Parents

fe16235f

mathlib3 030a7047 - feat(group_theory/perm/sign): Order of product of disjoint permutations (#6998)

mathlib3
030a7047 - feat(group_theory/perm/sign): Order of product of disjoint permutations (#6998)