Subfields

Some useful results on fieldRange.

theorem RingHom.mem_fieldRange_self {K : Type u_1} {L : Type u_2} [DivisionRing K] [DivisionRing L] (f : K →+* L) (x : K) : f x ∈ f.fieldRange

theorem RingHom.fieldRange_eq_top_iff {K : Type u_1} {L : Type u_2} [DivisionRing K] [DivisionRing L] {f : K →+* L} : f.fieldRange = ⊤ ↔ Function.Surjective ⇑f