def definition def or abbrev

`majorThird`

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

formal statement (Lean)

  55def majorThird : ℝ := 2 ^ (4 / 12 : ℝ)

Definition body.

  56
  57/-- Just major third: 5/4 = 1.25. -/

From the project-wide theorem graph. These declarations reference this one in their body.

third_quality in IndisputableMonolith.Aesthetics.MusicalScale decl_use
consonance_hierarchy in IndisputableMonolith.MusicTheory.Consonance decl_use
extended_ratio_cost_hierarchy in IndisputableMonolith.MusicTheory.Consonance decl_use
hierarchy_majorThird_lt_fourth in IndisputableMonolith.MusicTheory.Consonance decl_use
hierarchy_minorThird_lt_majorThird in IndisputableMonolith.MusicTheory.Consonance decl_use
jcost_majorThird in IndisputableMonolith.MusicTheory.Consonance decl_use
majorThird in IndisputableMonolith.MusicTheory.HarmonicModes decl_use
majorThird_eq_superparticular in IndisputableMonolith.MusicTheory.HarmonicModes decl_use
majorThirdInterval in IndisputableMonolith.MusicTheory.HarmonicModes decl_use
majorThird_jcost in IndisputableMonolith.MusicTheory.HarmonicModes decl_use
majorThird_pos in IndisputableMonolith.MusicTheory.HarmonicModes decl_use
major_is_positive in IndisputableMonolith.MusicTheory.Valence decl_use
major_skew_gt_minor_skew in IndisputableMonolith.MusicTheory.Valence decl_use
majorThird in IndisputableMonolith.MusicTheory.Valence decl_use
major_third_skew in IndisputableMonolith.MusicTheory.Valence decl_use
major_third_skew_pos in IndisputableMonolith.MusicTheory.Valence decl_use
valence_difference in IndisputableMonolith.MusicTheory.Valence decl_use
valence_difference_one_twelfth in IndisputableMonolith.MusicTheory.Valence decl_use

Lean names referenced from this declaration's body.