Commit 2024-05-21 08:06 70a13be1
View on Github →feat: Units and Associates of nonZeroDivisors (#12776)
This PR defines the following two group/monoid isomorphisms:
variable {α : Type*} [MonoidWithZero α]
def unitsNonZeroDivisorsEquiv : α⁰ˣ ≃* αˣ
def nonZeroDivisorsAssociatesEquiv : (Associates α)⁰ ≃* Associates α⁰