If a semiring is a field, any isomorphic semiring is also a field.

This is in a separate file to avoiding need to import Field in Mathlib.Algebra.Ring.Equiv.

theorem MulEquiv.isField {A : Type u_1} (B : Type u_2) [Semiring A] [Semiring B] (hB : IsField B) (e : A ≃* B) : IsField A