ModuleQuadraticIntegralGenerator.lean
Nyll.SawinTotallyRealTowers.QuadraticIntegralGenerator
2 declarations indexed from sourceView source ↗ Module documentation
Integral elements expressed using a rational square root
A square root of an integer is integral. More generally, the element (m + n * α) / 2, where α ^ 2 = d, is integral whenever 4 ∣ m ^ 2 - d * n ^ 2. The divisibility witness supplies the integer constant coefficient of the monic polynomial X ^ 2 - m * X + k. No degree or squarefreeness assumption is needed for this construction.
Imports5
- Mathlib.Algebra.Algebra.Basic
- Mathlib.Algebra.Algebra.Rat
- Mathlib.Algebra.Polynomial.Monic
- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
- Mathlib.Tactic.LinearCombination
Imported by3
Declarations
ClassFieldTower.Sawin.isIntegral_int_of_sq_eq_int
DocumentationA square root of an integer in a ℚ-algebra is integral over ℤ.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open Polynomial
universe u
namespace ClassFieldTower.Sawin
ClassFieldTower.Sawin.isIntegral_half_int_linear_combination_of_four_dvd
DocumentationThe congruence m ^ 2 ≡ d * n ^ 2 (mod 4) makes the half-integer linear combination of 1 and a square root of d integral over ℤ.
Source context 3 commands
Surrounding namespaces, section variables, and local commands at this declaration.
open Polynomial
universe u
namespace ClassFieldTower.Sawin