mathlib4 icon indicating copy to clipboard operation
mathlib4 copied to clipboard

feat: two equiv involving `Associates` and `nonZeroDivisors`

Open xroblot opened this issue 1 year ago • 2 comments

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


Open in Gitpod

xroblot avatar May 08 '24 16:05 xroblot

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.

YaelDillies avatar May 19 '24 14:05 YaelDillies

Yeah, I agree with that. I'll change this one to WIP and the other one to awaiting-review.

xroblot avatar May 19 '24 15:05 xroblot