Adjoining a zero/one to semigroups and related algebraic structures

In this file we provide a basic inequality result when adding a zero to the multiplicative group of integers.

theorem Multiplicative.ofAdd_neg_one_lt_one : ↑(Multiplicative.ofAdd (-1)) < 1

https://github.com/mariainesdff/local_fields_journal/blob/0b408ff3af36e18f991f9d4cb87be3603cfc3fc3/src/for_mathlib/with_zero.lean#L129