mathlib4
mathlib4 copied to clipboard
feat: two equiv involving `Associates` and `nonZeroDivisors`
This PR contains mainly the following two equivalences:
def nonZeroDivisorsUnitsEquiv (α : Type*) [MonoidWithZero α] :
(α⁰)ˣ ≃* αˣ
and
def AssociatesNonZeroDivisorsMulEquiv (α : Type*) [CommMonoidWithZero α] :
Associates α⁰ ≃* (Associates α)⁰
These results require to import Mathlib.Algebra.Associated and Mathlib.Algebra.GroupWithZero.NonZeroDivisors. Since there are no (low enough) file that imports these two files, this PR makes a directory Mathlib/Algebra/GroupWithZero/NonZeroDivisors, move the file Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean to Mathlib/Algebra/GroupWithZero/NonZeroDivisors/Basic.lean and put the new results in a file Mathlib/Algebra/GroupWithZero/NonZeroDivisors/Associates.lean.
This explains why so many files are touched by this PR.
Another (better?) solution would be to add the import Mathlib.Algebra.Associated to Mathlib.Algebra.GroupWithZero.NonZeroDivisors and put the new results in this file... see #12776
Given that Algebra.Associated is pretty low-level (and will be even more so very soon thanks to @Ruben-VandeVelde and I) and that in contrast Algebra.GroupWithZero.NonZeroDivisors is a mess (why is it under GroupWithZero if it imports rings?), I prefer #12776 over this PR.
Yeah, I agree with that. I'll change this one to WIP and the other one to awaiting-review.