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
chore(RingTheory/PrincipalIdealDomain): PID implies Noetherian (#18382)
Also, generalize IsPrincipal.generator
to Semiring R
and AddCommMonoid M