mathlib

b30d648a - feat(algebra/gcd_monoid): normalization and gcd are subsingletons given unique units (#17149)

feat(algebra/gcd_monoid): normalization and gcd are subsingletons given unique units (#17149) This PR answers a question raised in #17100 by proving that a monoid `α` with unique units (e.g. `ℕ` or `ideal R`) has a unique value for `normalization_monoid α`, and `gcd_monoid α` and `normalized_gcd_monoid α` are subsingletons. Co-authored-by: Anne Baanen <Vierkantor@users.noreply.github.com> Co-authored-by: Junyan Xu <junyanxu.math@gmail.com>