1 parent 6e3d202 commit 908bd52Copy full SHA for 908bd52
1 file changed
Mathlib/RingTheory/Coalgebra/IsFrobenius.lean
@@ -58,7 +58,6 @@ In texts, this is what the Frobenius equations are usually referred to as.
58
* `Bialgebra.nonempty_algEquiv_of_isFrobenius`: when an `R`-bialgebra `A` satisfies the Frobenius
59
equations, `R` is isomorphic to `A`
60
61
-
62
## TODO
63
64
* show `IsFrobenius R (A ⊗ B)`
0 commit comments