Documentation

LeanAPAP.Mathlib.Algebra.Order.Field.Basic

source
@[simp]
theorem NNRat.cast_pos {α : Type u_1} [LinearOrderedSemifield α] {q : ℚ≥0} :
0 < ↑q ↔ 0 < q