Def IsAdjoinRootMonic.basis

Modification history

2026-03-21 17:40

Mathlib/RingTheory/IsAdjoinRoot.lean

feat(Algebra/MonoidAlgebra): `map` and `comapDomain` (#36768) …

Modified IsAdjoinRootMonic.basis View on Github →

2025-07-23 19:36

Mathlib/RingTheory/IsAdjoinRoot.lean

style(RingTheory/IsAdjoinRoot): improve style and golf (#27374) …

Modified IsAdjoinRootMonic.basis View on Github →

2023-06-19 04:18

Mathlib/RingTheory/IsAdjoinRoot.lean

feat: port RingTheory.IsAdjoinRoot (#5190)

Added IsAdjoinRootMonic.basis View on Github →