pith. machine review for the scientific record. sign in
theorem proved term proof

compose_left_id

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)

  62theorem compose_left_id (a : FrequencyRatio) :
  63    strictMusicRealization.compose strictMusicRealization.one a = a := by

proof body

Term-mode proof.

  64  show (⟨1 * a.1, _⟩ : FrequencyRatio) = a
  65  apply Subtype.ext
  66  simp
  67
  68end MusicRich
  69
  70/-! ## Biology -/
  71
  72namespace BiologyRich
  73
  74open Biology
  75

depends on (7)

Lean names referenced from this declaration's body.