No prose has been written for this declaration yet. The Lean source and graph data below render
without it.
generate prose now
formal statement (Lean)
66def prev (p : Phase) : Phase := p - 1
proof body
Definition body.
67
used by (7)
From the project-wide theorem graph. These declarations reference this one in their body.
-
phiPow
in IndisputableMonolith.Algebra.PhiRing
decl_use
-
ballFS
in IndisputableMonolith.Causality.ConeBound
decl_use
-
card_ballFS_succ_le
in IndisputableMonolith.Causality.ConeBound
decl_use
-
normalizedRadius
in IndisputableMonolith.Chemistry.AtomicRadii
decl_use
-
run
in IndisputableMonolith.LedgerPostingAdjacency
decl_use
-
next_prev
in IndisputableMonolith.RRF.Hypotheses.EightTick
decl_use
-
prev_next
in IndisputableMonolith.RRF.Hypotheses.EightTick
decl_use
depends on (2)
Lean names referenced from this declaration's body.
-
Phase
in IndisputableMonolith.Information.ChurchTuringPhysicsStructure
decl_use
-
Phase
in IndisputableMonolith.RRF.Hypotheses.EightTick
decl_use