Division_Ring_is_Vector_Space_over_Prime_Subfield_v3
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_v3 {K : Type _} [Field K] : forall (r s : K) (v : K), r • (s • v) = (r * s) • v ∧ (1 : K) • v = v := by sorrySource