English
If |discr K| ≤ N for a number field K, then finrank_Q K ≤ rankOfDiscrBdd N.
Русский
Если для числа поля K выполняется |дискр K| ≤ N, то finrank_Q K не превосходит rankOfDiscrBdd N.
LaTeX
$$$$\\operatorname{finrank}_{\\mathbb{Q}}(K) \\le \\operatorname{rankOfDiscrBdd}(N).$$$$
Lean4
/-- If `|discr K| ≤ N` then the Minkowski bound of `K` is less than `boundOfDiscrBdd`. -/
theorem minkowskiBound_lt_boundOfDiscBdd : minkowskiBound K ↑1 < boundOfDiscBdd N :=
by
have : boundOfDiscBdd N - 1 < boundOfDiscBdd N := by
simp_rw [boundOfDiscBdd, add_tsub_cancel_right, lt_add_iff_pos_right, zero_lt_one]
refine lt_of_le_of_lt ?_ (coe_lt_coe.mpr this)
rw [minkowskiBound, volume_fundamentalDomain_fractionalIdealLatticeBasis, boundOfDiscBdd, add_tsub_cancel_right,
Units.val_one, FractionalIdeal.absNorm_one, Rat.cast_one, ENNReal.ofReal_one, one_mul, mixedEmbedding.finrank,
volume_fundamentalDomain_latticeBasis, coe_mul, ENNReal.coe_pow, coe_ofNat,
show sqrt N = (1 : ℝ≥0∞) * sqrt N by rw [one_mul]]
gcongr
· exact pow_le_one₀ (by positivity) (by simp)
·
rwa [← NNReal.coe_le_coe, coe_nnnorm, Int.norm_eq_abs, ← Int.cast_abs, NNReal.coe_natCast, ← Int.cast_natCast,
Int.cast_le]
· exact one_le_two
· exact rank_le_rankOfDiscrBdd hK
