pith. machine review for the scientific record. sign in
def definition def or abbrev

music_admissible

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

formal statement (Lean)

  54noncomputable def music_admissible : AdmissibleRealization Music.strictMusicRealization := by

proof body

Definition body.

  55  refine ⟨?_, ?_, Or.inl ?_⟩
  56  · intro a b
  57    apply Classical.dec
  58  · exact RichDomainCosts.MusicRich.compose_assoc
  59  · -- compose one one = one for Music: 1 * 1 = 1
  60    show (⟨(1 : ℝ) * 1, _⟩ : Music.FrequencyRatio) = ⟨1, _⟩
  61    apply Subtype.ext; norm_num
  62

used by (2)

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

depends on (10)

Lean names referenced from this declaration's body.