AdjoinRoot

📁 Source: Mathlib/RingTheory/AdjoinRoot.lean

Statistics

Metric	Count
Definitions toAdjoin, quotQuotEquivComm, algEquivOfAssociated, algEquivOfEq, algHomOfDvd, equiv, equiv', hasCoeT, instAlgebra, instCommRing, instDecidableEq, instDistribMulActionOfIsScalarTower, instDistribSMulOfIsScalarTower, instField, instGroupWithZero, instInhabited, instSMulAdjoinRoot, liftAlgHom, liftHom, map, mapAlgEquiv, mapAlgHom, mapRingEquiv, mk, mkₐ, modByMonicHom, of, ofAlgHom, powerBasis, powerBasis', powerBasisAux, powerBasisAux', quotAdjoinRootEquivQuotPolynomialQuot, quotEquivQuotMap, quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk, quotMapOfEquivQuotMapCMapSpanMk, root, quotientEquivQuotientMinpolyMap	38
Theorems coe_toAdjoin, coe_toAdjoin_mk_X, surjective, quotQuotEquivComm_mk, quotQuotEquivComm_symm_mk_mk, adjoinRoot_eq_top, aeval_algHom_eq_zero, aeval_eq, aeval_eq_of_algebra, algEquivOfAssociated_apply_root, algEquivOfAssociated_root, algEquivOfAssociated_symm, algEquivOfAssociated_toAlgHom, algEquivOfEq_apply_root, algEquivOfEq_root, algEquivOfEq_symm, algEquivOfEq_toAlgHom, algHomOfDvd_apply_root, algHomOfDvd_root, algHom_ext, algHom_ext', algHom_ext'_iff, algHom_ext_iff, algHom_subsingleton, algebraMap_eq, algebraMap_eq', coe_algEquivOfAssociated, coe_algEquivOfEq, coe_algHomOfDvd, coe_injective, coe_injective', coe_liftAlgHom, coe_liftHom, coe_mapAlgEquiv, coe_mapAlgHom, coe_mapRingEquiv, coe_mkₐ, coe_ofAlgHom, equiv'_apply, equiv'_symm_apply, equiv'_symm_toAlgHom, equiv'_toAlgHom, eval₂_root, finitePresentation, finiteType, induction_on, instIsNoetherianRing, instIsScalarTower, instSMulCommClass, isAlgebraic_root, isDomain_of_prime, isIntegral_root, isIntegral_root', isRoot_root, isScalarTower_right, liftAlgHom_eq_algHom, liftAlgHom_mk, liftAlgHom_of, liftAlgHom_root, liftHom_eq_algHom, liftHom_mk, liftHom_of, liftHom_root, lift_comp_of, lift_mk, lift_of, lift_root, mapAlgHom_comp_mapAlghom, map_comp_map, map_of, map_root, minpoly_powerBasis_gen, minpoly_powerBasis_gen_of_monic, minpoly_root, mk_C, mk_X, mk_eq_mk, mk_eq_zero, mk_leftInverse, mk_ne_zero_of_degree_lt, mk_ne_zero_of_natDegree_lt, mk_self, mk_surjective, mkₐ_toRingHom, modByMonicHom_mk, mul_div_root_cancel, noZeroSMulDivisors_of_prime_of_degree_ne_zero, nontrivial, injective_of_degree_ne_zero, powerBasis'_dim, powerBasis'_gen, powerBasisAux'_repr_apply_to_fun, powerBasisAux'_repr_symm_apply, powerBasis_dim, powerBasis_gen, quotAdjoinRootEquivQuotPolynomialQuot_mk_of, quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk, quotEquivQuotMap_apply, quotEquivQuotMap_apply_mk, quotEquivQuotMap_symm_apply, quotEquivQuotMap_symm_apply_mk, quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk, quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk, quotMapOfEquivQuotMapCMapSpanMk_mk, quotMapOfEquivQuotMapCMapSpanMk_symm_mk, ringHom_ext, ringHom_ext_iff, root_isInv, smul_mk, smul_of, span_maximal_of_irreducible, symm_mapAlgEquiv, symm_mapRingEquiv, toRingHom_liftAlgHom, toRingHom_ofAlgHom, exists_dvd_monic_irreducible_of_isIntegral, exists_splits_map, finite_adjoinRoot, finite_quotient, free_adjoinRoot, free_quotient, quotientEquivQuotientMinpolyMap_apply, quotientEquivQuotientMinpolyMap_apply_mk, quotientEquivQuotientMinpolyMap_symm_apply, quotientEquivQuotientMinpolyMap_symm_apply_mk, finrank_quotient_span_eq_natDegree	126
Total	164

AdjoinRoot

Definitions

Name	Category	Theorems
algEquivOfAssociated 📖	CompOp	5 math math: algEquivOfAssociated_apply_root, algEquivOfAssociated_root, algEquivOfAssociated_toAlgHom, algEquivOfAssociated_symm, coe_algEquivOfAssociated
algEquivOfEq 📖	CompOp	5 math math: algEquivOfEq_root, algEquivOfEq_apply_root, coe_algEquivOfEq, algEquivOfEq_symm, algEquivOfEq_toAlgHom
algHomOfDvd 📖	CompOp	7 math math: algHomOfDvd_root, algEquivOfAssociated_toAlgHom, coe_algEquivOfEq, coe_algHomOfDvd, algEquivOfEq_toAlgHom, algHomOfDvd_apply_root, coe_algEquivOfAssociated
equiv 📖	CompOp	—
equiv' 📖	CompOp	6 math math: PowerBasis.quotientEquivQuotientMinpolyMap_apply, equiv'_symm_toAlgHom, equiv'_toAlgHom, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, equiv'_symm_apply, equiv'_apply
hasCoeT 📖	CompOp	—
instAlgebra 📖	CompOp	95 math math: algEquivOfAssociated_apply_root, minpoly.ToAdjoin.injective, isAdjoinRoot_root_eq_root, AlgEquiv.coe_adjoinSingletonEquivAdjoinRootMinpoly_symm, minpoly_root, autAdjoinRootXPowSubCEquiv_root, IntermediateField.adjoinRootEquivAdjoin_symm_apply_gen, IsAdjoinRoot.adjoinRootAlgEquiv_symm_apply_eq_mk, PowerBasis.quotientEquivQuotientMinpolyMap_apply, adjoinRootXPowSubCEquiv_symm_eq_root, autAdjoinRootXPowSubCEquiv_symm_smul, algEquivOfAssociated_root, algHom_ext_iff, powerBasis'_gen, AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly_symm_toAlgHom, quotEquivQuotMap_symm_apply_mk, algHom_ext'_iff, liftAlgHom_of, Minpoly.toAdjoin.surjective, powerBasis'_dim, Differential.instDifferentialAlgebraAdjoinRoot, algHomOfDvd_root, coe_mapAlgHom, coe_liftHom, algebraMap_eq, aeval_eq_of_algebra, mk_leftInverse, algebraMap_eq', finiteType, IsAdjoinRoot.adjoinRootAlgEquiv_apply_root, Minpoly.coe_toAdjoin, quotEquivQuotMap_apply, isAdjoinRoot_map_eq_mkₐ, IntermediateField.adjoin_root_eq_top, isAlgebraic_root, liftAlgHom_eq_algHom, IsAdjoinRoot.algEquiv_def, Polynomial.Monic.finite_adjoinRoot, IsAdjoinRoot.adjoinRootAlgEquiv_apply_eq_map, modByMonicHom_mk, isAdjoinRootMonic_toAdjoinRoot, mapAlgHom_comp_mapAlghom, liftAlgHom_mk, algEquivOfAssociated_toAlgHom, coe_mkₐ, algEquivOfEq_root, IntermediateField.adjoinRootEquivAdjoin_apply_root, Minpoly.coe_toAdjoin_mk_X, powerBasisAux'_repr_symm_apply, quotEquivQuotMap_apply_mk, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, toRingHom_liftAlgHom, IsAdjoinRoot.adjoinRootAlgEquiv_apply_mk, algEquivOfAssociated_symm, isSplittingField_AdjoinRoot_X_pow_sub_C, toRingHom_ofAlgHom, liftHom_eq_algHom, IsAdjoinRoot.adjoinRootAlgEquiv_symm_apply_root, isIntegral_root', algEquivOfEq_apply_root, adjoinRootXPowSubCEquiv_root, coe_liftAlgHom, powerBasis_dim, noZeroSMulDivisors_of_prime_of_degree_ne_zero, minpoly.equivAdjoin_toAlgHom, algHom_subsingleton, coe_mapAlgEquiv, minpoly.coe_equivAdjoin, finitePresentation, minpoly_powerBasis_gen, aeval_algHom_eq_zero, quotEquivQuotMap_symm_apply, powerBasisAux'_repr_apply_to_fun, coe_algEquivOfEq, aeval_eq, IsLocalization.adjoin_inv, liftHom_of, adjoinRoot_eq_top, liftHom_root, symm_mapAlgEquiv, coe_algHomOfDvd, Polynomial.Monic.free_adjoinRoot, liftAlgHom_root, autAdjoinRootXPowSubC_root, algEquivOfEq_symm, minpoly_powerBasis_gen_of_monic, liftHom_mk, algEquivOfEq_toAlgHom, algHomOfDvd_apply_root, WeierstrassCurve.Affine.CoordinateRing.basis_apply, mkₐ_toRingHom, isIntegral_root, powerBasis_gen, coe_ofAlgHom, coe_algEquivOfAssociated
instCommRing 📖	CompOp	163 math math: algEquivOfAssociated_apply_root, minpoly.ToAdjoin.injective, isAdjoinRoot_root_eq_root, AlgEquiv.coe_adjoinSingletonEquivAdjoinRootMinpoly_symm, WeierstrassCurve.Affine.CoordinateRing.smul, minpoly_root, autAdjoinRootXPowSubCEquiv_root, quotMapOfEquivQuotMapCMapSpanMk_symm_mk, root_X_pow_sub_C_eq_zero_iff, IntermediateField.adjoinRootEquivAdjoin_symm_apply_gen, WeierstrassCurve.Affine.CoordinateRing.basis_one, IsAdjoinRoot.adjoinRootAlgEquiv_symm_apply_eq_mk, PowerBasis.quotientEquivQuotientMinpolyMap_apply, adjoinRootXPowSubCEquiv_symm_eq_root, WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_C, mk_surjective, WeierstrassCurve.Affine.CoordinateRing.coe_basis, WeierstrassCurve.Affine.Point.toClass_zero, autAdjoinRootXPowSubCEquiv_symm_smul, algEquivOfAssociated_root, algHom_ext_iff, powerBasis'_gen, AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly_symm_toAlgHom, smul_mk, quotEquivQuotMap_symm_apply_mk, algHom_ext'_iff, liftAlgHom_of, evalEval_apply, symm_mapRingEquiv, Minpoly.toAdjoin.surjective, powerBasis'_dim, Differential.instDifferentialAlgebraAdjoinRoot, instIsNoetherianRing, mk_eq_mk, algHomOfDvd_root, isDomain_of_prime, WeierstrassCurve.Affine.CoordinateRing.mk_ψ, coe_mapAlgHom, coe_liftHom, algebraMap_eq, mul_div_root_cancel, WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial, aeval_eq_of_algebra, WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_neg_mul, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_add_eq, mk_leftInverse, algebraMap_eq', finiteType, coe_injective, quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk, IsAdjoinRoot.adjoinRootAlgEquiv_apply_root, mk_eq_zero, Minpoly.coe_toAdjoin, lift_comp_of, quotEquivQuotMap_apply, isAdjoinRoot_map_eq_mkₐ, WeierstrassCurve.Affine.CoordinateRing.norm_smul_basis, WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis, coe_injective', smul_of, isAlgebraic_root, isScalarTower_right, liftAlgHom_eq_algHom, IsAdjoinRoot.algEquiv_def, Polynomial.Monic.finite_adjoinRoot, lift_mk, WeierstrassCurve.Affine.CoordinateRing.map_mk, root_isInv, IsAdjoinRoot.adjoinRootAlgEquiv_apply_eq_map, modByMonicHom_mk, isAdjoinRootMonic_toAdjoinRoot, WeierstrassCurve.Affine.CoordinateRing.mk_φ, mapAlgHom_comp_mapAlghom, map_comp_map, liftAlgHom_mk, algEquivOfAssociated_toAlgHom, coe_mkₐ, algEquivOfEq_root, IntermediateField.adjoinRootEquivAdjoin_apply_root, WeierstrassCurve.Affine.CoordinateRing.instIsDomain, Minpoly.coe_toAdjoin_mk_X, powerBasisAux'_repr_symm_apply, quotEquivQuotMap_apply_mk, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, WeierstrassCurve.Affine.CoordinateRing.mk_Ψ_sq, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_neg_mul, toRingHom_liftAlgHom, WeierstrassCurve.Affine.CoordinateRing.exists_smul_basis_eq, WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial_slope, WeierstrassCurve.Affine.CoordinateRing.mk_XYIdeal'_mul_mk_XYIdeal', IsAdjoinRoot.adjoinRootAlgEquiv_apply_mk, root_X_pow_sub_C_pow, algEquivOfAssociated_symm, toRingHom_ofAlgHom, liftHom_eq_algHom, eval₂_root, IsAdjoinRoot.adjoinRootAlgEquiv_symm_apply_root, WeierstrassCurve.Affine.CoordinateRing.map_injective, isIntegral_root', algEquivOfEq_apply_root, adjoinRootXPowSubCEquiv_root, coe_liftAlgHom, WeierstrassCurve.Affine.Point.toClass_some, WeierstrassCurve.Affine.Point.toClass_injective, powerBasis_dim, map_root, noZeroSMulDivisors_of_prime_of_degree_ne_zero, mk_X, quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk, minpoly.equivAdjoin_toAlgHom, algHom_subsingleton, WeierstrassCurve.Affine.CoordinateRing.coe_norm_smul_basis, lift_of, coe_mapAlgEquiv, WeierstrassCurve.Affine.CoordinateRing.mk_ψ₂_sq, WeierstrassCurve.Affine.CoordinateRing.basis_zero, minpoly.coe_equivAdjoin, finitePresentation, quotMapOfEquivQuotMapCMapSpanMk_mk, minpoly_powerBasis_gen, aeval_algHom_eq_zero, lift_root, quotEquivQuotMap_symm_apply, quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk, powerBasisAux'_repr_apply_to_fun, coe_algEquivOfEq, aeval_eq, IsLocalization.adjoin_inv, liftHom_of, adjoinRoot_eq_top, Polynomial.X_sub_C_mul_removeFactor, WeierstrassCurve.Affine.Point.toClass_eq_zero, map_of, mk_self, liftHom_root, symm_mapAlgEquiv, WeierstrassCurve.Affine.CoordinateRing.XYIdeal'_eq, coe_algHomOfDvd, Polynomial.Monic.free_adjoinRoot, liftAlgHom_root, WeierstrassCurve.Affine.CoordinateRing.map_smul, autAdjoinRootXPowSubC_root, algEquivOfEq_symm, minpoly_powerBasis_gen_of_monic, liftHom_mk, algEquivOfEq_toAlgHom, coe_mapRingEquiv, algHomOfDvd_apply_root, quotAdjoinRootEquivQuotPolynomialQuot_mk_of, WeierstrassCurve.Affine.CoordinateRing.basis_apply, WeierstrassCurve.Affine.Point.toClass_apply, mkₐ_toRingHom, isIntegral_root, ringHom_ext_iff, WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_Y, powerBasis_gen, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_mul_XYIdeal, mk_C, coe_ofAlgHom, of.injective_of_degree_ne_zero, isRoot_root, evalEval_mk, coe_algEquivOfAssociated
instDecidableEq 📖	CompOp	—
instDistribMulActionOfIsScalarTower 📖	CompOp	—
instDistribSMulOfIsScalarTower 📖	CompOp	—
instField 📖	CompOp	10 math math: instNumberFieldRat, Polynomial.SplittingFieldAux.succ, Polynomial.SplittingFieldAux.algebraMap_succ, mul_div_root_cancel, Polynomial.natDegree_removeFactor, Polynomial.SplittingFieldAux.scalar_tower', IntermediateField.adjoin_root_eq_top, isSplittingField_AdjoinRoot_X_pow_sub_C, Polynomial.natDegree_removeFactor', Polynomial.X_sub_C_mul_removeFactor
instGroupWithZero 📖	CompOp	—
instInhabited 📖	CompOp	—
instSMulAdjoinRoot 📖	CompOp	18 math math: WeierstrassCurve.Affine.CoordinateRing.smul, autAdjoinRootXPowSubCEquiv_root, WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_C, autAdjoinRootXPowSubCEquiv_symm_smul, smul_mk, WeierstrassCurve.Affine.CoordinateRing.instIsScalarTowerPolynomial, WeierstrassCurve.Affine.CoordinateRing.norm_smul_basis, Polynomial.SplittingFieldAux.scalar_tower', WeierstrassCurve.Affine.CoordinateRing.degree_norm_smul_basis, smul_of, isScalarTower_right, instIsScalarTower, WeierstrassCurve.Affine.CoordinateRing.exists_smul_basis_eq, instSMulCommClass, WeierstrassCurve.Affine.CoordinateRing.coe_norm_smul_basis, WeierstrassCurve.Affine.CoordinateRing.map_smul, autAdjoinRootXPowSubC_root, WeierstrassCurve.Affine.CoordinateRing.smul_basis_mul_Y
liftAlgHom 📖	CompOp	11 math math: liftAlgHom_of, Minpoly.coe_toAdjoin, liftAlgHom_eq_algHom, equiv'_toAlgHom, liftAlgHom_mk, toRingHom_liftAlgHom, coe_liftAlgHom, equiv'_apply, coe_algHomOfDvd, liftAlgHom_root, liftHom_mk
liftHom 📖	CompOp	4 math math: coe_liftHom, liftHom_eq_algHom, liftHom_of, liftHom_root
map 📖	CompOp	6 math math: coe_mapAlgHom, map_comp_map, map_root, coe_mapAlgEquiv, map_of, coe_mapRingEquiv
mapAlgEquiv 📖	CompOp	2 math math: coe_mapAlgEquiv, symm_mapAlgEquiv
mapAlgHom 📖	CompOp	2 math math: coe_mapAlgHom, mapAlgHom_comp_mapAlghom
mapRingEquiv 📖	CompOp	2 math math: symm_mapRingEquiv, coe_mapRingEquiv
mk 📖	CompOp	—
mkₐ 📖	CompOp	3 math math: isAdjoinRoot_map_eq_mkₐ, coe_mkₐ, mkₐ_toRingHom
modByMonicHom 📖	CompOp	3 math math: mk_leftInverse, modByMonicHom_mk, powerBasisAux'_repr_apply_to_fun
of 📖	CompOp	33 math math: quotMapOfEquivQuotMapCMapSpanMk_symm_mk, PowerBasis.quotientEquivQuotientMinpolyMap_apply, Polynomial.SplittingFieldAux.algebraMap_succ, quotEquivQuotMap_symm_apply_mk, liftAlgHom_of, algebraMap_eq, mul_div_root_cancel, algebraMap_eq', coe_injective, lift_comp_of, quotEquivQuotMap_apply, coe_injective', smul_of, root_isInv, quotEquivQuotMap_apply_mk, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, root_X_pow_sub_C_pow, toRingHom_ofAlgHom, eval₂_root, quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk, WeierstrassCurve.Affine.CoordinateRing.coe_norm_smul_basis, lift_of, quotMapOfEquivQuotMapCMapSpanMk_mk, quotEquivQuotMap_symm_apply, liftHom_of, Polynomial.X_sub_C_mul_removeFactor, map_of, quotAdjoinRootEquivQuotPolynomialQuot_mk_of, ringHom_ext_iff, mk_C, coe_ofAlgHom, of.injective_of_degree_ne_zero, isRoot_root
ofAlgHom 📖	CompOp	3 math math: algHom_ext'_iff, toRingHom_ofAlgHom, coe_ofAlgHom
powerBasis 📖	CompOp	4 math math: powerBasis_dim, minpoly_powerBasis_gen, minpoly_powerBasis_gen_of_monic, powerBasis_gen
powerBasis' 📖	CompOp	3 math math: powerBasis'_gen, powerBasis'_dim, WeierstrassCurve.Affine.CoordinateRing.basis_apply
powerBasisAux 📖	CompOp	—
powerBasisAux' 📖	CompOp	2 math math: powerBasisAux'_repr_symm_apply, powerBasisAux'_repr_apply_to_fun
quotAdjoinRootEquivQuotPolynomialQuot 📖	CompOp	5 math math: PowerBasis.quotientEquivQuotientMinpolyMap_apply, quotEquivQuotMap_apply, quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk, quotEquivQuotMap_symm_apply, quotAdjoinRootEquivQuotPolynomialQuot_mk_of
quotEquivQuotMap 📖	CompOp	5 math math: quotEquivQuotMap_symm_apply_mk, quotEquivQuotMap_apply, quotEquivQuotMap_apply_mk, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, quotEquivQuotMap_symm_apply
quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk 📖	CompOp	2 math math: quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk, quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk
quotMapOfEquivQuotMapCMapSpanMk 📖	CompOp	2 math math: quotMapOfEquivQuotMapCMapSpanMk_symm_mk, quotMapOfEquivQuotMapCMapSpanMk_mk
root 📖	CompOp	45 math math: algEquivOfAssociated_apply_root, isAdjoinRoot_root_eq_root, minpoly_root, autAdjoinRootXPowSubCEquiv_root, root_X_pow_sub_C_eq_zero_iff, IntermediateField.adjoinRootEquivAdjoin_symm_apply_gen, adjoinRootXPowSubCEquiv_symm_eq_root, autAdjoinRootXPowSubCEquiv_symm_smul, algEquivOfAssociated_root, algHom_ext_iff, powerBasis'_gen, algHom_ext'_iff, algHomOfDvd_root, mul_div_root_cancel, aeval_eq_of_algebra, IsAdjoinRoot.adjoinRootAlgEquiv_apply_root, IntermediateField.adjoin_root_eq_top, isAlgebraic_root, liftAlgHom_eq_algHom, root_isInv, algEquivOfEq_root, IntermediateField.adjoinRootEquivAdjoin_apply_root, root_X_pow_sub_C_pow, liftHom_eq_algHom, eval₂_root, IsAdjoinRoot.adjoinRootAlgEquiv_symm_apply_root, isIntegral_root', algEquivOfEq_apply_root, adjoinRootXPowSubCEquiv_root, map_root, mk_X, aeval_algHom_eq_zero, lift_root, aeval_eq, adjoinRoot_eq_top, Polynomial.X_sub_C_mul_removeFactor, liftHom_root, coe_algHomOfDvd, liftAlgHom_root, autAdjoinRootXPowSubC_root, algHomOfDvd_apply_root, isIntegral_root, ringHom_ext_iff, powerBasis_gen, isRoot_root

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjoinRoot_eq_top 📖	mathematical	—	Algebra.adjoin AdjoinRoot CommRing.toCommSemiring CommSemiring.toSemiring instCommRing instAlgebra Algebra.id Set Set.instSingletonSet root Top.top Subalgebra OrderTop.toTop Preorder.toLE PartialOrder.toPreorder SemilatticeSup.toPartialOrder Lattice.toSemilatticeSup CompleteLattice.toLattice Algebra.instCompleteLatticeSubalgebra BoundedOrder.toOrderTop CompleteLattice.toBoundedOrder	—	Algebra.eq_top_iff induction_on aeval_eq Algebra.adjoin_singleton_eq_range_aeval
aeval_algHom_eq_zero 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval AdjoinRoot instCommRing instAlgebra root MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	RingHom.ext_iff AlgHom.commutes Polynomial.aeval_def map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass eval₂_root Polynomial.hom_eval₂
aeval_eq 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot Polynomial.semiring instCommRing Polynomial.algebraOfAlgebra Algebra.id instAlgebra AlgHom.funLike Polynomial.aeval root RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	aeval_eq_of_algebra Algebra.algebraMap_self Polynomial.map_id
aeval_eq_of_algebra 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot Polynomial.semiring instCommRing Polynomial.algebraOfAlgebra Algebra.id instAlgebra AlgHom.funLike Polynomial.aeval root RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.map algebraMap	—	Polynomial.induction_on Polynomial.aeval_C Polynomial.map_C IsScalarTower.algebraMap_apply instIsScalarTower IsScalarTower.right map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Polynomial.map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass pow_add pow_one map_mul NonUnitalAlgSemiHomClass.toMulHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass Polynomial.aeval_X Polynomial.map_mul Polynomial.map_pow Polynomial.map_X NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass
algEquivOfAssociated_apply_root 📖	mathematical	Associated Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	DFunLike.coe AlgEquiv AdjoinRoot instCommRing instAlgebra AlgEquiv.instFunLike algEquivOfAssociated root	—	algEquivOfAssociated_root
algEquivOfAssociated_root 📖	mathematical	Associated Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	DFunLike.coe AlgEquiv AdjoinRoot instCommRing instAlgebra AlgEquiv.instFunLike algEquivOfAssociated root	—	Associated.dvd Associated.symm coe_algEquivOfAssociated algHomOfDvd_root
algEquivOfAssociated_symm 📖	mathematical	Associated Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	AlgEquiv.symm AdjoinRoot instCommRing instAlgebra algEquivOfAssociated Associated.symm	—	—
algEquivOfAssociated_toAlgHom 📖	mathematical	Associated Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	AlgEquiv.toAlgHom AdjoinRoot instCommRing instAlgebra algEquivOfAssociated algHomOfDvd Associated.dvd Associated.symm	—	—
algEquivOfEq_apply_root 📖	mathematical	—	DFunLike.coe AlgEquiv AdjoinRoot CommRing.toCommSemiring CommSemiring.toSemiring instCommRing instAlgebra AlgEquiv.instFunLike algEquivOfEq root	—	algEquivOfEq_root
algEquivOfEq_root 📖	mathematical	—	DFunLike.coe AlgEquiv AdjoinRoot CommRing.toCommSemiring CommSemiring.toSemiring instCommRing instAlgebra AlgEquiv.instFunLike algEquivOfEq root	—	Eq.dvd coe_algEquivOfEq algHomOfDvd_root
algEquivOfEq_symm 📖	mathematical	—	AlgEquiv.symm AdjoinRoot CommRing.toCommSemiring CommSemiring.toSemiring instCommRing instAlgebra algEquivOfEq Polynomial	—	—
algEquivOfEq_toAlgHom 📖	mathematical	—	AlgEquiv.toAlgHom AdjoinRoot CommRing.toCommSemiring CommSemiring.toSemiring instCommRing instAlgebra algEquivOfEq algHomOfDvd Eq.dvd Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	—	—
algHomOfDvd_apply_root 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing	DFunLike.coe AlgHom AdjoinRoot instCommRing instAlgebra AlgHom.funLike algHomOfDvd root	—	algHomOfDvd_root
algHomOfDvd_root 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing	DFunLike.coe AlgHom AdjoinRoot instCommRing instAlgebra AlgHom.funLike algHomOfDvd root	—	map_root AlgHomClass.toRingHomClass AlgHom.algHomClass
algHom_ext 📖	—	DFunLike.coe AlgHom AdjoinRoot CommRing.toCommSemiring CommSemiring.toSemiring instCommRing instAlgebra Algebra.id AlgHom.funLike root	—	—	Ideal.Quotient.algHom_ext Ideal.instIsTwoSided_1 Polynomial.algHom_ext
algHom_ext' 📖	—	AlgHom.comp AdjoinRoot CommSemiring.toSemiring CommRing.toCommSemiring instCommRing instAlgebra ofAlgHom DFunLike.coe AlgHom AlgHom.funLike root	—	—	AlgHom.coe_ringHom_injective ringHom_ext AlgHomClass.toRingHomClass AlgHom.algHomClass
algHom_ext'_iff 📖	mathematical	—	AlgHom.comp AdjoinRoot CommSemiring.toSemiring CommRing.toCommSemiring instCommRing instAlgebra ofAlgHom DFunLike.coe AlgHom AlgHom.funLike root	—	algHom_ext'
algHom_ext_iff 📖	mathematical	—	DFunLike.coe AlgHom AdjoinRoot CommRing.toCommSemiring CommSemiring.toSemiring instCommRing instAlgebra Algebra.id AlgHom.funLike root	—	algHom_ext
algHom_subsingleton 📖	mathematical	—	AlgHom AdjoinRoot Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instSub CommRing.toRing Polynomial.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C Polynomial.X Polynomial.instOne instCommRing instAlgebra Algebra.id	—	algHom_ext inv_unique AlgHom.commutes map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass algebraMap_eq root_isInv map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass
algebraMap_eq 📖	mathematical	—	algebraMap AdjoinRoot CommRing.toCommSemiring CommSemiring.toSemiring instCommRing instAlgebra Algebra.id of	—	—
algebraMap_eq' 📖	mathematical	—	algebraMap AdjoinRoot CommSemiring.toSemiring CommRing.toCommSemiring instCommRing instAlgebra RingHom.comp Semiring.toNonAssocSemiring of	—	—
coe_algEquivOfAssociated 📖	mathematical	Associated Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	DFunLike.coe AlgEquiv AdjoinRoot instCommRing instAlgebra AlgEquiv.instFunLike algEquivOfAssociated AlgHom AlgHom.funLike algHomOfDvd Associated.dvd Associated.symm	—	—
coe_algEquivOfEq 📖	mathematical	—	DFunLike.coe AlgEquiv AdjoinRoot CommRing.toCommSemiring CommSemiring.toSemiring instCommRing instAlgebra AlgEquiv.instFunLike algEquivOfEq AlgHom AlgHom.funLike algHomOfDvd Eq.dvd Polynomial MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	—	—
coe_algHomOfDvd 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing	DFunLike.coe AlgHom AdjoinRoot instCommRing instAlgebra AlgHom.funLike algHomOfDvd Algebra.id liftAlgHom Algebra.ofId root Polynomial.semiring Polynomial.algebraOfAlgebra Polynomial.aeval RingHom Semiring.toNonAssocSemiring RingHom.instFunLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing aeval_eq	—	—
coe_injective 📖	mathematical	—	AdjoinRoot EuclideanDomain.toCommRing Field.toEuclideanDomain DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.instFunLike of	—	nontrivial instIsDomain RingHom.injective DivisionRing.isSimpleRing
coe_injective' 📖	mathematical	—	AdjoinRoot EuclideanDomain.toCommRing Field.toEuclideanDomain DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.instFunLike of	—	RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing
coe_liftAlgHom 📖	mathematical	Polynomial.eval₂ CommSemiring.toSemiring CommRing.toCommSemiring RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	DFunLike.coe AdjoinRoot instCommRing instAlgebra liftAlgHom RingHom RingHom.instFunLike lift AlgHom.toRingHom	—	AlgHomClass.toRingHomClass AlgHom.algHomClass
coe_liftHom 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	RingHomClass.toRingHom AdjoinRoot instCommRing instAlgebra Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass liftHom lift algebraMap	—	AlgHomClass.toRingHomClass AlgHom.algHomClass
coe_mapAlgEquiv 📖	mathematical	Associated Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.map RingHomClass.toRingHom AlgEquiv AlgEquiv.instFunLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass	DFunLike.coe AdjoinRoot instCommRing instAlgebra mapAlgEquiv RingHom RingHom.instFunLike map Associated.dvd Associated.symm	—	AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass
coe_mapAlgHom 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing Polynomial.map RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	DFunLike.coe AdjoinRoot instCommRing instAlgebra mapAlgHom RingHom RingHom.instFunLike map	—	AlgHomClass.toRingHomClass AlgHom.algHomClass
coe_mapRingEquiv 📖	mathematical	Associated Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.map RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike Semiring.toNonAssocSemiring RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass	DFunLike.coe AdjoinRoot instCommRing mapRingEquiv RingHom RingHom.instFunLike map Associated.dvd Associated.symm	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass
coe_mkₐ 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot Polynomial.semiring instCommRing Polynomial.algebraOfAlgebra Algebra.id instAlgebra AlgHom.funLike mkₐ RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	—
coe_ofAlgHom 📖	mathematical	—	DFunLike.coe AlgHom AdjoinRoot CommSemiring.toSemiring CommRing.toCommSemiring instCommRing instAlgebra AlgHom.funLike ofAlgHom RingHom Semiring.toNonAssocSemiring RingHom.instFunLike of	—	—
equiv'_apply 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot Polynomial.semiring instCommRing Polynomial.algebraOfAlgebra Algebra.id instAlgebra AlgHom.funLike Polynomial.aeval root minpoly CommRing.toRing PowerBasis.gen MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	AlgEquiv AlgEquiv.instFunLike equiv' liftAlgHom Algebra.ofId	—	—
equiv'_symm_apply 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot Polynomial.semiring instCommRing Polynomial.algebraOfAlgebra Algebra.id instAlgebra AlgHom.funLike Polynomial.aeval root minpoly CommRing.toRing PowerBasis.gen MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	AlgEquiv AlgEquiv.instFunLike AlgEquiv.symm equiv' Ring.toSemiring PowerBasis.lift	—	—
equiv'_symm_toAlgHom 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot Polynomial.semiring instCommRing Polynomial.algebraOfAlgebra Algebra.id instAlgebra AlgHom.funLike Polynomial.aeval root minpoly CommRing.toRing PowerBasis.gen MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	AlgEquiv.toAlgHom AlgEquiv.symm equiv' PowerBasis.lift	—	—
equiv'_toAlgHom 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot Polynomial.semiring instCommRing Polynomial.algebraOfAlgebra Algebra.id instAlgebra AlgHom.funLike Polynomial.aeval root minpoly CommRing.toRing PowerBasis.gen MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	AlgEquiv.toAlgHom equiv' liftAlgHom Algebra.ofId	—	—
eval₂_root 📖	mathematical	—	Polynomial.eval₂ AdjoinRoot CommSemiring.toSemiring CommRing.toCommSemiring instCommRing of root MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	algebraMap_eq Polynomial.aeval_def aeval_eq mk_self
finitePresentation 📖	mathematical	—	Algebra.FinitePresentation AdjoinRoot CommRing.toCommSemiring CommSemiring.toSemiring instCommRing instAlgebra	—	Algebra.FinitePresentation.quotient Submodule.fg_span_singleton Algebra.FinitePresentation.polynomial
finiteType 📖	mathematical	—	Algebra.FiniteType AdjoinRoot CommSemiring.toSemiring CommRing.toCommSemiring instCommRing instAlgebra	—	Algebra.FiniteType.quotient Algebra.FiniteType.instPolynomial
induction_on 📖	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot Semiring.toNonAssocSemiring Polynomial.semiring instCommRing RingHom.instFunLike	—	—	Quotient.inductionOn'
instIsNoetherianRing 📖	mathematical	—	IsNoetherianRing AdjoinRoot CommSemiring.toSemiring CommRing.toCommSemiring instCommRing	—	Ideal.Quotient.isNoetherianRing Polynomial.isNoetherianRing
instIsScalarTower 📖	mathematical	—	IsScalarTower AdjoinRoot instSMulAdjoinRoot	—	Submodule.Quotient.isScalarTower Polynomial.isScalarTower
instSMulCommClass 📖	mathematical	—	SMulCommClass AdjoinRoot instSMulAdjoinRoot	—	Submodule.Quotient.smulCommClass Polynomial.smulCommClass
isAlgebraic_root 📖	mathematical	—	IsAlgebraic AdjoinRoot CommRing.toRing instCommRing instAlgebra CommRing.toCommSemiring Algebra.id root	—	eval₂_root
isDomain_of_prime 📖	mathematical	Prime Polynomial CommSemiring.toSemiring CommRing.toCommSemiring CommSemiring.toCommMonoidWithZero Polynomial.commSemiring	IsDomain AdjoinRoot instCommRing	—	Ideal.instIsTwoSided_1 Ideal.Quotient.isDomain_iff_prime Ideal.span_singleton_prime Prime.ne_zero
isIntegral_root 📖	mathematical	—	IsIntegral AdjoinRoot EuclideanDomain.toCommRing Field.toEuclideanDomain CommRing.toRing instCommRing instAlgebra CommRing.toCommSemiring Algebra.id root	—	IsAlgebraic.isIntegral isAlgebraic_root
isIntegral_root' 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring	IsIntegral AdjoinRoot CommRing.toRing instCommRing instAlgebra Algebra.id root	—	eval₂_root
isRoot_root 📖	mathematical	—	Polynomial.IsRoot AdjoinRoot CommSemiring.toSemiring CommRing.toCommSemiring instCommRing Polynomial.map of root	—	Polynomial.IsRoot.eq_1 Polynomial.eval_map eval₂_root
isScalarTower_right 📖	mathematical	—	IsScalarTower AdjoinRoot instSMulAdjoinRoot Algebra.toSMul CommRing.toCommSemiring instCommRing CommSemiring.toSemiring Algebra.id	—	Ideal.Quotient.isScalarTower_right Ideal.instIsTwoSided_1
liftAlgHom_eq_algHom 📖	mathematical	—	liftAlgHom Algebra.id CommRing.toCommSemiring Algebra.ofId CommSemiring.toSemiring DFunLike.coe AlgHom AdjoinRoot instCommRing instAlgebra AlgHom.funLike root aeval_algHom_eq_zero	—	algHom_ext aeval_algHom_eq_zero liftAlgHom_root
liftAlgHom_mk 📖	mathematical	Polynomial.eval₂ CommSemiring.toSemiring CommRing.toCommSemiring RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	DFunLike.coe AdjoinRoot instCommRing instAlgebra liftAlgHom RingHom Polynomial Polynomial.semiring RingHom.instFunLike	—	AlgHomClass.toRingHomClass AlgHom.algHomClass
liftAlgHom_of 📖	mathematical	Polynomial.eval₂ CommSemiring.toSemiring CommRing.toCommSemiring RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	DFunLike.coe AdjoinRoot instCommRing instAlgebra liftAlgHom RingHom RingHom.instFunLike of	—	AlgHomClass.toRingHomClass AlgHom.algHomClass lift_of
liftAlgHom_root 📖	mathematical	Polynomial.eval₂ CommSemiring.toSemiring CommRing.toCommSemiring RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	DFunLike.coe AdjoinRoot instCommRing instAlgebra liftAlgHom root	—	AlgHomClass.toRingHomClass AlgHom.algHomClass lift_root
liftHom_eq_algHom 📖	mathematical	—	liftHom DFunLike.coe AlgHom AdjoinRoot CommRing.toCommSemiring CommSemiring.toSemiring instCommRing instAlgebra Algebra.id AlgHom.funLike root aeval_algHom_eq_zero	—	liftAlgHom_eq_algHom
liftHom_mk 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	AdjoinRoot instCommRing instAlgebra liftAlgHom Algebra.ofId RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	—
liftHom_of 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	AdjoinRoot instCommRing instAlgebra liftHom RingHom Semiring.toNonAssocSemiring RingHom.instFunLike of algebraMap	—	lift_of
liftHom_root 📖	mathematical	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id AlgHom.funLike Polynomial.aeval MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	AdjoinRoot instCommRing instAlgebra liftHom root	—	lift_root
lift_comp_of 📖	mathematical	Polynomial.eval₂ CommSemiring.toSemiring CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	RingHom.comp AdjoinRoot Semiring.toNonAssocSemiring instCommRing lift of	—	RingHom.ext lift_of
lift_mk 📖	mathematical	Polynomial.eval₂ CommSemiring.toSemiring CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	DFunLike.coe RingHom AdjoinRoot Semiring.toNonAssocSemiring instCommRing RingHom.instFunLike lift Polynomial Polynomial.semiring	—	—
lift_of 📖	mathematical	Polynomial.eval₂ CommSemiring.toSemiring CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	DFunLike.coe RingHom AdjoinRoot Semiring.toNonAssocSemiring instCommRing RingHom.instFunLike lift of	—	mk_C Polynomial.eval₂_C
lift_root 📖	mathematical	Polynomial.eval₂ CommSemiring.toSemiring CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	DFunLike.coe RingHom AdjoinRoot Semiring.toNonAssocSemiring instCommRing RingHom.instFunLike lift root	—	root.eq_1 Polynomial.eval₂_X
mapAlgHom_comp_mapAlghom 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing Polynomial.map RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	AlgHom.comp AdjoinRoot instCommRing instAlgebra mapAlgHom Dvd.dvd.trans	—	AlgHomClass.toRingHomClass AlgHom.algHomClass algHom_ext' Dvd.dvd.trans AlgHom.ext map_of map_root
map_comp_map 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing Polynomial.map	RingHom.comp AdjoinRoot Semiring.toNonAssocSemiring instCommRing map Dvd.dvd.trans	—	ringHom_ext Dvd.dvd.trans RingHom.ext map_of map_root
map_of 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing Polynomial.map	DFunLike.coe RingHom AdjoinRoot Semiring.toNonAssocSemiring instCommRing RingHom.instFunLike map of	—	lift_of
map_root 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing Polynomial.map	DFunLike.coe RingHom AdjoinRoot Semiring.toNonAssocSemiring instCommRing RingHom.instFunLike map root	—	lift_root
minpoly_powerBasis_gen 📖	mathematical	—	minpoly AdjoinRoot EuclideanDomain.toCommRing Field.toEuclideanDomain CommRing.toRing instCommRing instAlgebra CommRing.toCommSemiring Algebra.id PowerBasis.gen powerBasis Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Polynomial.leadingCoeff	—	powerBasis_gen minpoly_root
minpoly_powerBasis_gen_of_monic 📖	mathematical	Polynomial.Monic DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial Polynomial.instZero Polynomial.Monic.ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing	minpoly AdjoinRoot EuclideanDomain.toCommRing Field.toEuclideanDomain CommRing.toRing instCommRing instAlgebra CommRing.toCommSemiring Algebra.id PowerBasis.gen powerBasis	—	minpoly_powerBasis_gen Polynomial.Monic.leadingCoeff inv_one RingHom.map_one mul_one
minpoly_root 📖	mathematical	—	minpoly AdjoinRoot EuclideanDomain.toCommRing Field.toEuclideanDomain CommRing.toRing instCommRing instAlgebra CommRing.toCommSemiring Algebra.id root Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Polynomial.leadingCoeff	—	Polynomial.monic_mul_leadingCoeff_inv minpoly.unique map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass aeval_eq mk_self MulZeroClass.zero_mul Polynomial.ringHom_ext' RingHom.ext lift_of lift_root Polynomial.degree_eq_natDegree Polynomial.Monic.ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing Nat.cast_le WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid WithBot.zeroLEOneClass Nat.instZeroLEOneClass WithBot.charZero Nat.instCharZero Polynomial.natDegree_mul IsDomain.to_noZeroDivisors instIsDomain Polynomial.C_eq_zero inv_eq_zero Polynomial.leadingCoeff_eq_zero Polynomial.natDegree_C add_zero Polynomial.natDegree_le_of_dvd RingHom.comp_apply map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass mk_eq_zero
mk_C 📖	mathematical	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot Semiring.toNonAssocSemiring Polynomial.semiring instCommRing RingHom.instFunLike Polynomial.C of	—	—
mk_X 📖	mathematical	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot Semiring.toNonAssocSemiring Polynomial.semiring instCommRing RingHom.instFunLike Polynomial.X root	—	—
mk_eq_mk 📖	mathematical	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot Semiring.toNonAssocSemiring Polynomial.semiring instCommRing RingHom.instFunLike semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing Polynomial.instSub CommRing.toRing	—	Ideal.Quotient.eq Ideal.mem_span_singleton
mk_eq_zero 📖	mathematical	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot Semiring.toNonAssocSemiring Polynomial.semiring instCommRing RingHom.instFunLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring Polynomial.commRing	—	sub_zero
mk_leftInverse 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring	AdjoinRoot Polynomial DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring instCommRing RingHom.instFunLike LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Polynomial.commRing Algebra.toModule instAlgebra Algebra.id Polynomial.module Semiring.toModule LinearMap.instFunLike modByMonicHom	—	induction_on Polynomial.modByMonic_eq_sub_mul_div sub_sub_cancel_left dvd_neg dvd_mul_right
mk_ne_zero_of_degree_lt 📖	—	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder Polynomial.degree	—	—	Iff.not mk_eq_zero Polynomial.Monic.not_dvd_of_degree_lt
mk_ne_zero_of_natDegree_lt 📖	—	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.natDegree	—	—	Iff.not mk_eq_zero Polynomial.Monic.not_dvd_of_natDegree_lt
mk_self 📖	mathematical	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot Semiring.toNonAssocSemiring Polynomial.semiring instCommRing RingHom.instFunLike MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Quotient.sound' QuotientAddGroup.leftRel_apply Ideal.mem_span_singleton add_zero
mk_surjective 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring instCommRing RingHom.instFunLike	—	Ideal.Quotient.mk_surjective
mkₐ_toRingHom 📖	mathematical	—	RingHomClass.toRingHom AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot Polynomial.semiring instCommRing Polynomial.algebraOfAlgebra Algebra.id instAlgebra AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass mkₐ	—	AlgHomClass.toRingHomClass AlgHom.algHomClass
modByMonicHom_mk 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring	DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring AdjoinRoot Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing Polynomial.commRing Algebra.toModule instAlgebra Algebra.id Polynomial.module Semiring.toModule LinearMap.instFunLike modByMonicHom RingHom Polynomial.semiring RingHom.instFunLike Polynomial.modByMonic CommRing.toRing	—	—
mul_div_root_cancel 📖	mathematical	—	Polynomial AdjoinRoot EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField CommSemiring.toSemiring CommRing.toCommSemiring instCommRing Polynomial.instMul Polynomial.instSub DivisionRing.toRing Field.toDivisionRing Polynomial.X DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C root Polynomial.instDiv Polynomial.map of	—	Polynomial.IsRoot.mul_div_eq isRoot_root
noZeroSMulDivisors_of_prime_of_degree_ne_zero 📖	mathematical	Prime Polynomial CommSemiring.toSemiring CommRing.toCommSemiring CommSemiring.toCommMonoidWithZero Polynomial.commSemiring	Module.IsTorsionFree AdjoinRoot NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing Algebra.toModule instAlgebra Algebra.id	—	Module.isTorsionFree_iff_algebraMap_injective isDomain_of_prime of.injective_of_degree_ne_zero
nontrivial 📖	mathematical	—	Nontrivial AdjoinRoot	—	IsDomain.to_noZeroDivisors Polynomial.degree_C IsUnit.ne_zero IsDomain.toNontrivial
powerBasis'_dim 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring	PowerBasis.dim AdjoinRoot CommRing.toRing instCommRing instAlgebra Algebra.id powerBasis' Polynomial.natDegree	—	—
powerBasis'_gen 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring	PowerBasis.gen AdjoinRoot CommRing.toRing instCommRing instAlgebra Algebra.id powerBasis' root	—	—
powerBasisAux'_repr_apply_to_fun 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring	DFunLike.coe Finsupp Polynomial.natDegree MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Finsupp.instFunLike LinearEquiv RingHom.id RingHomInvPair.ids AdjoinRoot NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing Finsupp.instAddCommMonoid Algebra.toModule instAlgebra Algebra.id Finsupp.module Semiring.toModule EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv Module.Basis.repr powerBasisAux' Polynomial.coeff LinearMap Polynomial Polynomial.commRing Polynomial.module LinearMap.instFunLike modByMonicHom	—	RingHomInvPair.ids
powerBasisAux'_repr_symm_apply 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids Finsupp Polynomial.natDegree MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring AdjoinRoot Finsupp.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing Finsupp.module Semiring.toModule Algebra.toModule instAlgebra Algebra.id EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearEquiv.symm Module.Basis.repr powerBasisAux' RingHom Polynomial Polynomial.semiring RingHom.instFunLike Finset.sum Polynomial.commRing Finset.univ Fin.fintype LinearMap Polynomial.module LinearMap.instFunLike Polynomial.monomial Finsupp.instFunLike	—	RingHomInvPair.ids
powerBasis_dim 📖	mathematical	—	PowerBasis.dim AdjoinRoot EuclideanDomain.toCommRing Field.toEuclideanDomain CommRing.toRing instCommRing instAlgebra CommRing.toCommSemiring Algebra.id powerBasis Polynomial.natDegree DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield	—	—
powerBasis_gen 📖	mathematical	—	PowerBasis.gen AdjoinRoot EuclideanDomain.toCommRing Field.toEuclideanDomain CommRing.toRing instCommRing instAlgebra CommRing.toCommSemiring Algebra.id powerBasis root	—	—
quotAdjoinRootEquivQuotPolynomialQuot_mk_of 📖	mathematical	—	DFunLike.coe RingEquiv HasQuotient.Quotient AdjoinRoot Ideal CommSemiring.toSemiring CommRing.toCommSemiring instCommRing Ideal.instHasQuotient_1 Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike of Polynomial Ideal.Quotient.semiring Polynomial.semiring Polynomial.commRing Ideal.Quotient.commRing Ideal.span Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 Set Set.instSingletonSet Polynomial.map Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike quotAdjoinRootEquivQuotPolynomialQuot Polynomial.ring Ideal.Quotient.instRingQuotient	—	Ideal.instIsTwoSided_1
quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk 📖	mathematical	—	DFunLike.coe RingEquiv HasQuotient.Quotient Polynomial Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.Quotient.semiring Polynomial.semiring Polynomial.commRing Ideal.Quotient.commRing Ideal.span Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 Set Set.instSingletonSet Polynomial.map AdjoinRoot instCommRing Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike of Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm quotAdjoinRootEquivQuotPolynomialQuot Polynomial.ring Ideal.Quotient.instRingQuotient	—	Ideal.instIsTwoSided_1 quotAdjoinRootEquivQuotPolynomialQuot.eq_1 RingEquiv.symm_trans_apply RingEquiv.symm_symm Ideal.quotEquivOfEq_symm RingHom.comp_apply DoubleQuot.quotQuotMk.eq_1 quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk
quotEquivQuotMap_apply 📖	mathematical	—	DFunLike.coe AlgEquiv HasQuotient.Quotient AdjoinRoot Ideal CommSemiring.toSemiring CommRing.toCommSemiring instCommRing Ideal.instHasQuotient_1 Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike of Polynomial Ideal.Quotient.semiring Polynomial.semiring Polynomial.commRing Ideal.Quotient.commRing Ideal.span Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 Set Set.instSingletonSet Polynomial.map Ideal.instAlgebraQuotient instAlgebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike quotEquivQuotMap RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike quotAdjoinRootEquivQuotPolynomialQuot	—	Ideal.instIsTwoSided_1
quotEquivQuotMap_apply_mk 📖	mathematical	—	DFunLike.coe AlgEquiv HasQuotient.Quotient AdjoinRoot Ideal CommSemiring.toSemiring CommRing.toCommSemiring instCommRing Ideal.instHasQuotient_1 Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike of Polynomial Ideal.Quotient.semiring Polynomial.semiring Polynomial.commRing Ideal.Quotient.commRing Ideal.span Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 Set Set.instSingletonSet Polynomial.map Ideal.instAlgebraQuotient instAlgebra Algebra.id Polynomial.algebraOfAlgebra AlgEquiv.instFunLike quotEquivQuotMap Polynomial.ring Ideal.Quotient.instRingQuotient	—	Ideal.instIsTwoSided_1 quotEquivQuotMap_apply quotAdjoinRootEquivQuotPolynomialQuot_mk_of
quotEquivQuotMap_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv HasQuotient.Quotient Polynomial Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.Quotient.semiring Polynomial.semiring Polynomial.commRing Ideal.Quotient.commRing Ideal.span Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 Set Set.instSingletonSet Polynomial.map AdjoinRoot instCommRing Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike of Ideal.instAlgebraQuotient Polynomial.algebraOfAlgebra Algebra.id instAlgebra AlgEquiv.instFunLike AlgEquiv.symm quotEquivQuotMap RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm quotAdjoinRootEquivQuotPolynomialQuot	—	Ideal.instIsTwoSided_1
quotEquivQuotMap_symm_apply_mk 📖	mathematical	—	DFunLike.coe AlgEquiv HasQuotient.Quotient Polynomial Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.Quotient.semiring Polynomial.semiring Polynomial.commRing Ideal.Quotient.commRing Ideal.span Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 Set Set.instSingletonSet Polynomial.map AdjoinRoot instCommRing Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike of Ideal.instAlgebraQuotient Polynomial.algebraOfAlgebra Algebra.id instAlgebra AlgEquiv.instFunLike AlgEquiv.symm quotEquivQuotMap Polynomial.ring Ideal.Quotient.instRingQuotient	—	Ideal.instIsTwoSided_1 quotEquivQuotMap_symm_apply
quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk 📖	mathematical	—	DFunLike.coe RingEquiv HasQuotient.Quotient AdjoinRoot Ideal Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring Polynomial.ring CommRing.toRing Ideal.instHasQuotient Ideal.span Set Set.instSingletonSet Ideal.Quotient.semiring Polynomial.commRing Ideal.instHasQuotient_1 Ideal.Quotient.commRing Ideal.map RingHom Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 Polynomial.semiring RingHom.instFunLike Polynomial.C Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk instCommRing DoubleQuot.quotQuotMk	—	Ideal.instIsTwoSided_1
quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk 📖	mathematical	—	DFunLike.coe RingEquiv HasQuotient.Quotient Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Ideal Polynomial.semiring Ideal.instHasQuotient_1 Polynomial.commRing Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C Ring.toSemiring Polynomial.ring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.semiring Ideal.Quotient.commRing Ideal.Quotient.ring Ideal.instIsTwoSided_1 Ideal.span Set Set.instSingletonSet AdjoinRoot Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk DoubleQuot.quotQuotMk Ideal.Quotient.instRingQuotient instCommRing	—	Ideal.instIsTwoSided_1
quotMapOfEquivQuotMapCMapSpanMk_mk 📖	mathematical	—	DFunLike.coe RingEquiv HasQuotient.Quotient AdjoinRoot Ideal CommSemiring.toSemiring CommRing.toCommSemiring instCommRing Ideal.instHasQuotient_1 Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike of Polynomial Ring.toSemiring Polynomial.ring CommRing.toRing Ideal.instHasQuotient Ideal.span Set Set.instSingletonSet Ideal.Quotient.semiring Polynomial.commRing Ideal.Quotient.commRing Ideal.Quotient.ring Ideal.instIsTwoSided_1 Polynomial.semiring Polynomial.C Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike quotMapOfEquivQuotMapCMapSpanMk Ideal.Quotient.instRingQuotient	—	Ideal.instIsTwoSided_1
quotMapOfEquivQuotMapCMapSpanMk_symm_mk 📖	mathematical	—	DFunLike.coe RingEquiv HasQuotient.Quotient AdjoinRoot Ideal Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Ring.toSemiring Polynomial.ring CommRing.toRing Ideal.instHasQuotient Ideal.span Set Set.instSingletonSet Ideal.Quotient.semiring Polynomial.commRing Ideal.instHasQuotient_1 Ideal.Quotient.commRing Ideal.map RingHom Semiring.toNonAssocSemiring Ideal.Quotient.ring Ideal.instIsTwoSided_1 Polynomial.semiring RingHom.instFunLike Polynomial.C instCommRing of Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm quotMapOfEquivQuotMapCMapSpanMk Ideal.Quotient.instRingQuotient	—	Ideal.instIsTwoSided_1 quotMapOfEquivQuotMapCMapSpanMk.eq_1 Ideal.quotEquivOfEq_symm
ringHom_ext 📖	—	RingHom.comp AdjoinRoot Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing of DFunLike.coe RingHom RingHom.instFunLike root	—	—	Ideal.Quotient.ringHom_ext Ideal.instIsTwoSided_1 Polynomial.ringHom_ext' RingHom.ext
ringHom_ext_iff 📖	mathematical	—	RingHom.comp AdjoinRoot Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing of DFunLike.coe RingHom RingHom.instFunLike root	—	ringHom_ext
root_isInv 📖	mathematical	—	AdjoinRoot Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instSub CommRing.toRing Polynomial.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C Polynomial.X Polynomial.instOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing of root AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne	—	Polynomial.eval₂_mul Polynomial.eval₂_C Polynomial.eval₂_X Polynomial.eval₂_one sub_eq_zero Polynomial.eval₂_sub eval₂_root
smul_mk 📖	mathematical	—	AdjoinRoot instSMulAdjoinRoot DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Semiring.toNonAssocSemiring Polynomial.semiring instCommRing RingHom.instFunLike SMulZeroClass.toSMul Polynomial.instZero Polynomial.smulZeroClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—
smul_of 📖	mathematical	—	AdjoinRoot instSMulAdjoinRoot DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing RingHom.instFunLike of SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DistribSMul.toSMulZeroClass	—	of.eq_1 RingHom.comp_apply Polynomial.smul_C
span_maximal_of_irreducible 📖	mathematical	—	Ideal.IsMaximal Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.semiring Ideal.span Set Set.instSingletonSet	—	PrincipalIdealRing.isMaximal_of_irreducible EuclideanDomain.to_principal_ideal_domain Fact.out
symm_mapAlgEquiv 📖	mathematical	Associated Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.map RingHomClass.toRingHom AlgEquiv AlgEquiv.instFunLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instEquivLike AlgEquiv.instAlgEquivClass	AlgEquiv.symm AdjoinRoot instCommRing instAlgebra mapAlgEquiv	—	AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass
symm_mapRingEquiv 📖	mathematical	Associated Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring Polynomial.map RingHomClass.toRingHom RingEquiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike Semiring.toNonAssocSemiring RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass	RingEquiv.symm AdjoinRoot instCommRing mapRingEquiv	—	RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass
toRingHom_liftAlgHom 📖	mathematical	Polynomial.eval₂ CommSemiring.toSemiring CommRing.toCommSemiring RingHomClass.toRingHom AlgHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	AdjoinRoot instCommRing instAlgebra liftAlgHom lift AlgHom.toRingHom	—	AlgHomClass.toRingHomClass AlgHom.algHomClass
toRingHom_ofAlgHom 📖	mathematical	—	RingHomClass.toRingHom AlgHom AdjoinRoot CommSemiring.toSemiring CommRing.toCommSemiring instCommRing instAlgebra AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass ofAlgHom of	—	AlgHomClass.toRingHomClass AlgHom.algHomClass

AdjoinRoot.Minpoly

Definitions

Name	Category	Theorems
toAdjoin 📖	CompOp	8 math math: minpoly.ToAdjoin.injective, AlgEquiv.coe_adjoinSingletonEquivAdjoinRootMinpoly_symm, AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly_symm_toAlgHom, toAdjoin.surjective, coe_toAdjoin, coe_toAdjoin_mk_X, minpoly.equivAdjoin_toAlgHom, minpoly.coe_equivAdjoin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_toAdjoin 📖	mathematical	—	DFunLike.coe AlgHom AdjoinRoot minpoly CommRing.toRing Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin Set Set.instSingletonSet AdjoinRoot.instCommRing Subalgebra.toSemiring AdjoinRoot.instAlgebra Algebra.id Subalgebra.algebra AlgHom.funLike toAdjoin Polynomial.instCommRingAdjoinSingleton AdjoinRoot.liftAlgHom Algebra.ofId Algebra.self_mem_adjoin_singleton	—	—
coe_toAdjoin_mk_X 📖	mathematical	—	Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin Set Set.instSingletonSet DFunLike.coe AlgHom AdjoinRoot minpoly CommRing.toRing AdjoinRoot.instCommRing Subalgebra.toSemiring AdjoinRoot.instAlgebra Algebra.id Subalgebra.algebra AlgHom.funLike toAdjoin RingHom Polynomial Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.X	—	Algebra.self_mem_adjoin_singleton AdjoinRoot.liftAlgHom_root

AdjoinRoot.Minpoly.toAdjoin

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
surjective 📖	mathematical	—	AdjoinRoot minpoly CommRing.toRing Subalgebra CommRing.toCommSemiring CommSemiring.toSemiring SetLike.instMembership Subalgebra.instSetLike Algebra.adjoin Set Set.instSingletonSet DFunLike.coe AlgHom AdjoinRoot.instCommRing Subalgebra.toSemiring AdjoinRoot.instAlgebra Algebra.id Subalgebra.algebra AlgHom.funLike AdjoinRoot.Minpoly.toAdjoin	—	AlgHom.range_eq_top eq_top_iff Algebra.adjoin_adjoin_coe_preimage Algebra.adjoin_le Algebra.self_mem_adjoin_singleton AdjoinRoot.liftAlgHom_root

AdjoinRoot.Polynomial

Definitions

Name	Category	Theorems
quotQuotEquivComm 📖	CompOp	2 math math: quotQuotEquivComm_mk, quotQuotEquivComm_symm_mk_mk

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quotQuotEquivComm_mk 📖	mathematical	—	DFunLike.coe RingEquiv HasQuotient.Quotient Polynomial Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.Quotient.semiring Polynomial.semiring Polynomial.commRing Ideal.Quotient.commRing Ideal.span Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 Set Set.instSingletonSet Polynomial.map Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C Polynomial.ring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike quotQuotEquivComm Ideal.Quotient.instRingQuotient	—	Ideal.instIsTwoSided_1
quotQuotEquivComm_symm_mk_mk 📖	mathematical	—	DFunLike.coe RingEquiv HasQuotient.Quotient Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Ideal Polynomial.semiring Ideal.instHasQuotient_1 Polynomial.commRing Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C Ideal.Quotient.semiring Ideal.Quotient.commRing Ideal.span Ring.toSemiring CommRing.toRing Polynomial.ring Ideal.instHasQuotient Set Set.instSingletonSet Ideal.Quotient.ring Ideal.instIsTwoSided_1 Polynomial.map Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm quotQuotEquivComm Ideal.Quotient.instRingQuotient	—	Ideal.instIsTwoSided_1

AdjoinRoot.of

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
injective_of_degree_ne_zero 📖	mathematical	—	AdjoinRoot DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring AdjoinRoot.instCommRing RingHom.instFunLike AdjoinRoot.of	—	injective_iff_map_eq_zero RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Polynomial.C_eq_zero eq_zero_of_zero_dvd AdjoinRoot.mk_eq_zero RingHom.comp_apply eq_1 Mathlib.Tactic.Contrapose.contrapose₂ Polynomial.degree_C le_antisymm Polynomial.degree_le_of_dvd IsDomain.to_noZeroDivisors Polynomial.zero_le_degree_iff

Irreducible

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_dvd_monic_irreducible_of_isIntegral 📖	mathematical	Irreducible Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.map algebraMap	—	ne_zero isIntegral_trans AdjoinRoot.instIsScalarTower IsScalarTower.right AdjoinRoot.isIntegral_root minpoly.dvd_map_of_isScalarTower AdjoinRoot.minpoly_root minpoly.monic minpoly.irreducible instIsDomain dvd_of_mul_right_dvd

Polynomial.Monic

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_splits_map 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring	Polynomial.Splits Polynomial.map algebraMap	—	Nat.strong_induction_on Module.Finite.self Module.Free.self Polynomial.map_one eq_one_of_isUnit Polynomial.eval_map_algebraMap AdjoinRoot.aeval_eq AdjoinRoot.mk_self of_mul_monic_left Polynomial.monic_X_sub_C map free_adjoinRoot finite_adjoinRoot Ideal.Quotient.nontrivial_iff natDegree_map natDegree_mul Polynomial.natDegree_sub_C Polynomial.natDegree_X IsRightCancelAdd.addRightStrictMono_of_addRightMono AddRightCancelSemigroup.toIsRightCancelAdd covariant_swap_add_of_covariant_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_swap_add_of_contravariant_add contravariant_lt_of_covariant_le Nat.instZeroLEOneClass IsScalarTower.right IsScalarTower.of_algebraMap_eq' Module.Finite.trans Module.Free.trans IsScalarTower.algebraMap_eq Polynomial.map_map Polynomial.map_mul Polynomial.Splits.mul Polynomial.map_sub Polynomial.map_X Polynomial.map_C
finite_adjoinRoot 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring	Module.Finite AdjoinRoot NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AdjoinRoot.instCommRing Algebra.toModule AdjoinRoot.instAlgebra Algebra.id	—	Module.Finite.of_basis Finite.of_fintype
finite_quotient 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring	Module.Finite HasQuotient.Quotient Polynomial Ideal Polynomial.semiring Ideal.instHasQuotient_1 Polynomial.commRing Ideal.span Set Set.instSingletonSet NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Submodule.Quotient.module' Polynomial.ring CommRing.toRing Ring.toAddCommGroup Semiring.toModule Algebra.toSMul Polynomial.algebraOfAlgebra Algebra.id Polynomial.module IsScalarTower.right	—	finite_adjoinRoot
free_adjoinRoot 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring	Module.Free AdjoinRoot NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AdjoinRoot.instCommRing Algebra.toModule AdjoinRoot.instAlgebra Algebra.id	—	Module.Free.of_basis
free_quotient 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring	Module.Free HasQuotient.Quotient Polynomial Ideal Polynomial.semiring Ideal.instHasQuotient_1 Polynomial.commRing Ideal.span Set Set.instSingletonSet NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Submodule.Quotient.module' Polynomial.ring CommRing.toRing Ring.toAddCommGroup Semiring.toModule Algebra.toSMul Polynomial.algebraOfAlgebra Algebra.id Polynomial.module IsScalarTower.right	—	free_adjoinRoot

PowerBasis

Definitions

Name	Category	Theorems
quotientEquivQuotientMinpolyMap 📖	CompOp	4 math math: quotientEquivQuotientMinpolyMap_apply, quotientEquivQuotientMinpolyMap_apply_mk, quotientEquivQuotientMinpolyMap_symm_apply_mk, quotientEquivQuotientMinpolyMap_symm_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
quotientEquivQuotientMinpolyMap_apply 📖	mathematical	—	DFunLike.coe AlgEquiv HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap Polynomial Ideal.Quotient.semiring Polynomial.semiring Polynomial.commRing Ideal.Quotient.commRing Ideal.span Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 Set Set.instSingletonSet Polynomial.map minpoly gen Ideal.instAlgebraQuotient Polynomial.algebraOfAlgebra Algebra.id AlgEquiv.instFunLike quotientEquivQuotientMinpolyMap RingEquiv AdjoinRoot AdjoinRoot.instCommRing AdjoinRoot.of Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toAdd EquivLike.toFunLike RingEquiv.instEquivLike AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot Ideal.quotientMap RingHomClass.toRingHom NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing RingEquiv.symm RingEquivClass.toRingEquiv AdjoinRoot.instAlgebra AlgEquiv.instEquivLike AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass AdjoinRoot.equiv'	—	Ideal.instIsTwoSided_1
quotientEquivQuotientMinpolyMap_apply_mk 📖	mathematical	—	DFunLike.coe AlgEquiv HasQuotient.Quotient Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap Polynomial Ideal.Quotient.semiring Polynomial.semiring Polynomial.commRing Ideal.Quotient.commRing Ideal.span Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 Set Set.instSingletonSet Polynomial.map minpoly gen Ideal.instAlgebraQuotient Polynomial.algebraOfAlgebra Algebra.id AlgEquiv.instFunLike quotientEquivQuotientMinpolyMap AlgHom AlgHom.funLike Polynomial.aeval Polynomial.ring Ideal.Quotient.instRingQuotient	—	Ideal.instIsTwoSided_1 quotientEquivQuotientMinpolyMap.eq_1 AlgEquiv.trans_apply AlgEquiv.ofRingEquiv_apply AlgEquiv.coe_ringEquiv' AdjoinRoot.equiv'_symm_apply lift_aeval AdjoinRoot.aeval_eq
quotientEquivQuotientMinpolyMap_symm_apply 📖	mathematical	—	DFunLike.coe AlgEquiv HasQuotient.Quotient Polynomial Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.Quotient.semiring Polynomial.semiring Polynomial.commRing Ideal.Quotient.commRing Ideal.span Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 Set Set.instSingletonSet Polynomial.map minpoly gen Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap Ideal.instAlgebraQuotient Polynomial.algebraOfAlgebra Algebra.id AlgEquiv.instFunLike AlgEquiv.symm quotientEquivQuotientMinpolyMap MulEquiv AdjoinRoot AdjoinRoot.instCommRing AdjoinRoot.of Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring EquivLike.toFunLike MulEquiv.instEquivLike MulEquiv.symm MulEquivClass.toMulEquiv RingEquiv Distrib.toAdd RingEquiv.instEquivLike RingEquivClass.toMulEquivClass RingEquiv.instRingEquivClass RingEquivClass.toRingEquiv AdjoinRoot.instAlgebra AlgEquiv.instEquivLike AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass AlgEquiv.ofRingEquiv Ideal.quotientEquiv RingEquiv.symm AdjoinRoot.equiv' AdjoinRoot.quotEquivQuotMap	—	Ideal.instIsTwoSided_1
quotientEquivQuotientMinpolyMap_symm_apply_mk 📖	mathematical	—	DFunLike.coe AlgEquiv HasQuotient.Quotient Polynomial Ideal CommSemiring.toSemiring CommRing.toCommSemiring Ideal.instHasQuotient_1 Ideal.Quotient.semiring Polynomial.semiring Polynomial.commRing Ideal.Quotient.commRing Ideal.span Ring.toSemiring CommRing.toRing Ideal.instHasQuotient Ideal.Quotient.ring Ideal.instIsTwoSided_1 Set Set.instSingletonSet Polynomial.map minpoly gen Ideal.map RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap Ideal.instAlgebraQuotient Polynomial.algebraOfAlgebra Algebra.id AlgEquiv.instFunLike AlgEquiv.symm quotientEquivQuotientMinpolyMap Polynomial.ring Ideal.Quotient.instRingQuotient AlgHom AlgHom.funLike Polynomial.aeval	—	Ideal.instIsTwoSided_1 AlgEquivClass.toRingEquivClass AlgEquiv.instAlgEquivClass RingEquivClass.toRingHomClass RingEquiv.instRingEquivClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass RingHom.instRingHomClass

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
finrank_quotient_span_eq_natDegree 📖	mathematical	—	Module.finrank HasQuotient.Quotient Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Ideal Polynomial.semiring Ideal.instHasQuotient_1 Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain Ideal.span Set Set.instSingletonSet NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Ideal.Quotient.commRing Submodule.Quotient.module' Polynomial.ring DivisionRing.toRing Field.toDivisionRing Ring.toAddCommGroup Semiring.toModule Algebra.toSMul Semifield.toCommSemiring Polynomial.algebraOfAlgebra Algebra.id Polynomial.module IsScalarTower.right Polynomial.natDegree	—	IsScalarTower.right Polynomial.natDegree_zero LinearEquiv.finrank_eq LinearMap.IsScalarTower.compatibleSMul Ideal.Quotient.isScalarTower Ideal.span_singleton_zero Module.finrank_of_not_finite IsNoetherianRing.strongRankCondition IsLocalRing.toNontrivial Field.instIsLocalRing PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain Polynomial.instFree Polynomial.not_finite PowerBasis.finrank AdjoinRoot.powerBasis_dim

---

← Back to Index