A uniform product-of-minima bound from Blichfeldt's principle. The constant n^n is sufficient for the number-field lattice application.

theorem CCDN.lattice_flag_minima_product_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {n : ℕ} (hn : 0 < n) (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (c : OrthonormalBasis (Fin n) ℝ E) (a : Fin n → ℝ) (hpos : ∀ (i : Fin n), 0 < a i) (hmono : Monotone a) (hminimum : ∀ (i : Fin n), ∀ x ∈ L, x ∉ Submodule.span ℝ (⇑c '' Set.Iio i) → a i ≤ ‖x‖) : ∏ i : Fin n, a i ≤ ↑n ^ n * ZLattice.covolume L MeasureTheory.volume

Any positive monotone sequence of flag minima has product at most n^n times the lattice covolume.