Properties of Equiv.Perm on Finite types

Let α be a Finite type.

• Nat.card_perm: cardinality of Equiv.Perm α.

• Equiv.Perm.isCyclic_of_card_le_two: if Nat.card α ≤ 2, then Equiv.Perm α is cyclic.

• Equiv.Perm.isCyclic_iff_card_le_two: Equiv.Perm α is cyclic iff Nat.card α ≤ 2.

• Equiv.Perm.isMulCommutative_iff_card_le_two: Equiv.Perm α is commutative iff Nat.card α ≤ 2.

theorem Nat.card_perm {α : Type u_1} [Finite α] : Nat.card (Equiv.Perm α) = (Nat.card α).factorial

theorem Equiv.Perm.isCyclic_of_card_le_two {α : Type u_1} [Finite α] (hα : Nat.card α ≤ 2) : IsCyclic (Perm α)

theorem Equiv.Perm.isMulCommutative_iff_card_le_two {α : Type u_1} [Finite α] : IsMulCommutative (Perm α) ↔ Nat.card α ≤ 2

theorem Equiv.Perm.isCyclic_iff_card_le_two {α : Type u_1} [Finite α] : IsCyclic (Perm α) ↔ Nat.card α ≤ 2