Theorem AlgHomClass.toLinearMap_toAlgHom

Modification history

2026-09-09 08:54
Mathlib/Algebra/Algebra/Hom.lean
chore: rename Alg{Hom,Equiv}Class.toAlg{Hom,Equiv} to Alg{Hom,Equiv}.ofClass (#43557) …
Deleted AlgHomClass.toLinearMap_toAlgHomView on Github →
2025-07-11 14:29
Mathlib/Algebra/Algebra/Hom.lean
feat: promote an `AlgEquiv` preserving `counit` and `comul` to a `BialgEquiv` (#25271) …
Added AlgHomClass.toLinearMap_toAlgHomView on Github →