simp only [_root_.pow_zero] at h_card
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
H : ∃ x y, x ≠ y
h_card : Fintype.card R = Fintype.card ↥Z ^ 0
⊢ False
R : Type u_1
inst✝¹ : DecidableEq R
inst✝ : DivisionRing R
h : Fintype R
Z : Subring R := center R
H : ∃ x y, x ≠ y
h_card : Fintype.card R = 1
⊢ False