Commit 2021-06-24 16:50 25d8aac6

chore(field_theory): turn intermediate_field.subalgebra.equiv_of_eq into intermediate_field.equiv_of_eq (#8069) I was looking for intermediate_field.equiv_of_eq. There was a definition of subalgebra.equiv_of_eq in the intermediate_field namespace which is equal to the original subalgebra.equiv_of_eq definition. Meanwhile, there was no intermediate_field.equiv_of_eq. So I decided to turn the duplicate into what I think was intended. (As a bonus, I added the simp lemmas from subalgebra.equiv_of_eq.)