let Z := center R
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
⊢ IsField R
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
⊢ IsField R