Skip to content

Commit 95a4c73

Browse files
committed
chore(GroupTheory/QuotientGroup/Basic): remove transitive import (#39604)
1 parent 9eb40b4 commit 95a4c73

1 file changed

Lines changed: 0 additions & 1 deletion

File tree

Mathlib/GroupTheory/QuotientGroup/Basic.lean

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,6 @@ module
88

99
public import Mathlib.Algebra.Group.Subgroup.Pointwise
1010
public import Mathlib.Data.Int.Cast.Lemmas
11-
public import Mathlib.GroupTheory.Congruence.Hom
1211
public import Mathlib.GroupTheory.Coset.Basic
1312
public import Mathlib.GroupTheory.QuotientGroup.Defs
1413
public import Mathlib.Algebra.BigOperators.Group.Finset.Defs

0 commit comments

Comments
 (0)