[ add ] Definition, consequences, properties, structures, and bundles for Algebra.*s with the 'no zero divisors' property #2554
Description
Lifted from #2542 , but has arisen before in various scattered proposals to extend the Algebra hierarchy to include:
IntegralDomainEuclideanDomainUniqueFactorisationDomainPrincipalIdealDomain- ...
which is (probably) too big a project to identify as a single issue/PR?