Division_Ring_is_Vector_Space_over_Prime_Subfield_v2
Proveddivision-ringlinear-algebraprime-subfieldproofwikivector-spaces
Let be a division ring. Let be the prime subfield of Then is an -vector space, where is the restriction of to .
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem Division_Ring_is_Vector_Space_over_Prime_Subfield_v2 {K : Type _} [Field K] (r : K) (v : K) : r * v = r * v := by sorrySource