Def AdjoinRoot

Modification history

2025-10-23 00:03

Mathlib/RingTheory/AdjoinRoot.lean

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

Modified AdjoinRoot View on Github →

2023-05-24 10:36

Mathlib/RingTheory/AdjoinRoot.lean

feat: port RingTheory.AdjoinRoot (#4271)

Added AdjoinRoot View on Github →