adding items to fixAbbreviation in to_additive

Stream: mathlib4

[Pieter Cuijpers]

I'm adding Quantale definitions, which are based on Semigroup, so it makes sense to use to_additive and get both the Add and Mul variants.

Different kinds of Quantales are "Commutative", "Integral", "Idempotent" and "Unital".
For Commutative we have the standard abbreviation Comm, and for Unital we have the standard Zero or One depending on whether we are dealing with Add or Mul.

I would like to add Idem for Idempotent, and Integral for Integral to the fixAbbreviation definition in ToAdditive.Frontend, but cannot judge the consequences of such a change. Any objections or thoughts what to keep in mind here?

[Eric Wieser]

This change sounds simple enough that it might be easiest to judge the consequence by just making the PR and seeing what breaks

[Jireh Loreaux]

@Eric Wieser #17289. Please see if you agree with my assessment.