instance NominalSets.Perm.instPermAction {𝔸 : Type u_1} : PermAction 𝔸 (Perm 𝔸)

Equations

• NominalSets.Perm.instPermAction = { perm := fun (π π' : NominalSets.Perm 𝔸) => π * π' * π⁻¹, perm_one := ⋯, perm_mul := ⋯ }

theorem NominalSets.Perm.perm_def {𝔸 : Type u_1} (π π' : Perm 𝔸) : perm π π' = π * π' * π⁻¹