Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2022-07-17 19:11
f19c6153
View on Github →
feat(algebra/group/with_one): units of a group with zero is isomorphic to the group (
#15403
)
Estimated changes
Modified
src/algebra/group/with_one.lean
added
theorem
with_one.coe_unone
added
def
with_one.unone
added
theorem
with_one.unone_coe
added
def
with_zero.units_with_zero_equiv