Theorem AdjoinRoot.liftHom_mk

Modification history

2026-04-17 09:59
Mathlib/RingTheory/AdjoinRoot.lean
chore: remove declarations deprecated between 2021-04-15 and 2025-10-15 (#38057) …
Deleted AdjoinRoot.liftHom_mkView on Github →
2026-03-04 12:02
Mathlib/RingTheory/AdjoinRoot.lean
feat(Algebra/Polynomial): add aevalEquiv and its bivariate version (#35283)
Modified AdjoinRoot.liftHom_mkView on Github →
2025-10-23 00:03
Mathlib/RingTheory/AdjoinRoot.lean
feat(AdjoinRoot): bundle operations as `AlgHom`s (#29132) …
Modified AdjoinRoot.liftHom_mkView on Github →
2023-05-24 10:36
Mathlib/RingTheory/AdjoinRoot.lean
feat: port RingTheory.AdjoinRoot (#4271)
Added AdjoinRoot.liftHom_mkView on Github →