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

This is in a separate file to avoid needing to import Field in Mathlib/Algebra/Ring/Equiv.lean

theorem IsLocalHom.isField {A : Type u_1} {B : Type u_2} {F : Type u_3} [Semiring A] [Semiring B] [FunLike F A B] [MonoidWithZeroHomClass F A B] {f : F} [IsLocalHom f] (inj : Function.Injective ⇑f) (hB : IsField B) : IsField A

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

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