Center_of_Division_Ring_is_Subfield
Provedcenterdivision-ringsproofwikisubfields
Let K be a division ring. Then the center Z(K) is a commutative subfield.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Center_of_Division_Ring_is_Subfield {K : Type _} [DivisionRing K] (a b : K) (ha : ∀ r : K, a * r = r * a) (hb : ∀ r : K, b * r = r * b) : a * b = b * a := by sorrySource