Keyboard shortcuts

Press ← or → to navigate between chapters

Press ? to show this help

Press Esc to hide this help

Successive Minima

Abstract

Successive minima yield linearly independent lattice points in dilated convex bodies.

Theorem 1.1 (Successive Minima).

Lean statement: D5/S3/Arith/AbsoluteValues/Heights/SuccessiveMinima.exists_linearIndependent_mem_smul_successiveMinimum

Proof. Machine-checked in Lean as D5/S3/Arith/AbsoluteValues/Heights/SuccessiveMinima.exists_linearIndependent_mem_smul_successiveMinimum (✓ std3). ∎

Citation. Ralf Stephan (2026). Subspace-Theorems. URL: https://github.com/rwst/Subspace-Theorems/tree/bfd830f481b296989fa5f0c1e48d9316f72270d8.

Commentary.

Successive minima yield linearly independent lattice points in dilated convex bodies.

References

  • Truth anchor: D5/S3/Arith/AbsoluteValues/Heights/SuccessiveMinima.exists_linearIndependent_mem_smul_successiveMinimum