Commit 2020-10-29 19:28 78811e0a

View on Github →

feat(ring_theory/unique_factorization_domain): unique_factorization_monoid structure on polynomials over ufd (#4774) Provides the unique_factorization_monoid structure on polynomials over a UFD

Estimated changes

Modified docs/overview.yaml

Modified docs/undergrad.yaml

Modified src/ring_theory/polynomial/basic.lean

modified theorem polynomial.exists_irreducible_of_degree_pos

modified theorem polynomial.exists_irreducible_of_nat_degree_ne_zero

modified theorem polynomial.exists_irreducible_of_nat_degree_pos

Modified src/ring_theory/polynomial/content.lean

Modified src/ring_theory/unique_factorization_domain.lean