Documentation
FormalConjectures
.
ForMathlib
.
Data
.
Nat
.
Prime
.
Composite
Search
return to top
source
Imports
Init
Mathlib.Data.Nat.Prime.Defs
Imported by
Nat
.
Composite
source
@[reducible, inline]
abbrev
Nat
.
Composite
(
n
:
ℕ
)
:
Prop
Equations
n
.
Composite
=
(
1
<
n
∧
¬
Nat.Prime
n
)
Instances For