Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-02-24 15:36 f9220866

View on Github →

feat(ring_theory/polynomial): more operations on polynomials (#679)

Estimated changes

Modified src/ring_theory/polynomial.lean

added theorem is_noetherian_ring_mv_polynomial_fin

added theorem is_noetherian_ring_mv_polynomial_of_fintype

added theorem polynomial.coeff_restriction'

added theorem polynomial.coeff_restriction

added theorem polynomial.coeff_to_subring'

added theorem polynomial.coeff_to_subring

added theorem polynomial.degree_restriction

added theorem polynomial.degree_to_subring

added theorem polynomial.eval₂_restriction

added theorem polynomial.frange_of_subring

added theorem polynomial.monic_restriction

added theorem polynomial.monic_to_subring

added theorem polynomial.nat_degree_restriction

added theorem polynomial.nat_degree_to_subring

added def polynomial.of_subring

added def polynomial.restriction

added theorem polynomial.restriction_one

added theorem polynomial.restriction_zero

added def polynomial.to_subring

added theorem polynomial.to_subring_one

added theorem polynomial.to_subring_zero