image of a field is a field

Stream: Is there code for X?

[Edison Xie]

Do we have that for f : F →+* R a ring homomorphism, if F is a field then f.range is also a field?

[Eric Wieser]

docs#RingHom.fieldRange is close but not what you want

[Kevin Buzzard]

It's not true if R=0

[Aaron Liu]

If R is nontrivial then

import Mathlib

example {R S : Type*} [Ring R] [Ring S] [Nontrivial S] (f : R →+* S) (hr : IsField R) : IsField f.range :=
  have b : RingHom.ker f = ⊥ := (RingHom.ker_eq_bot_iff_eq_zero f).2 fun _ hx =>
    let := hr.toField
    isUnit_iff_ne_zero.not_left.1 fun hu => (hu.map f).ne_zero hx
  (f.quotientKerEquivRange.symm.trans
    ((Ideal.quotEquivOfEq b).trans (RingEquiv.quotientBot R))).toMulEquiv.isField R hr

[Edison Xie]

Aaron Liu said:

If R is nontrivial then

import Mathlib

example {R S : Type*} [Ring R] [Ring S] [Nontrivial S] (f : R →+* S) (hr : IsField R) : IsField f.range :=
  have b : RingHom.ker f = ⊥ := (RingHom.ker_eq_bot_iff_eq_zero f).2 fun _ hx =>
    let := hr.toField
    isUnit_iff_ne_zero.not_left.1 fun hu => (hu.map f).ne_zero hx
  (f.quotientKerEquivRange.symm.trans
    ((Ideal.quotEquivOfEq b).trans (RingEquiv.quotientBot R))).toMulEquiv.isField R hr

If this is not a one-liner, does that mean we should have it in Mathlib?