theorem NNRat.smul_one_eq_cast (α : Type u_1) [DivisionSemiring α] (q : ℚ≥0) : q • 1 = ↑q

Alias of NNRat.smul_one_eq_coe.