theorem proved term proof

`octave_eq_8`

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

formal statement (Lean)

  59theorem octave_eq_8 : octave = 8 := by

Term-mode proof.

  60  unfold octave D
  61  norm_num
  62
  63/-- D equals F₄ -/

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

Lean names referenced from this declaration's body.

octave in IndisputableMonolith.Aesthetics.MusicalScale decl_use
octave in IndisputableMonolith.Constants decl_use
octave in IndisputableMonolith.Foundation.UniversalForcing.Strict.Music decl_use
octave in IndisputableMonolith.Masses.CoherenceExponent decl_use
octave in IndisputableMonolith.MusicTheory.HarmonicModes decl_use