Epimorphism_from_Division_Ring_to_Ring
Proveddivision-ringsproofwikiring-homomorphisms
Let K be a division ring and R a nontrivial ring. If φ : K → R is a surjective ring homomorphism, then either R is the null ring or φ is an isomorphism.
Preamble
import Mathlib.Algebra.Ring.Hom.Defs import Mathlib.Algebra.Field.Basic
Formal statement
theorem Epimorphism_from_Division_Ring_to_Ring {K R : Type _} [DivisionRing K] [Ring R] [Nontrivial R] (φ : K →+* R) (hsurj : Function.Surjective φ) : Function.Injective φ := by sorrySource