Commit 2024-10-26 14:30 cc310263

RFC/chore(Algebra/GCDMonoid): should we un-@[simp] normalize_apply? (#18006) The lemma normalize_apply feels to me like it exposes the implementation detail that normalize is defined in terms of normUnit. I think the normalize function itself is much more familiar so it doesn't really seem like a simplification to insert normUnit instead. Indeed there are quite a few simp [-normalize_apply] in Mathlib. Moreover, there were some simp lemmas about normalize that had to be given higher priority since e.g. normalize (a * b) = normalize a * normalize b but normUnit (a * b) does not necessarily equal normUnit a * normUnit b. A few downstream fixes are needed where a @[simp] lemma is proved for normUnit and not for normalize, otherwise everything goes very smoothly.