Def BialgHom.toAlgHom

Modification history

2026-05-05 00:06
Mathlib/RingTheory/Bialgebra/Hom.lean
refactor(Algebra): replace `AlgHomClass` coercions with structure-specific coercions (#38715) …
Added BialgHom.toAlgHomView on Github →