def definition def or abbrev

`tuningRankingCert`

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

formal statement (Lean)

  91def tuningRankingCert : TuningRankingCert where
  92  ji_zero := jiCost_zero

proof body

Definition body.

  93  tet_positive := tetStep_jcost_pos
  94  ji_beats_tet := ji_beats_tet
  95
  96end
  97end TuningSystemJCostRanking
  98end MusicTheory
  99end IndisputableMonolith

depends on (4)

Lean names referenced from this declaration's body.

ji_beats_tet in IndisputableMonolith.MusicTheory.TuningSystemJCostRanking decl_use
jiCost_zero in IndisputableMonolith.MusicTheory.TuningSystemJCostRanking decl_use
tetStep_jcost_pos in IndisputableMonolith.MusicTheory.TuningSystemJCostRanking decl_use
TuningRankingCert in IndisputableMonolith.MusicTheory.TuningSystemJCostRanking decl_use