Cost.FixedPoint
IndisputableMonolith.Cost.FixedPoint
No prose has been written for this declaration yet. The Lean source and graph data below render without it.
generate prose now
Lean names referenced from this declaration's body.
IndisputableMonolith.Constants
phi_is_cost_fixed_point