Commit 2023-05-25 08:46 4c6c02a9

View on Github →

feat: port RingTheory.Adjoin.Field (#4303)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Adjoin/Field.lean

added def AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly

added theorem lift_of_splits