def Legendre.InLegendreInterval (n p : ℕ) : Prop

p lies strictly between n^2 and (n + 1)^2.

Equations

• Legendre.InLegendreInterval n p = (n ^ 2 < p ∧ p < (n + 1) ^ 2)

def Legendre.HasLegendrePrime (n : ℕ) : Prop

Existence of a prime strictly between consecutive squares.

Equations

• Legendre.HasLegendrePrime n = ∃ (p : ℕ), Nat.Prime p ∧ Legendre.InLegendreInterval n p

instance Legendre.instDecidableInLegendreInterval (n p : ℕ) : Decidable (InLegendreInterval n p)

Equations

• Legendre.instDecidableInLegendreInterval n p = id inferInstance