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

noncomputable def AVenhance.Ingredients.KhomScalar {β : ℝ} (I : Ingredients β) (κ : ℝ) (m : ℕ) : ℝ

The scalar a with KBar^κ_m = a I (line 2994): the (1,1) entry. That KBar is scalar and a > 0 is the theorem Khom_eq_scalar; the abuse of notation of the source is KhomScalar.

Equations

• I.KhomScalar κ m = I.Khom κ m 0 0