Skip to content

Commit 3cc311f

Browse files
committed
chore(RingTheory/Bialgebra): drop unused opens in Primitive
1 parent bba17f3 commit 3cc311f

1 file changed

Lines changed: 1 addition & 1 deletion

File tree

Mathlib/RingTheory/Bialgebra/Primitive.lean

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ This file defines primitive elements in a bialgebra, i.e. elements `a` such that
2727

2828
public section
2929

30-
open Bialgebra Coalgebra TensorProduct Algebra.TensorProduct
30+
open Coalgebra TensorProduct
3131

3232
variable {F R A B : Type*}
3333

0 commit comments

Comments
 (0)