Partial division. It is defined when the second argument is invertible, and unlike the division operator in division_ring it is not totalized at zero.