Commit 2023-10-03 19:47 b2540cf9

View on Github →

feat: add some Associated/Prime lemmas (#7465) From flt-regular.

Estimated changes

added theorem Prime.dvd_pow_iff_dvd
added theorem Associated.prod
added theorem isUnit_neg_one