Theorem BialgEquiv.coe_ofBijective

Modification history

2025-07-11 14:29
Mathlib/RingTheory/Bialgebra/Equiv.lean
feat: promote an `AlgEquiv` preserving `counit` and `comul` to a `BialgEquiv` (#25271) …
Modified BialgEquiv.coe_ofBijectiveView on Github →
2025-05-16 10:01
Mathlib/RingTheory/Bialgebra/Equiv.lean
feat(RingTheory/Coalgebra/Equiv, RingTheory/Bialgebra/Equiv): constructors for coalgebra and bialgebra equivalences (#24121) …
Added BialgEquiv.coe_ofBijectiveView on Github →