Commit 2024-10-30 17:12 72cd7065

View on Github →

chore(RingTheory/PrincipalIdealDomain): PID implies Noetherian (#18382) Also, generalize IsPrincipal.generator to Semiring R and AddCommMonoid M

Estimated changes