diff options
| author | Hannes Schulze <contact@haschu.me> | 2026-04-15 16:18:07 +0200 |
|---|---|---|
| committer | Hannes Schulze <contact@haschu.me> | 2026-04-15 16:18:47 +0200 |
| commit | 2e5f7e22761bd30857bbe067862a8b256805ecd8 (patch) | |
| tree | c40311802db91f935bc0a1ea00fbc98b5ae4c141 /Nominal/Instances/Basic.lean | |
| parent | 37f7c86a7591da1233cdf1d293bf851f43c65ba1 (diff) | |
fs constructions
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 |