mathlib3

25d8aac6 - chore(field_theory): turn `intermediate_field.subalgebra.equiv_of_eq` into `intermediate_field.equiv_of_eq` (#8069)

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`.) Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com>