Mathlib Changelog
v4
Changelog
About
Github
Commit
2024-12-10 16:18
28a2a670
View on Github →
feat: isomorphism between the non-divisors and units of a group with zero (
#19868
) From FLT
Estimated changes
Modified
Mathlib/Algebra/GroupWithZero/NonZeroDivisors.lean
modified
theorem
isUnit_of_mem_nonZeroDivisors
modified
theorem
mem_nonZeroDivisors_iff_ne_zero