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)
25@[simp] def ofInt (z : ℤ) : Rung := (z : ℚ)
proof body
Definition body.
26
27/-- The quarter‑ladder embedding: `k ↦ k/4`. -/
used by (6)
From the project-wide theorem graph. These declarations reference this one in their body.
-
UnitsKGateCert
in IndisputableMonolith.Certificates.UnitsKGate
decl_use
-
res_nu3
in IndisputableMonolith.Physics.NeutrinoSector
decl_use
-
ofInt
in IndisputableMonolith.QFT.SpinStatistics
decl_use
-
one
in IndisputableMonolith.QFT.SpinStatistics
decl_use
-
two
in IndisputableMonolith.QFT.SpinStatistics
decl_use
-
zero
in IndisputableMonolith.QFT.SpinStatistics
decl_use
depends on (3)
Lean names referenced from this declaration's body.
-
ofInt
in IndisputableMonolith.QFT.SpinStatistics
decl_use
-
quarter
in IndisputableMonolith.Support.RungFractions
decl_use
-
Rung
in IndisputableMonolith.Support.RungFractions
decl_use