abbrev definition def or abbrev

`Prime`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  36abbrev Prime (n : ℕ) : Prop := Nat.Prime n

proof body

Definition body.

used by (40)

From the project-wide theorem graph. These declarations reference this one in their body.

gamma_numerical_bounds in IndisputableMonolith.Constants.EulerMascheroni decl_use
BarrierCert in IndisputableMonolith.Gap45.RecognitionBarrier decl_use
beat_is_prime in IndisputableMonolith.Gap45.RecognitionBarrier decl_use
gapDiff_prime in IndisputableMonolith.Gap45.ShimmerFactor decl_use
shimmer_cert in IndisputableMonolith.Gap45.ShimmerFactor decl_use
ShimmerCert in IndisputableMonolith.Gap45.ShimmerFactor decl_use
shimmer_is_gap45_arithmetic in IndisputableMonolith.Gap45.ShimmerFactor decl_use
prime_unit_cost in IndisputableMonolith.Mathematics.GoldbachFromRS decl_use
congruence_offsets_unique in IndisputableMonolith.Mathematics.RamanujanBridge.CongruenceQ3Bridge decl_use
congruence_primes_are_three_smallest in IndisputableMonolith.Mathematics.RamanujanBridge.CongruenceQ3Bridge decl_use
IsCongruenceEligible in IndisputableMonolith.Mathematics.RamanujanBridge.CongruenceQ3Bridge decl_use
IsMockOrder in IndisputableMonolith.Mathematics.RamanujanBridge.CongruenceQ3Bridge decl_use
mock_orders_complete in IndisputableMonolith.Mathematics.RamanujanBridge.CongruenceQ3Bridge decl_use
no_cong_prime_between_3_5 in IndisputableMonolith.Mathematics.RamanujanBridge.CongruenceQ3Bridge decl_use
no_cong_prime_between_5_7 in IndisputableMonolith.Mathematics.RamanujanBridge.CongruenceQ3Bridge decl_use
no_cong_prime_between_7_11 in IndisputableMonolith.Mathematics.RamanujanBridge.CongruenceQ3Bridge decl_use
mock_orders_are_complete in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
mock_orders_are_odd_primes_lt_8 in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
mock_orders_exactly_odd_primes_lt_8 in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
odd_prime_lt_8_in_mock_orders in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
prime_closes_iff_two in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom decl_use
one103_is_prime in IndisputableMonolith.Mathematics.RamanujanBridge.RamanujanPiFactors decl_use
RamanujanPiCert in IndisputableMonolith.Mathematics.RamanujanBridge.RamanujanPiFactors decl_use
nthPrime in IndisputableMonolith.NavierStokes.RM2U.NonParasitism decl_use
nthPrime_prime in IndisputableMonolith.NavierStokes.RM2U.NonParasitism decl_use
pairwise_coprime_nthPrime in IndisputableMonolith.NavierStokes.RM2U.NonParasitism decl_use
cost_twisted_certificate in IndisputableMonolith.NumberTheory.CostTwistedLSeries decl_use
twistedCostSpectrumValue_pow in IndisputableMonolith.NumberTheory.CostTwistedLSeries decl_use
twistedCostSpectrumValue_prime in IndisputableMonolith.NumberTheory.CostTwistedLSeries decl_use
twistedPrimeCostSum in IndisputableMonolith.NumberTheory.CostTwistedLSeries decl_use

… and 10 more