Theorem AdjoinRoot.liftAlgHom_eq_algHom

Modification history

2025-10-23 00:03
Mathlib/RingTheory/AdjoinRoot.lean
feat(AdjoinRoot): bundle operations as `AlgHom`s (#29132) …
Added AdjoinRoot.liftAlgHom_eq_algHomView on Github →