Theorem AdjoinRoot.liftHom_mk

Modification history

2025-10-23 00:03

Mathlib/RingTheory/AdjoinRoot.lean

feat(AdjoinRoot): bundle operations as `AlgHom`s (#29132) …

Modified AdjoinRoot.liftHom_mk View on Github →

2023-05-24 10:36

Mathlib/RingTheory/AdjoinRoot.lean

feat: port RingTheory.AdjoinRoot (#4271)

Added AdjoinRoot.liftHom_mk View on Github →