Theorem AlgEquiv.ofBijective_apply

Modification history

2025-07-11 14:29
Mathlib/Algebra/Algebra/Equiv.lean
feat: promote an `AlgEquiv` preserving `counit` and `comul` to a `BialgEquiv` (#25271) …
Modified AlgEquiv.ofBijective_applyView on Github →
2023-02-28 17:47
Mathlib/Algebra/Algebra/Equiv.lean
feat: port Algebra.Algebra.Equiv (#2413)
Added AlgEquiv.ofBijective_applyView on Github →