mathlib3
f24f0161 - almost finished showing `Mon_ AddCommGroup \iso Ring`

Commit

3 years ago

almost finished showing `Mon_ AddCommGroup \iso Ring`

References

#17006 - feat(category_theory/*): Monoid objects in Abelian group are rings

Author

jjaassoonn

jjaassoonn

Parents

Loading