Module

RootDiscriminantBound.lean

Nyll.ClassFieldTheory.AlgebraicNumberTheory.NumberField.RootDiscriminantBound

1 declaration indexed from sourceView source ↗

Module documentation

From an integral discriminant bound to a root discriminant bound

Imports4

Mathlib.NumberTheory.NumberField.Discriminant.Basic
Mathlib.Analysis.SpecialFunctions.Pow.Real
Mathlib.Tactic.Positivity
Mathlib.Tactic.NormNum

Imported by2

theorem

rootDiscr_le_of_natAbs_discr_le_pow

L20 ↗

AlgebraicNumberTheory.DiscriminantBounds.rootDiscr_le_of_natAbs_discr_le_pow

Documentation

A degree-power bound on the absolute discriminant gives a uniform bound on the usual real root discriminant.

Source context 1 command

Surrounding namespaces, section variables, and local commands at this declaration.

namespace AlgebraicNumberTheory.DiscriminantBounds

Lean source · statement

theorem rootDiscr_le_of_natAbs_discr_le_pow
    (F : Type*) [Field F] [NumberField F] (C : ℕ)
    (h : (NumberField.discr F).natAbs ≤ C ^ Module.finrank ℚ F) :
    NumberField.rootDiscr F ≤ (C : ℝ)

Module documentation

From an integral discriminant bound to a root discriminant bound

Declarations

rootDiscr_le_of_natAbs_discr_le_pow