module module

`IndisputableMonolith.Musicology.ModalPreferenceFromPhi`

show as: view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (16)

inductive GreekMode L43
def costRank L57
def all L67
theorem all_length L70
theorem all_nodup L73
theorem ionian_lowest L76
theorem aeolian_second L79
theorem locrian_highest L82
theorem ionian_aeolian_dominant L85
theorem locrian_uniquely_worst L90
def majorThirdReference L102
theorem majorThirdReference_pos L107
theorem majorThirdReference_below_phi L110
structure ModalPreferenceCert L118
def modalPreferenceCert L129
theorem musicology_one_statement L141