Mathlib Changelog
v3
Changelog
About
Github
Mathlib v3 is deprecated.
Go to Mathlib v4
Theorem
unique_factorization_monoid.le_multiplicity_iff_replicate_le_normalized_factors
Modification history
2023-05-04 13:44
src/ring_theory/unique_factorization_domain.lean
feat(ring_theory/localization/away) : Add `num_denom` section (#18830) …
Modified
unique_factorization_monoid.le_multiplicity_iff_replicate_le_normalized_factors
View on Github →
2023-01-15 06:15
src/ring_theory/unique_factorization_domain.lean
refactor(*): define `list.replicate` and migrate to it (#18127) …
Added
unique_factorization_monoid.le_multiplicity_iff_replicate_le_normalized_factors
View on Github →