Definition semitonesPitchRatio (semitones : R) : R :=
  Rpower 2.0 (Rdiv semitones 12.0).
