Lax Lean Archive

While this submission is a draft, it cannot be used by other submissions.

Primality claims restated from lax-242665

Lax771644.ExternalPrimes · concepts/Lax771644/ExternalPrimes.lean · lax-771644

proven

Loading review…

Community review

Flags

Each flag is tied to a public ORCID identity and explains why this concept may be incorrect.

No flags have been submitted.

    Community review

    Flag this concept

    State precisely what appears incorrect. This explanation will be public under your ORCID name.

    No source line selected.

    Natural Language Statement

    Theorem

    Two statements phrased over the notion of primality of An Introduction to Lax (lax−242665lax-242665), each discharged by the corresponding statement of that submission. They exist so that this submission's proof network contains external nodes belonging to another archive record.

    Concept map
    2 concepts
    100%
    Proven claimDefinitionThis conceptRelated conceptA → B: B builds on A
    Evidence

    This concept declares 2 statements. Each proof establishes one of them relative to its assumptions.

    1 e1_has_prime_divisor proven

    2 e2_has_larger_prime proven

    Lean source view on GitHub

    1import Mathlib.Data.Nat.Notation
    2import Lax242665.Primes
    3
    4/-!
    5---
    6title: Primality claims restated from lax-242665
    7type: theorem
    8---
    9Two statements phrased over the notion of primality of *An Introduction to
    10Lax* (`lax-242665`), each discharged by the corresponding statement of that
    11submission. They exist so that this submission's proof network contains external
    12nodes belonging to another archive record.
    13
    14# Formalization notes
    15
    16The statements are verbatim copies of `lax-242665`'s two claims, so each
    17proof is the foreign statement itself. Importing `Lax242665.Primes` in the
    18concept package also puts an external node into the concept DAG.
    19-/
    20
    21namespace Lax771644.ExternalPrimes
    22
    23/-- Every natural number greater than `1` has a prime divisor, in the sense of
    24`lax-242665`. -/
    25axiom e1_has_prime_divisor : ∀ n : ℕ, 1 < n → ∃ p : ℕ, Lax242665.Primes.Prime p ∧ p ∣ n
    26
    27/-- Beyond every natural number lies a prime, in the sense of `lax-242665`. -/
    28axiom e2_has_larger_prime : ∀ n : ℕ, ∃ p : ℕ, Lax242665.Primes.Prime p ∧ n < p
    29
    30end Lax771644.ExternalPrimes
    31
    Show ProofShow Proof
    Formalization notes

    The statements are verbatim copies of lax−242665lax-242665's two claims, so each proof is the foreign statement itself. Importing Lax242665.PrimesLax242665.Primes in the concept package also puts an external node into the concept DAG.

    Builds on
    Used by

    none

    From Mathlib

    Discussion

    Ask a question or add context. Endorsements and structured flags are kept in the review panel above.

    Loading discussion…