Commit 2023-03-30 13:14 d38f441e

View on Github →

feat: port RingTheory.Polynomial.Basic (#3067)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/Polynomial/Basic.lean

added def Ideal.degreeLe

added theorem Ideal.eq_zero_of_constant_mem_of_maximal

added theorem Ideal.isPrime_map_C_iff_isPrime

added theorem Ideal.isPrime_map_C_of_isPrime

added theorem Ideal.is_fg_degreeLe

added def Ideal.leadingCoeff

added def Ideal.leadingCoeffNth

added theorem Ideal.leadingCoeffNth_mono

added theorem Ideal.mem_leadingCoeff

added theorem Ideal.mem_leadingCoeffNth

added theorem Ideal.mem_leadingCoeffNth_zero

added theorem Ideal.mem_map_C_iff

added theorem Ideal.mem_ofPolynomial

added def Ideal.ofPolynomial

added theorem Ideal.polynomial_mem_ideal_of_coeff_mem_ideal

added theorem Ideal.polynomial_not_isField

added theorem MvPolynomial.isNoetherianRing_fin

added theorem MvPolynomial.isNoetherianRing_fin_0

added theorem MvPolynomial.ker_map

added theorem MvPolynomial.map_mvPolynomial_eq_eval₂

added theorem MvPolynomial.mem_ideal_of_coeff_mem_ideal

added theorem MvPolynomial.mem_map_C_iff

added theorem MvPolynomial.noZeroDivisors_fin

added theorem MvPolynomial.noZeroDivisors_of_finite

added theorem MvPolynomial.prime_C_iff

added theorem MvPolynomial.prime_rename_iff

added theorem Polynomial.Monic.geom_sum'

added theorem Polynomial.Monic.geom_sum

added theorem Polynomial.coeff_mem_frange

added theorem Polynomial.coeff_ofSubring

added theorem Polynomial.coeff_prod_mem_ideal_pow_tsub

added theorem Polynomial.coeff_restriction'

added theorem Polynomial.coeff_restriction

added theorem Polynomial.coeff_toSubring

added theorem Polynomial.coeff_to_subring'

added def Polynomial.degreeLe

added theorem Polynomial.degreeLe_eq_span_X_pow

added theorem Polynomial.degreeLe_mono

added def Polynomial.degreeLt

added def Polynomial.degreeLtEquiv

added theorem Polynomial.degreeLtEquiv_eq_zero_iff_eq_zero

added theorem Polynomial.degreeLt_eq_span_X_pow

added theorem Polynomial.degreeLt_mono

added theorem Polynomial.degree_restriction

added theorem Polynomial.degree_toSubring

added theorem Polynomial.disjoint_ker_aeval_of_coprime

added theorem Polynomial.eval_eq_sum_degreeLtEquiv

added theorem Polynomial.eval₂_restriction

added theorem Polynomial.exists_irreducible_of_degree_pos

added theorem Polynomial.exists_irreducible_of_natDegree_ne_zero

added theorem Polynomial.exists_irreducible_of_natDegree_pos

added def Polynomial.frange

added theorem Polynomial.frange_ofSubring

added theorem Polynomial.frange_one

added theorem Polynomial.frange_zero

added theorem Polynomial.geom_sum_X_comp_X_add_one_eq_sum

added theorem Polynomial.ker_mapRingHom

added theorem Polynomial.ker_modByMonicHom

added theorem Polynomial.linearIndependent_powers_iff_aeval

added theorem Polynomial.map_restriction

added theorem Polynomial.map_toSubring

added theorem Polynomial.mem_degreeLe

added theorem Polynomial.mem_degreeLt

added theorem Polynomial.mem_frange_iff

added theorem Polynomial.mem_ker_mod_by_monic

added theorem Polynomial.monic_geom_sum_X

added theorem Polynomial.monic_restriction

added theorem Polynomial.monic_toSubring

added theorem Polynomial.natDegree_restriction

added theorem Polynomial.natDegree_toSubring

added def Polynomial.ofSubring

added theorem Polynomial.prime_C_iff

added def Polynomial.restriction

added theorem Polynomial.restriction_one

added theorem Polynomial.restriction_zero

added theorem Polynomial.sup_aeval_range_eq_top_of_coprime

added theorem Polynomial.sup_ker_aeval_eq_ker_aeval_mul_of_coprime

added theorem Polynomial.sup_ker_aeval_le_ker_aeval_mul

added theorem Polynomial.support_restriction

added theorem Polynomial.support_toSubring

added def Polynomial.toSubring

added theorem Polynomial.toSubring_one

added theorem Polynomial.toSubring_zero