diff options
Diffstat (limited to 'Nominal/Instances/Basic.lean')
| -rw-r--r-- | Nominal/Instances/Basic.lean | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Nominal/Instances/Basic.lean b/Nominal/Instances/Basic.lean index 7a88eeb..a7aec47 100644 --- a/Nominal/Instances/Basic.lean +++ b/Nominal/Instances/Basic.lean @@ -398,7 +398,7 @@ instance : PermSet 𝔸 S where exact MulAction.one_smul x.val mul_smul π τ x := by apply Subtype.ext - exact SemigroupAction.mul_smul π τ x.val + exact mul_smul π τ x.val @[simp] lemma smul_val (π : FPerm 𝔸) (x : S) : (π • x).val = π • x.val := rfl |