The algebraic nondegeneracy input for the uniform shape estimate of a number-field lattice. Multiplication preserving a rational hyperplane must be multiplication by a scalar. The proof uses linear functionals and works over an arbitrary field extension.

theorem CCDN.multiplication_pairing_on_hyperplane_complement {F : Type u_1} {K : Type u_2} [Field F] [Field K] [Algebra F K] (ℓ μ : K →ₗ[F] F) (hℓ : ℓ ≠ 0) (hℓ1 : ℓ 1 = 0) (hμ1 : μ 1 = 1) (a : K) (ha0 : a ≠ 0) (hℓa : ℓ a = 0) (hμa : μ a = 0) : ∃ (b : K), ℓ b = 0 ∧ μ b = 0 ∧ ℓ (a * b) ≠ 0

On the complement to the scalars inside a hyperplane containing one, the multiplication pairing detected by the hyperplane functional is nondegenerate. The second functional specifies that complement explicitly.