We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent 4cd2f5f commit b10e530Copy full SHA for b10e530
1 file changed
Mathlib/LinearAlgebra/TensorAlgebra/Hopf.lean
@@ -3,7 +3,7 @@ Copyright (c) 2025 Nikolas Tapia. All rights reserved.
3
Released under Apache 2.0 license as described in the file LICENSE.
4
Authors: Nikolas Tapia
5
-/
6
-module
+module
7
8
public import Mathlib.LinearAlgebra.TensorAlgebra.Basic
9
public import Mathlib.RingTheory.Coalgebra.Convolution
@@ -26,7 +26,7 @@ open LinearMap TensorProduct
26
27
variable (R : Type*) [CommRing R] {M : Type*} [AddCommMonoid M] [Module R M]
28
29
-local notation "T["M"]" => TensorAlgebra R M
+local notation "T[" M "]" => TensorAlgebra R M
30
31
/-- Linear map inducing the comultiplication in `TensorAlgebra R M`. -/
32
def comul' : M →ₗ[R] T[M] ⊗[R] T[M] :=
0 commit comments