From 3fc2bc57aaa6fc31b94aa72e5af88cd5f45f5e2a Mon Sep 17 00:00:00 2001 From: Antoine Chambert-Loir Date: Thu, 4 Jul 2024 00:39:44 +0200 Subject: [PATCH] fix import --- Mathlib/GroupTheory/GroupAction/Blocks.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Mathlib/GroupTheory/GroupAction/Blocks.lean b/Mathlib/GroupTheory/GroupAction/Blocks.lean index 7777028af26f0..2fdfa311b9f93 100644 --- a/Mathlib/GroupTheory/GroupAction/Blocks.lean +++ b/Mathlib/GroupTheory/GroupAction/Blocks.lean @@ -11,7 +11,7 @@ import Mathlib.Data.Setoid.Partition import Mathlib.GroupTheory.GroupAction.Basic import Mathlib.GroupTheory.GroupAction.Pointwise import Mathlib.GroupTheory.GroupAction.SubMulAction --- import Mathlib.GroupTheory.Subgroup.Actions +import Mathlib.Algebra.Group.Subgroup.Actions /-! # Blocks