`cert`

definition

show as: view math explainer →

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

open explainer

Read the cached plain-language explainer.

open lean source

IndisputableMonolith.Ethnomusicology.ScaleCountFromConfigDim on GitHub at line 61.

browse module

All declarations in this module, on Recognition.

explainer page

A cached Ask Recognition explainer exists for this declaration.

open explainer

depends on

formal source

  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.