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 f17a877 commit b788da7Copy full SHA for b788da7
1 file changed
Mathlib/RingTheory/HopfAlgebra/Generators.lean
@@ -22,9 +22,6 @@ antimultiplicative antipode data on generators.
22
* `LinearMap.convMul_eq_one_of_adjoin_eq_top_left` and
23
`LinearMap.convMul_eq_one_of_adjoin_eq_top_right`: a pointwise one-sided convolution inverse of
24
a multiplicative map on generators is a global one.
25
-* `HopfAlgebra.eq_antipode_of_convMul_id_eq_one` and
26
- `HopfAlgebra.eq_antipode_of_id_convMul_eq_one`: a one-sided convolution inverse of `id` is the
27
- antipode.
28
* `HopfAlgebra.eq_antipode_of_adjoin_eq_top_left` and
29
`HopfAlgebra.eq_antipode_of_adjoin_eq_top_right`: a one-sided convolution inverse of `id` on a
30
generating set is the antipode.
0 commit comments