NYLL
Module

QuadraticIntegralParity.lean

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

Module documentation

Parity of integral quadratic coordinates

For a signed squarefree integer d, the norm numerator a² - d b² is divisible by four precisely for even coordinates, or for odd coordinates when d is one modulo four.

Imports2
  • Mathlib.Data.Nat.Squarefree
  • Mathlib.NumberTheory.Multiplicity
Imported by2

Declarations

theorem

sq_mod_four_eq_zero_of_even

L20 ↗
ClassFieldTower.Sawin.sq_mod_four_eq_zero_of_even
Source context 1 command

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

namespace ClassFieldTower.Sawin
Lean source · statement
theorem sq_mod_four_eq_zero_of_even {x : ℤ} (hx : Even x) :
    x ^ 2 % 4 = 0
theorem

four_dvd_sq_sub_mul_sq_iff

L28 ↗
ClassFieldTower.Sawin.four_dvd_sq_sub_mul_sq_iff
Documentation

The parity criterion for half-integer coordinates in a quadratic field.

Source context 1 command

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

namespace ClassFieldTower.Sawin
Lean source · statement
theorem four_dvd_sq_sub_mul_sq_iff
    (d a b : ℤ) (hd : Squarefree d.natAbs) :
    4 ∣ a ^ 2 - d * b ^ 2 ↔
      (Even a ∧ Even b) ∨ (Odd a ∧ Odd b ∧ d % 4 = 1)

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