Module docstring
{"# 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.
"}
MulEquiv.isField
theorem
{A : Type*} (B : Type*) [Semiring A] [Semiring B] (hB : IsField B) (e : A ≃* B) : IsField A
Full source
protected theorem isField {A : Type*} (B : Type*) [Semiring A] [Semiring B] (hB : IsField B)
(e : A ≃* B) : IsField A where
exists_pair_ne := have ⟨x, y, h⟩ := hB.exists_pair_ne; ⟨e.symm x, e.symm y, e.symm.injective.ne h⟩
mul_comm := fun x y => e.injective <| by rw [map_mul, map_mul, hB.mul_comm]
mul_inv_cancel := fun h => by
obtain ⟨a', he⟩ := hB.mul_inv_cancel ((e.injective.ne h).trans_eq <| map_zero e)
exact ⟨e.symm a', e.injective <| by rw [map_mul, map_one, e.apply_symm_apply, he]⟩Informal description
Let $A$ and $B$ be semirings, and suppose $B$ is a field (i.e., satisfies the `IsField` predicate). If there exists a multiplicative isomorphism $e \colon A \simeq^* B$, then $A$ is also a field.