Commit 2024-11-15 15:51 1124c33d

View on Github →

chore(Algebra/Polynomial): split Eval.lean into smaller files (#19036) This PR takes the rather large file Algebra/Polynomial/Eval.lean and splits it into the following smaller files:

Algebra/Polynomial/Eval/Defs.lean: definition of evaluation and bundled homs
Algebra/Polynomial/Eval/Algebra.lean: evaluating where the map is algebraMap
Algebra/Polynomial/Eval/Coeff.lean: eval and coeff
Algebra/Polynomial/Eval/Degree.lean: eval and degree
Algebra/Polynomial/Eval/Irreducible.lean: eval and Irreducible
Algebra/Polynomial/Eval/SMul.lean: eval and the module structure on Polynomial
Algebra/Polynomial/Eval/Subring.lean: eval into a subring

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/LinearRecurrence.lean

Modified Mathlib/Algebra/MvPolynomial/Polynomial.lean

Modified Mathlib/Algebra/Polynomial/AlgebraMap.lean

Modified Mathlib/Algebra/Polynomial/Degree/Lemmas.lean

Modified Mathlib/Algebra/Polynomial/DenomsClearable.lean

Modified Mathlib/Algebra/Polynomial/Derivative.lean

Created Mathlib/Algebra/Polynomial/Eval/Algebra.lean

added theorem Polynomial.eval₂_comp'

added theorem Polynomial.eval₂_mul'

added theorem Polynomial.eval₂_pow'

Created Mathlib/Algebra/Polynomial/Eval/Coeff.lean

added theorem Polynomial.IsRoot.map

added theorem Polynomial.IsRoot.of_map

added theorem Polynomial.coeff_map

added theorem Polynomial.coeff_zero_eq_eval_zero

added theorem Polynomial.evalRingHom_zero

added theorem Polynomial.eval_intCast_map

added theorem Polynomial.eval_natCast_map

added theorem Polynomial.eval_one_map

added theorem Polynomial.eval_zero_map

added theorem Polynomial.eval₂_C_X

added theorem Polynomial.eval₂_at_zero

added theorem Polynomial.eval₂_hom

added theorem Polynomial.eval₂_map

added theorem Polynomial.hom_eval₂

added theorem Polynomial.isRoot_map_iff

added theorem Polynomial.mapRingHom_comp

added theorem Polynomial.mapRingHom_id

added theorem Polynomial.map_id

added theorem Polynomial.map_injective

added theorem Polynomial.map_map

added theorem Polynomial.map_surjective

added def Polynomial.piEquiv

added theorem Polynomial.support_map_of_injective

added theorem Polynomial.support_map_subset

added theorem Polynomial.zero_isRoot_of_coeff_zero_eq_zero

Renamed Mathlib/Algebra/Polynomial/Eval.lean to Mathlib/Algebra/Polynomial/Eval/Defs.lean

deleted theorem Polynomial.IsRoot.map

deleted theorem Polynomial.IsRoot.of_map

deleted theorem Polynomial.Monic.irreducible_of_irreducible_map

deleted theorem Polynomial.coeff_comp_degree_mul_degree

deleted theorem Polynomial.coeff_map

deleted theorem Polynomial.coeff_zero_eq_eval_zero

deleted theorem Polynomial.degree_map_eq_of_leadingCoeff_ne_zero

deleted theorem Polynomial.degree_map_le

deleted theorem Polynomial.evalRingHom_zero

deleted theorem Polynomial.eval_eq_sum_range'

deleted theorem Polynomial.eval_eq_sum_range

deleted theorem Polynomial.eval_intCast_map

deleted theorem Polynomial.eval_monomial_one_add_sub

deleted theorem Polynomial.eval_natCast_map

deleted theorem Polynomial.eval_one_map

deleted theorem Polynomial.eval_smul

deleted theorem Polynomial.eval_zero_map

deleted theorem Polynomial.eval₂_C_X

deleted theorem Polynomial.eval₂_at_zero

deleted theorem Polynomial.eval₂_comp'

deleted theorem Polynomial.eval₂_comp

deleted theorem Polynomial.eval₂_eq_sum_range'

deleted theorem Polynomial.eval₂_eq_sum_range

deleted theorem Polynomial.eval₂_hom

deleted theorem Polynomial.eval₂_map

deleted theorem Polynomial.eval₂_mul'

deleted theorem Polynomial.eval₂_pow'

deleted theorem Polynomial.eval₂_smul

deleted theorem Polynomial.hom_eval₂

deleted theorem Polynomial.isRoot_map_iff

deleted theorem Polynomial.isUnit_of_isUnit_leadingCoeff_of_isUnit_map

deleted theorem Polynomial.iterate_comp_eval

deleted theorem Polynomial.iterate_comp_eval₂

deleted theorem Polynomial.leadingCoeff_map_of_leadingCoeff_ne_zero

deleted def Polynomial.leval

deleted def Polynomial.mapEquiv

deleted theorem Polynomial.mapRingHom_comp

deleted theorem Polynomial.mapRingHom_id

deleted theorem Polynomial.map_id

deleted theorem Polynomial.map_injective

deleted theorem Polynomial.map_map

deleted theorem Polynomial.map_monic_eq_zero_iff

deleted theorem Polynomial.map_monic_ne_zero

deleted theorem Polynomial.map_surjective

deleted theorem Polynomial.mem_map_range

deleted theorem Polynomial.mem_map_rangeS

deleted theorem Polynomial.natDegree_map_le

deleted theorem Polynomial.natDegree_map_of_leadingCoeff_ne_zero

deleted def Polynomial.piEquiv

deleted theorem Polynomial.smul_comp

deleted theorem Polynomial.support_map_of_injective

deleted theorem Polynomial.support_map_subset

deleted theorem Polynomial.zero_isRoot_of_coeff_zero_eq_zero

Created Mathlib/Algebra/Polynomial/Eval/Degree.lean

added theorem Polynomial.coeff_comp_degree_mul_degree

added theorem Polynomial.degree_map_eq_of_leadingCoeff_ne_zero

added theorem Polynomial.degree_map_le

added theorem Polynomial.eval_eq_sum_range'

added theorem Polynomial.eval_eq_sum_range

added theorem Polynomial.eval_monomial_one_add_sub

added theorem Polynomial.eval₂_comp

added theorem Polynomial.eval₂_eq_sum_range'

added theorem Polynomial.eval₂_eq_sum_range

added theorem Polynomial.isUnit_of_isUnit_leadingCoeff_of_isUnit_map

added theorem Polynomial.iterate_comp_eval

added theorem Polynomial.iterate_comp_eval₂

added theorem Polynomial.leadingCoeff_map_of_leadingCoeff_ne_zero

added def Polynomial.mapEquiv

added theorem Polynomial.map_monic_eq_zero_iff

added theorem Polynomial.map_monic_ne_zero

added theorem Polynomial.natDegree_map_le

added theorem Polynomial.natDegree_map_of_leadingCoeff_ne_zero

Created Mathlib/Algebra/Polynomial/Eval/Irreducible.lean

added theorem Polynomial.Monic.irreducible_of_irreducible_map

Created Mathlib/Algebra/Polynomial/Eval/SMul.lean

added theorem Polynomial.eval_smul

added theorem Polynomial.eval₂_smul

added def Polynomial.leval

added theorem Polynomial.smul_comp

Created Mathlib/Algebra/Polynomial/Eval/Subring.lean

added theorem Polynomial.mem_map_range

added theorem Polynomial.mem_map_rangeS

Modified Mathlib/Algebra/Polynomial/FieldDivision.lean

Modified Mathlib/Algebra/Polynomial/Lifts.lean

Modified Mathlib/Algebra/Polynomial/Reverse.lean

Modified Mathlib/Algebra/Polynomial/Smeval.lean

Modified Mathlib/Algebra/Polynomial/SumIteratedDerivative.lean

Modified Mathlib/Algebra/Polynomial/Taylor.lean

Modified Mathlib/Analysis/Asymptotics/SuperpolynomialDecay.lean

Modified Mathlib/Analysis/Polynomial/CauchyBound.lean

Modified Mathlib/Analysis/SpecialFunctions/PolynomialExp.lean

Modified Mathlib/Computability/TMComputable.lean

Modified Mathlib/FieldTheory/IsAlgClosed/AlgebraicClosure.lean

Modified Mathlib/LinearAlgebra/Matrix/Charpoly/Coeff.lean

Modified Mathlib/LinearAlgebra/SModEq.lean

Modified Mathlib/RingTheory/IntegralClosure/IsIntegral/Defs.lean

Modified Mathlib/RingTheory/Polynomial/Bernstein.lean

Modified Mathlib/RingTheory/Polynomial/IrreducibleRing.lean

Modified Mathlib/RingTheory/Polynomial/Pochhammer.lean

Modified Mathlib/RingTheory/Polynomial/Quotient.lean

Modified MathlibTest/RewriteSearch/Polynomial.lean