mathlib

2d30ffcf - feat(algebra/gcd_monoid): `simp` lemmas for `associated (normalize x) y` (#16249)

feat(algebra/gcd_monoid): `simp` lemmas for `associated (normalize x) y` (#16249) The lemmas in `gcd_monoid` package `associated_normalize` and `normalize_associated` into a form suitable for `simp`. Useful e.g. for working with `normalized_factors`. The lemmas in `associated` are the `simp`-normal forms of the `normalize` lemmas, since `normalize x` is not itself in `simp`-normal form.