Mathlib v3 is deprecated. Go to Mathlib v4

Def mul_equiv.prod_units

Modification history

2022-01-05 23:45
src/algebra/group/prod.lean
chore(*): notation for `units` (#11236)
Modified mul_equiv.prod_unitsView on Github →
2021-01-05 20:33
src/algebra/group/prod.lean
fix(algebra/group/prod): fixes for #5563 (#5577) …
Added mul_equiv.prod_unitsView on Github →