noncomputable def ClassGroupFinite.minkowskiConstant (K : Type u_1) [Field K] [NumberField K] : ℝ

theorem ClassGroupFinite.idealClass_exists_integral_absNorm_le_minkowskiConstant (K : Type u_1) [Field K] [NumberField K] (C : ClassGroup (NumberField.RingOfIntegers K)) : ∃ (I : ↥(nonZeroDivisors (Ideal (NumberField.RingOfIntegers K)))), ClassGroup.mk0 I = C ∧ ↑(Ideal.absNorm ↑I) ≤ minkowskiConstant K

theorem ClassGroupFinite.ideals_bounded_absNorm_card_le (K : Type u_1) [Field K] [NumberField K] (M : ℕ) : Nat.card ↑{I : Ideal (NumberField.RingOfIntegers K) | I ≠ ⊥ ∧ Ideal.absNorm I ≤ M} ≤ (Module.finrank ℚ K * M) ^ Nat.log 2 M

theorem ClassGroupFinite.classGroup_finite (K : Type u_1) [Field K] [NumberField K] : Finite (ClassGroup (NumberField.RingOfIntegers K))