doc: clarify the scope of field_simp (leanprover-community#39869)

The term semi-field is sufficiently non-standard that it has led to confusion whether e.g. `NNReal` is supported by field_simp: it is (as it is a semifield). Let's clarify the doc-string.

Inspired by discussions at the ICERM workshop "Techniques and Tools for the Formalization of Analysis".

Author: grunweg

Mathlib/Tactic/FieldSimp.lean

@@ -665,10 +665,10 @@ def parseDischarger (d : Option (TSyntax ``discharger)) (args : Option (TSyntax
     | _ => throwError "could not parse the provided discharger {d}"
 
 /--
-`field_simp` normalizes expressions in (semi-)fields by rewriting them to a common denominator,
-i.e. to reduce them to expressions of the form `n / d` where neither `n` nor `d` contains any
-division symbol. The `field_simp` tactic will also clear denominators in field *(in)equalities*, by
-cross-multiplying.
+`field_simp` normalizes expressions in (semi-)fields (i.e., does not require additive inverses)
+by rewriting them to a common denominator, i.e. to reduce them to expressions of the form `n / d`
+where neither `n` nor `d` contains any division symbol. The `field_simp` tactic will also clear
+denominators in field *(in)equalities*, by cross-multiplying.
 
 A very common pattern is `field_simp; ring` (clear denominators, then the resulting goal is
 solvable by the axioms of a commutative ring). The finishing tactic `field` is a shorthand for this