Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-03-24 10:12 eabc6192

View on Github →

feat(ring_theory/polynomial): mv_polynomial over UFD is UFD (#12866)

Estimated changes

Modified docs/overview.yaml

Modified docs/undergrad.yaml

Modified src/algebra/associated.lean

added theorem comap_prime

added theorem mul_equiv.prime_iff

Modified src/algebra/divisibility.lean

added theorem map_dvd

modified theorem monoid_hom.map_dvd

modified theorem mul_hom.map_dvd

Modified src/algebra/ring/basic.lean

modified theorem ring_hom.map_dvd

Modified src/data/mv_polynomial/rename.lean

added theorem mv_polynomial.exists_finset_rename₂

added def mv_polynomial.kill_compl

added theorem mv_polynomial.kill_compl_comp_rename

added theorem mv_polynomial.kill_compl_rename_app

Modified src/ring_theory/polynomial/basic.lean

added theorem mv_polynomial.prime_C_iff

added theorem mv_polynomial.prime_rename_iff

added theorem polynomial.prime_C_iff

Modified src/ring_theory/unique_factorization_domain.lean

added theorem mul_equiv.unique_factorization_monoid

added theorem mul_equiv.unique_factorization_monoid_iff