`ScaleCountCert`

definition

show as: view math explainer →

module: IndisputableMonolith.Ethnomusicology.ScaleCountFromConfigDim
domain: Ethnomusicology
line: 56 · github
papers citing: none yet

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Ethnomusicology.ScaleCountFromConfigDim on GitHub at line 56.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

used by

formal source

  53theorem chromatic_pos : 0 < chromaticCount := by
  54  unfold chromaticCount; norm_num
  55
  56structure ScaleCountCert where
  57  scale_count : canonicalScaleCount = 5
  58  diatonic_eq : diatonicCount = pentatonicCount + 2
  59  chromatic_pos : 0 < chromaticCount
  60
  61noncomputable def cert : ScaleCountCert where
  62  scale_count := canonicalScaleCount_eq
  63  diatonic_eq := diatonic_eq_pentatonic_plus_two
  64  chromatic_pos := chromatic_pos
  65
  66theorem cert_inhabited : Nonempty ScaleCountCert := ⟨cert⟩
  67
  68end
  69end ScaleCountFromConfigDim
  70end Ethnomusicology
  71end IndisputableMonolith

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.