Commit 2023-10-30 03:09 0044ce8e
View on Github →refactor(FieldTheory/Adjoin): provide a better defeq for ⊥ (#7957)
This means (⊥ : IntermediateField F E).toSubalgebra = ⊥ is true by definition.
Also adds IntermediateField.map_bot now that the proof is trivial.