Commit 2024-01-14 12:14 65ced9a7

View on Github →

feat: isUnit_iff_eq_one (#9706) From flt-regular. Also move the related units_eq_one nearby.

Estimated changes

deleted theorem units_eq_one
added theorem isUnit_iff_eq_one
added theorem units_eq_one