mathlib
11284f2f - feat(ring_theory): `y ≠ 0` in a UFD has finitely many divisors (#9034)

Commit

4 years ago

feat(ring_theory): `y ≠ 0` in a UFD has finitely many divisors (#9034) This implies ideals in a Dedekind domain are contained in only finitely many larger ideals.

Author

Vierkantor

Parents

86dd706c

mathlib 11284f2f - feat(ring_theory): `y ≠ 0` in a UFD has finitely many divisors (#9034)

mathlib
11284f2f - feat(ring_theory): `y ≠ 0` in a UFD has finitely many divisors (#9034)