Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Commit
2021-08-13 18:20
7f5d5b9a
View on Github →
feat(ring_theory): ideals in a Dedekind domain have unique factorization (
#8530
)
Estimated changes
Modified
src/ring_theory/dedekind_domain.lean
deleted
theorem
fractional_ideal.mul_inv_cancel
added
theorem
ideal.dvd_iff_le
added
theorem
ideal.dvd_not_unit_iff_lt
Modified
src/ring_theory/ideal/operations.lean
added
theorem
ideal.is_unit_iff
added
theorem
ideal.le_of_dvd