Commit 2023-03-13 12:48 f5400954

View on Github →

feat: Port Data.Polynomial.Lifts (#2835)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Data/Polynomial/Lifts.lean

added theorem Polynomial.C'_mem_lifts

added theorem Polynomial.base_mul_mem_lifts

added theorem Polynomial.c_mem_lifts

added theorem Polynomial.erase_mem_lifts

added def Polynomial.lifts

added def Polynomial.liftsRing

added theorem Polynomial.lifts_and_degree_eq_and_monic

added theorem Polynomial.lifts_and_natDegree_eq_and_monic

added theorem Polynomial.lifts_iff_coeff_lifts

added theorem Polynomial.lifts_iff_liftsRing

added theorem Polynomial.lifts_iff_ringHom_rangeS

added theorem Polynomial.lifts_iff_set_range

added def Polynomial.mapAlg

added theorem Polynomial.mapAlg_eq_map

added theorem Polynomial.mem_lifts

added theorem Polynomial.mem_lifts_and_degree_eq

added theorem Polynomial.mem_lifts_iff_mem_alg

added theorem Polynomial.monomial_mem_lifts

added theorem Polynomial.monomial_mem_lifts_and_degree_eq

added theorem Polynomial.smul_mem_lifts

added theorem Polynomial.x_mem_lifts

added theorem Polynomial.x_pow_mem_lifts