def AlgebraInLean.Symmetric (n : ℕ) : Type

Equations

• AlgebraInLean.Symmetric n = (Fin n ≃ Fin n)

instance AlgebraInLean.instGroupSymmetric (n : ℕ) : AlgebraInLean.Group (AlgebraInLean.Symmetric n)

Equations

• AlgebraInLean.instGroupSymmetric n = AlgebraInLean.Group.mk Equiv.symm ⋯