Commit 2023-05-24 10:36 0123bf2a

View on Github →

feat: port RingTheory.AdjoinRoot (#4271)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RingTheory/AdjoinRoot.lean

added theorem AdjoinRoot.Minpoly.toAdjoin.apply_X

added theorem AdjoinRoot.Minpoly.toAdjoin.surjective

added def AdjoinRoot.Minpoly.toAdjoin

added theorem AdjoinRoot.Minpoly.toAdjoin_apply'

added def AdjoinRoot.Polynomial.quotQuotEquivComm

added theorem AdjoinRoot.Polynomial.quotQuotEquivComm_mk

added theorem AdjoinRoot.Polynomial.quotQuotEquivComm_symm_mk_mk

added theorem AdjoinRoot.adjoinRoot_eq_top

added theorem AdjoinRoot.aeval_algHom_eq_zero

added theorem AdjoinRoot.aeval_eq

added theorem AdjoinRoot.algHom_ext

added theorem AdjoinRoot.algHom_subsingleton

added theorem AdjoinRoot.algebraMap_eq'

added theorem AdjoinRoot.algebraMap_eq

added theorem AdjoinRoot.coe_injective'

added theorem AdjoinRoot.coe_injective

added theorem AdjoinRoot.coe_liftHom

added def AdjoinRoot.equiv'

added theorem AdjoinRoot.equiv'_symm_toAlgHom

added theorem AdjoinRoot.equiv'_toAlgHom

added def AdjoinRoot.equiv

added theorem AdjoinRoot.eval₂_root

added theorem AdjoinRoot.finitePresentation

added theorem AdjoinRoot.finiteType

added theorem AdjoinRoot.induction_on

added theorem AdjoinRoot.isAlgebraic_root

added theorem AdjoinRoot.isDomain_of_prime

added theorem AdjoinRoot.isIntegral_root'

added theorem AdjoinRoot.isIntegral_root

added theorem AdjoinRoot.isRoot_root

added def AdjoinRoot.lift

added def AdjoinRoot.liftHom

added theorem AdjoinRoot.liftHom_eq_algHom

added theorem AdjoinRoot.liftHom_mk

added theorem AdjoinRoot.liftHom_of

added theorem AdjoinRoot.liftHom_root

added theorem AdjoinRoot.lift_comp_of

added theorem AdjoinRoot.lift_mk

added theorem AdjoinRoot.lift_of

added theorem AdjoinRoot.lift_root

added theorem AdjoinRoot.minpoly_powerBasis_gen

added theorem AdjoinRoot.minpoly_powerBasis_gen_of_monic

added theorem AdjoinRoot.minpoly_root

added def AdjoinRoot.mk

added theorem AdjoinRoot.mk_C

added theorem AdjoinRoot.mk_X

added theorem AdjoinRoot.mk_eq_mk

added theorem AdjoinRoot.mk_eq_zero

added theorem AdjoinRoot.mk_leftInverse

added theorem AdjoinRoot.mk_ne_zero_of_degree_lt

added theorem AdjoinRoot.mk_ne_zero_of_natDegree_lt

added theorem AdjoinRoot.mk_self

added theorem AdjoinRoot.mk_surjective

added def AdjoinRoot.modByMonicHom

added theorem AdjoinRoot.modByMonicHom_mk

added theorem AdjoinRoot.mul_div_root_cancel

added theorem AdjoinRoot.noZeroSMulDivisors_of_prime_of_degree_ne_zero

added theorem AdjoinRoot.of.injective_of_degree_ne_zero

added def AdjoinRoot.of

added def AdjoinRoot.powerBasis'

added def AdjoinRoot.powerBasis

added def AdjoinRoot.powerBasisAux'

added theorem AdjoinRoot.powerBasisAux'_repr_apply_to_fun

added theorem AdjoinRoot.powerBasisAux'_repr_symm_apply

added def AdjoinRoot.powerBasisAux

added def AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot

added theorem AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of

added theorem AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk

added theorem AdjoinRoot.quotEquivQuotMap_apply_mk

added theorem AdjoinRoot.quotEquivQuotMap_symm_apply_mk

added def AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk

added theorem AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk

added theorem AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk

added def AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk

added theorem AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_mk

added theorem AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_symm_mk

added def AdjoinRoot.root

added theorem AdjoinRoot.root_is_inv

added theorem AdjoinRoot.smul_mk

added theorem AdjoinRoot.smul_of

added def AdjoinRoot

added theorem PowerBasis.quotientEquivQuotientMinpolyMap_apply_mk

added theorem PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk