Module

RationalSquarefree.lean

Nyll.SawinTotallyRealTowers.RationalSquarefree

1 declaration indexed from sourceView source ↗

Module documentation

Signed squarefree representatives of rational square classes

Apply the natural-number squarefree decomposition to the product of the absolute numerator and denominator. The numerator's sign then gives an integer representative without introducing a square root in an extension.

Imports2

Mathlib.Data.Nat.Squarefree
Mathlib.Data.Rat.Cast.Defs

Imported by2

theorem

exists_squarefree_int_mul_sq

L22 ↗

ClassFieldTower.Sawin.exists_squarefree_int_mul_sq

Documentation

Every nonzero rational number is a nonzero square times a signed squarefree integer.

Source context 1 command

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

namespace ClassFieldTower.Sawin

Lean source · statement

theorem exists_squarefree_int_mul_sq (q : ℚ) (hq : q ≠ 0) :
    ∃ d : ℤ, ∃ r : ℚ,
      Squarefree d.natAbs ∧ d ≠ 0 ∧ r ≠ 0 ∧ q = (d : ℚ) * r ^ 2

Module documentation

Signed squarefree representatives of rational square classes

Declarations

exists_squarefree_int_mul_sq