Artie Khovanov
Artie Khovanov
In my real closed field repo, I had defined ordered algebras because I couldn't find them in Mathlib. Today I found out they have been "defined" in Mathlib not once...
> Moving it to `Algebra.Order.Algebra` would help OK, I will switch the module deprecation.
@jcommelin fixed
Spurious CI failure
Is it standard in this part of the library to construct field extensions as `IntermediateField`s below the algebraic closure? That's not the design of `AdjoinRoot`, `IsAdjoinRoot`, `QuadraticExtension`, *or* `IsCyclotomicExtension`, which...
@dleijnse those constructions could have equally been implemented using `Subalgebra`. I wasn't trying to point out he distinction between ring and field, but rather the distinction between defining the extension...