Mathlib v3 is deprecated. Go to Mathlib v4

Theorem unique_has_one

Modification history

2021-08-16 16:19
src/algebra/group/units.lean
feat(algebra/big_operators/basic): prod_subsingleton (#8423)
Added unique_has_oneView on Github →