Theorem BialgEquiv.toLinearMap_ofAlgEquiv

Modification history

2025-07-11 14:29
Mathlib/RingTheory/Bialgebra/Equiv.lean
feat: promote an `AlgEquiv` preserving `counit` and `comul` to a `BialgEquiv` (#25271) …
Added BialgEquiv.toLinearMap_ofAlgEquivView on Github →