Mathlib v3 is deprecated. Go to Mathlib v4

Def prod.units

Modification history

2021-01-05 20:33
src/algebra/group/prod.lean
fix(algebra/group/prod): fixes for #5563 (#5577) …
Deleted prod.unitsView on Github →
2021-01-02 15:05
src/algebra/group/prod.lean
feat(algebra/group/prod) Units of a product monoid (#5563) …
Added prod.unitsView on Github →