Definition 2.9.2.  Let F be a field, b ∈ F, a ∈ F×. For x ∈ F, we define:
b∕a = x  :⇔  b = x ⋅ a
Well-definedness.  No proof.