Def BialgEquiv.ofAlgEquiv

Modification history

2025-08-21 10:17
Mathlib/RingTheory/Bialgebra/Equiv.lean
refactor: state hypotheses of `BialgHom.ofAlgHom` as equalities of `AlgHom`s (#28142) …
Modified BialgEquiv.ofAlgEquivView on Github →
2025-07-11 14:29
Mathlib/RingTheory/Bialgebra/Equiv.lean
feat: promote an `AlgEquiv` preserving `counit` and `comul` to a `BialgEquiv` (#25271) …
Added BialgEquiv.ofAlgEquivView on Github →