Module

QuadraticBasisDiscriminant.lean

Nyll.SawinTotallyRealTowers.QuadraticBasisDiscriminant

1 declaration indexed from sourceView source ↗

Module documentation

Discriminant of a quadratic square-root basis

The actual rational basis 1, α, where α² = d, has diagonal trace matrix with entries 2 and 2d. Its discriminant is therefore 4d. No integrality or squarefreeness assumption is needed.

Imports3

Nyll.SawinTotallyRealTowers.QuadraticBasis
Nyll.SawinTotallyRealTowers.QuadraticTrace
Mathlib.RingTheory.Discriminant

Imported by2

theorem

discr_quadraticBasis

L24 ↗

ClassFieldTower.Sawin.discr_quadraticBasis

Documentation

The discriminant of the rational square-root basis is 4d.

Source context 2 commands

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

universe u
namespace ClassFieldTower.Sawin

Lean source · statement

theorem discr_quadraticBasis
    (L : Type u) [Field L] [Algebra ℚ L] [Algebra.IsQuadraticExtension ℚ L]
    (d : ℚ) (α : L) (hSquare : α ^ 2 = algebraMap ℚ L d)
    (hGenerate : IntermediateField.adjoin ℚ ({α} : Set L) = ⊤) :
    Algebra.discr ℚ (quadraticBasis L α hGenerate) = 4 * d

Module documentation

Discriminant of a quadratic square-root basis

Declarations

discr_quadraticBasis