Statement file: Khom_eq_scalar (Section3). This file contains exactly one declaration of the formalization's public statement surface.

theorem AVenhance.Ingredients.Khom_eq_scalar {β : ℝ} (I : Ingredients β) (κ : ℝ) (hκ : 0 < κ) (m : ℕ) (hm : 1 ≤ m) : I.Khom κ m = I.KhomScalar κ m • 1 ∧ 0 < I.KhomScalar κ m

Khom is a scalar matrix with positive scalar (source line 2994: "it follows that KBar^κ_m is a scalar matrix", "the positive scalar constant a").