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)
18abbrev FrequencyRatio := {x : ℝ // 0 < x}
proof body
Definition body.
19
used by (13)
From the project-wide theorem graph. These declarations reference this one in their body.
-
music_admissible
in IndisputableMonolith.Foundation.UniversalForcing.AdmissibleClass
decl_use
-
octave
in IndisputableMonolith.Foundation.UniversalForcing.Strict.Music
decl_use
-
perfectFifth
in IndisputableMonolith.Foundation.UniversalForcing.Strict.Music
decl_use
-
perfectFourth
in IndisputableMonolith.Foundation.UniversalForcing.Strict.Music
decl_use
-
ratioCost
in IndisputableMonolith.Foundation.UniversalForcing.Strict.Music
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
-
compose_assoc
in IndisputableMonolith.Foundation.UniversalForcing.Strict.RichDomainCosts
decl_use
-
compose_left_id
in IndisputableMonolith.Foundation.UniversalForcing.Strict.RichDomainCosts
decl_use
-
ratioCost_decidable
in IndisputableMonolith.Foundation.UniversalForcing.Strict.RichDomainCosts
decl_use
-
ratioCost_zero_iff
in IndisputableMonolith.Foundation.UniversalForcing.Strict.RichDomainCosts
decl_use
-
RichDomainCostsCert
in IndisputableMonolith.Foundation.UniversalForcing.Strict.RichDomainCosts
decl_use