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 res_charm : ℚ := res_bottom - step_bottom_charm
used by (8)
From the project-wide theorem graph. These declarations reference this one in their body.
depends on (4)
Lean names referenced from this declaration's body.
-
step_bottom_charm
in IndisputableMonolith.Physics.MixingGeometry
decl_use
-
res_bottom
in IndisputableMonolith.Physics.QuarkMasses
decl_use
-
res_bottom
in IndisputableMonolith.RRF.Physics.QuarkMasses
decl_use
-
res_charm
in IndisputableMonolith.RRF.Physics.QuarkMasses
decl_use