mathlib3
0e8b06c0 - feat(ring_theory): `y ≠ 0` in a UFD has finitely many divisors

Commit

4 years ago

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

Author

Vierkantor

Committer

Vierkantor

Parents

9e8bac05

mathlib3 0e8b06c0 - feat(ring_theory): `y ≠ 0` in a UFD has finitely many divisors

mathlib3
0e8b06c0 - feat(ring_theory): `y ≠ 0` in a UFD has finitely many divisors