Module

SquarefreeIntegralCoordinates.lean

Nyll.SawinTotallyRealTowers.SquarefreeIntegralCoordinates

1 declaration indexed from sourceView source ↗

Module documentation

Integral rational coordinates after multiplication by a squarefree integer

If a signed squarefree integer times the square of a rational number is integral, the denominator squared divides the squarefree integer. Coprimality of the rational numerator and denominator then forces the denominator to be one.

Imports2

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

Imported by3

theorem

exists_int_eq_of_squarefree_mul_sq_eq_int

L22 ↗

ClassFieldTower.Sawin.exists_int_eq_of_squarefree_mul_sq_eq_int

Documentation

A rational number whose square becomes integral after multiplication by a signed squarefree integer is itself integral.

Source context 1 command

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

namespace ClassFieldTower.Sawin

Lean source · statement

theorem exists_int_eq_of_squarefree_mul_sq_eq_int
    (d : ℤ) (hd : Squarefree d.natAbs) (x : ℚ)
    (hx : ∃ m : ℤ, (d : ℚ) * x ^ 2 = (m : ℚ)) :
    ∃ n : ℤ, x = (n : ℚ)

Module documentation

Integral rational coordinates after multiplication by a squarefree integer

Declarations

exists_int_eq_of_squarefree_mul_sq_eq_int