Documentation
Project
.
Example
Search
return to top
source
Imports
Init
Mathlib.FieldTheory.Finite.Basic
Imported by
card
card_units
katabami_theorem_fermat1
katabami_theorem_fermat2
katabami_theorem_fermat3
source
theorem
card
(
n
:
ℕ
)
[
Fintype
(
ZMod
n
)
]
:
Fintype.card
(
ZMod
n
)
=
n
source
theorem
card_units
(
p
:
ℕ
)
[
Fact
(
Nat.Prime
p
)
]
:
Fintype.card
(
ZMod
p
)
ˣ
=
p
-
1
source
theorem
katabami_theorem_fermat1
(
p
:
ℕ
)
[
Fact
(
Nat.Prime
p
)
]
{
a
:
ZMod
p
}
(
ha
:
a
≠
0
)
:
a
^
(
p
-
1
)
=
1
source
theorem
katabami_theorem_fermat2
(
p
:
ℕ
)
[
Fact
(
Nat.Prime
p
)
]
(
a
:
(
ZMod
p
)
ˣ
)
:
a
^
(
p
-
1
)
=
1
source
theorem
katabami_theorem_fermat3
(
p
:
ℕ
)
[
Fact
(
Nat.Prime
p
)
]
{
a
:
ZMod
p
}
(
ha
:
a
≠
0
)
:
a
^
(
p
-
1
)
=
1