NYLL
Module

QuadraticSquareClass.lean

Nyll.SawinTotallyRealTowers.QuadraticSquareClass
2 declarations indexed from sourceView source ↗

Module documentation

Uniqueness of squarefree quadratic radicands

Two signed squarefree integers in the same rational square class agree. Taking traces in a quadratic field shows that any two square-root generators have squares in the same rational square class. Thus the normalized radicand of a quadratic field is unique, including its sign.

Imports4
Imported by1

Declarations

theorem

squarefree_int_eq_of_mul_rat_sq

L27 ↗
ClassFieldTower.Sawin.squarefree_int_eq_of_mul_rat_sq
Documentation

Signed squarefree integers representing the same rational square class are equal; no positivity assumption is necessary.

Source context 2 commands

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

universe u
namespace ClassFieldTower.Sawin
Lean source · statement
theorem squarefree_int_eq_of_mul_rat_sq
    (d e : ℤ) (hd : Squarefree d.natAbs) (he : Squarefree e.natAbs)
    (q : ℚ) (h : (d : ℚ) = (e : ℚ) * q ^ 2) : d = e
theorem

quadratic_squarefree_radicand_unique

L49 ↗
ClassFieldTower.Sawin.quadratic_squarefree_radicand_unique
Documentation

Any two signed squarefree square-root generators of the same quadratic extension have the same radicand.

Source context 2 commands

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

universe u
namespace ClassFieldTower.Sawin
Lean source · statement
theorem quadratic_squarefree_radicand_unique
    (L : Type u) [Field L] [Algebra ℚ L] [Algebra.IsQuadraticExtension ℚ L]
    (d e : ℤ) (hd : Squarefree d.natAbs) (he : Squarefree e.natAbs)
    (α β : L)
    (hαSquare : α ^ 2 = algebraMap ℚ L (d : ℚ))
    (hβSquare : β ^ 2 = algebraMap ℚ L (e : ℚ))
    (hαGenerate : IntermediateField.adjoin ℚ ({α} : Set L) = ⊤)
    (hβGenerate : IntermediateField.adjoin ℚ ({β} : Set L) = ⊤) : d = e

Statements and documentation are read from the Lean source at the revision shown. Source entries are not a measure of mathematical completeness.