We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent e1b3f71 commit e44cdf8Copy full SHA for e44cdf8
Mathlib/RingTheory/Coalgebra/CoassocSimps.lean
@@ -4,9 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
4
Authors: Andrew Yang, Yaël Dillies
5
-/
6
module
7
+
8
public import Mathlib.LinearAlgebra.TensorProduct.Tower
9
public import Mathlib.RingTheory.Coalgebra.Basic
10
11
+import Mathlib.Tactic.Attr.Register
12
13
/-!
14
# Tactic to reassociate comultiplication in a coalgebra
15
0 commit comments