LeanPool.EcTateLean.Algebra.EllipticCurve.Kronecker

Imported Lean Pool material for LeanPool.EcTateLean.Algebra.EllipticCurve.Kronecker.

theorem div_succ_le_succ_div (m n : ℕ) : m.succ / n.succ ≤ (m / n.succ).succ

theorem div2_succ_succ_eq_succ_div2 (n : ℕ) : n.succ.succ / 2 = (n / 2).succ

theorem Int.div2_lt_self {x : ℕ} (h : 0 < x) : x / 2 < x

theorem Int.div2_succ_le_self (x : ℕ) : x.succ / 2 ≤ x

@[irreducible]

def Int.valBinNat (x : ℕ) : ℕ × ℕ

The 2-adic valuation and odd part of a natural number: valBinNat x = (v, r) where x = 2 ^ v * r with r odd (and (0, 0) for x = 0).

Equations

• Int.valBinNat x = if h : 0 < x ∧ x % 2 = 0 then have decr := ⋯; have vbn_half := Int.valBinNat (x / 2); (vbn_half.1 + 1, vbn_half.2) else if 0 < x then (0, x) else (0, 0)

theorem Int.valBinNat_even {x : ℕ} (h : 0 < x ∧ x % 2 = 0) : valBinNat x = ((valBinNat (x / 2)).1 + 1, (valBinNat (x / 2)).2)

def Int.valBin (x : ℤ) : ℕ × ℤ

The 2-adic valuation and signed odd part of an integer: valBin x = (v, r) where x = 2 ^ v * r with |r| odd.

Equations

• x.valBin = match Int.valBinNat x.natAbs with | (v, r) => (v, x.sign * ↑r)

theorem Int.odd_part_le_self_nat (x : ℕ) : (valBinNat x).2 ≤ x

theorem Int.odd_part_succ_pos (x : ℕ) : 0 < (valBinNat x.succ).2

theorem Int.odd_part_nat_pos (x : ℕ) : x ≠ 0 → 0 < (valBinNat x).2

def Int.kronecker_2 (x : ℕ) : ℤ

The Kronecker symbol (x / 2), which depends only on x mod 8.

Equations

• Int.kronecker_2 x = match x % 8 with | 1 => 1 | 7 => 1 | 3 => -1 | 5 => -1 | x => 0

@[irreducible]

def Int.kroneckerOdd (k : ℤ) (a b : ℕ) : ℤ

Auxiliary recursion computing the Kronecker symbol (a / b) for odd b, carrying an accumulated sign k; it strips powers of two from a via quadratic reciprocity until a is reduced.

Equations

• One or more equations did not get rendered due to their size.

def Int.kronecker (a b : ℤ) : ℤ

The Kronecker symbol (a / b) for integers a and b.

Equations

• One or more equations did not get rendered due to their size.

def Int.exRootQuad (a b c p : ℤ) : Bool

Decides, via the Kronecker symbol, whether the quadratic a x ^ 2 + b x + c has a root modulo p. This naive version fails for p = 2.

Equations

• a.exRootQuad b c p = decide (((b % p * (b % p) - 4 * (a % p) * (c % p)) % p).kronecker p = 1)

def Int.quadRootInZpZ (a b c : ℤ) (p : ℕ) : Bool

Decides whether the quadratic a x ^ 2 + b x + c has a root in ℤ / p ℤ, assuming p > 1 and p ∤ a.

Equations

• One or more equations did not get rendered due to their size.
• a.quadRootInZpZ b c 0 = panicWithPosWithDecl "LeanPool.EcTateLean.Algebra.EllipticCurve.Kronecker" "Int.quadRootInZpZ" 177 9 "unreachable code has been reached"
• a.quadRootInZpZ b c 1 = panicWithPosWithDecl "LeanPool.EcTateLean.Algebra.EllipticCurve.Kronecker" "Int.quadRootInZpZ" 178 9 "unreachable code has been reached"