Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-01-30 09:49 afa535e7

View on Github →

feat(ring_theory/polynomial): hilbert basis theorem

Estimated changes

Created src/ring_theory/polynomial.lean

added def ideal.degree_le

added theorem ideal.is_fg_degree_le

added def ideal.leading_coeff

added def ideal.leading_coeff_nth

added theorem ideal.leading_coeff_nth_mono

added theorem ideal.mem_leading_coeff

added theorem ideal.mem_leading_coeff_nth

added theorem ideal.mem_leading_coeff_nth_zero

added theorem ideal.mem_of_polynomial

added def ideal.of_polynomial

added theorem is_noetherian_ring_polynomial

added def polynomial.degree_le

added theorem polynomial.degree_le_eq_span_X_pow

added theorem polynomial.degree_le_mono

added theorem polynomial.mem_degree_le