Documentation
Marginis
.
BrunjesSerpe2007
Search
Google site search
return to top
source
Imports
Init
Mathlib.Data.Nat.Prime.Defs
Imported by
φ₀
proof_of_concept
ψ
sqrt_mod2
sqrt_mod3
Enlargements of schemes
#
by Lars Brünjes and Christian Serpé
JLA 2007
source
def
φ₀
(p :
ℕ
)
:
Prop
Equations
φ₀
p
=
(
(
2
+
0
)
%
p
=
0
%
p
)
Instances For
source
theorem
proof_of_concept
:
¬
∀ (
p
q
:
ℕ
),
Nat.Prime
p
→
Nat.Prime
q
→
(
φ₀
p
↔
φ₀
q
)
source
def
ψ
(p :
ℕ
)
(x :
ℕ
)
:
Prop
Equations
ψ
p
x
=
(
x
*
x
%
p
=
2
%
p
)
Instances For
source
theorem
sqrt_mod2
:
∃ (
x
:
ℕ
),
ψ
2
x
source
theorem
sqrt_mod3
:
¬
∃ (
x
:
ℕ
),
ψ
3
x