Composite numbers

DefinitionComposite numbers#✓fully proved

A natural number \(n\) is composite if \(n > 1\) and \(n\) is not prime.

def IsComposite (n : ℕ) : Prop :=
  1 < n ∧ ¬ n.Prime

Used by 4

Used byFibonacci squares plus one are eventually composite · Composite numbers are not prime · Composite numbers exceed one · Composite numbers from Mersenne shifts of an arithmetic progression

TheoremComposite numbers exceed one#✓fully proved

Every composite natural number \(n\) satisfies \(1 < n\).

theorem IsComposite.one_lt {n : ℕ} (h : n.IsComposite) : 1 < n

Uses 1

Statement usesComposite numbers

TheoremComposite numbers are not prime#✓fully proved

A composite natural number is not prime.

theorem IsComposite.not_prime {n : ℕ} (h : n.IsComposite) : ¬ n.Prime

Uses 1

Statement usesComposite numbers

3 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.