∀ {α : Type u_1} [inst : Lean.Grind.Field α] {a b : ℚ},
  ↑a.den ≠ 0 →
    ↑b.num ≠ 0 →
      Lean.Grind.Field.NormNum.ofRat (a / b) = Lean.Grind.Field.NormNum.ofRat a / Lean.Grind.Field.NormNum.ofRat b