Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-01-02 15:05 e142c825

View on Github →

feat(algebra/group/prod) Units of a product monoid (#5563) Just a simple seemingly missing def

Estimated changes

added def prod.units