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)
20noncomputable def ratioCost (a b : FrequencyRatio) : Nat :=
proof body
Definition body.
21 if a = b then 0 else 1
22
used by (8)
From the project-wide theorem graph. These declarations reference this one in their body.
-
ratioCost
in IndisputableMonolith.Foundation.LogicAsFunctionalEquation.PositiveRatioForcing
decl_use
-
ratioCost_eq_derivedCost
in IndisputableMonolith.Foundation.LogicAsFunctionalEquation.PositiveRatioForcing
decl_use
-
scale_free_comparison_factors_through_ratio
in IndisputableMonolith.Foundation.LogicAsFunctionalEquation.PositiveRatioForcing
decl_use
-
ratioCost_self
in IndisputableMonolith.Foundation.UniversalForcing.Strict.Music
decl_use
-
ratioCost_symm
in IndisputableMonolith.Foundation.UniversalForcing.Strict.Music
decl_use
-
strictMusicRealization
in IndisputableMonolith.Foundation.UniversalForcing.Strict.Music
decl_use
-
ratioCost_zero_iff
in IndisputableMonolith.Foundation.UniversalForcing.Strict.RichDomainCosts
decl_use
-
RichDomainCostsCert
in IndisputableMonolith.Foundation.UniversalForcing.Strict.RichDomainCosts
decl_use
depends on (2)
Lean names referenced from this declaration's body.
-
ratioCost
in IndisputableMonolith.Foundation.LogicAsFunctionalEquation.PositiveRatioForcing
decl_use
-
FrequencyRatio
in IndisputableMonolith.Foundation.UniversalForcing.Strict.Music
decl_use