def LatticeShortestVector.IsGramSchmidt {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (b b_star : Fin n → E) : Prop

theorem LatticeShortestVector.lattice_vector_norm_bound {n : ℕ} (hn : 0 < n) (b : Fin n → EuclideanSpace ℝ (Fin n)) (_hb_li : LinearIndependent ℝ b) (b_star : Fin n → EuclideanSpace ℝ (Fin n)) (hgs : IsGramSchmidt b b_star) (v : EuclideanSpace ℝ (Fin n)) (hv_lattice : ∃ (c : Fin n → ℤ), v = ∑ i : Fin n, ↑(c i) • b i) (hv_nonzero : v ≠ 0) : ‖v‖ ≥ ⨅ (i : Fin n), ‖b_star i‖