The only normed division algebras over ℝ are ℝ, ℂ, ℍ, and 𝕆.

#61 on Parcly-Taxel's 100 theorems list for Mathlib.

Sorry-free Lean 4 + Mathlib.

Both in Hurwitz.lean:

theorem hurwitz_dimension
    {A : Type*} [NonAssocRing A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A]
    [FiniteDimensional ℝ A]
    (N : QuadraticForm ℝ A) (hcomp : ∀ x y : A, N (x * y) = N x * N y)
    (hone : N 1 = 1) (hnd : ∀ x : A, N x = 0 → x = 0) :
    Module.finrank ℝ A ∈ ({1, 2, 4, 8} : Set ℕ)

theorem hurwitz_classification
    {A : Type*} [NonAssocRing A] [Module ℝ A] [IsScalarTower ℝ A A] [SMulCommClass ℝ A A]
    [FiniteDimensional ℝ A]
    (N : QuadraticForm ℝ A) (hcomp : ∀ x y, N (x * y) = N x * N y)
    (hone : N 1 = 1) (hnd : ∀ x, N x = 0 → x = 0) :
    Nonempty (A ≃+* ℝ) ∨ Nonempty (A ≃+* ℂ) ∨
    Nonempty (A ≃+* ℍ[ℝ]) ∨ Nonempty (A ≃+* 𝕆[ℝ])

File	Lines
⭐ Hurwitz.lean	93	the two main theorems
Hurwitz/Octonion.lean	325	octonion algebra, normSq, finrank = 8
CompositionAlgebra/Basic.lean	284	polar form, conjugation, alternative laws
CompositionAlgebra/CayleyDicksonDoubling.lean	472	doubling argument: dim >= 2, 4, 8
CompositionAlgebra/DimensionBound.lean	1545	dim in {1,2,4,8}
CompositionAlgebra/IsomReal.lean	47	dim 1 => iso R
CompositionAlgebra/IsomComplex.lean	94	dim 2 => iso C
CompositionAlgebra/IsomQuaternion.lean	327	dim 4 => iso H
CompositionAlgebra/IsomOctonion.lean	797	dim 8 => iso O