TODO: Add doc-string.

theorem pow_finrank_le_abs_discr_of_le_rootDiscr (K : Type u_1) [Field K] [NumberField K] {c : ℝ} (hc : 0 ≤ c) (h : c ≤ NumberField.rootDiscr K) : c ^ Module.finrank ℚ K ≤ |↑(NumberField.discr K)|

theorem target_pow_finrank_le_abs_discr (K : Type u_1) [Field K] [NumberField K] (h : 8.25 ≤ NumberField.rootDiscr K) : 8.25 ^ Module.finrank ℚ K ≤ |↑(NumberField.discr K)|