AsPolynomial

📁 Source: Mathlib/FieldTheory/RatFunc/AsPolynomial.lean

Statistics

Metric	Count
Definitions idealX, C, X, eval, instValuedWithZeroMultiplicativeInt	5
Theorems idealX_span, valuation_X_eq_neg_one, valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X, valuation_aeval_monomial_eq_valuation_pow, valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X, valuation_inv_monomial_eq_valuation_X_zpow, valuation_le_one_of_valuation_X_le_one, valuation_monomial_eq_valuation_X_pow, valuation_of_mk, C_injective, X_ne_zero, aeval_X_left_eq_algebraMap, algebraMap_C, algebraMap_X, algebraMap_comp_C, algebraMap_eq_C, algebraMap_monomial, denom_C, denom_X, eq_C_iff, eval_C, eval_X, eval_add, eval_algebraMap, eval_eq_zero_of_eval₂_denom_eq_zero, eval_mul, eval_one, eval_zero, eval₂_denom_ne_zero, liftRingHom_C, liftRingHom_X, num_C, num_X, smul_eq_C_mul, transcendental, transcendental_X, v_def	37
Total	42

Polynomial

Definitions

Name	Category	Theorems
idealX 📖	CompOp	16 math math: idealX_span, LaurentSeries.LaurentSeriesRingEquiv_def, valuation_of_mk, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, PowerSeries.intValuation_eq_of_coe, RatFunc.valuation_eq_LaurentSeries_valuation, LaurentSeries.coe_X_compare, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, RatFunc.v_def, LaurentSeries.powerSeries_ext_subring, LaurentSeries.powerSeriesRingEquiv_coe_apply, LaurentSeries.valuation_compare, LaurentSeries.tendsto_valuation, LaurentSeries.ratfuncAdicComplRingEquiv_apply, LaurentSeries.mem_integers_of_powerSeries, valuation_X_eq_neg_one

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
idealX_span 📖	mathematical	—	IsDedekindDomain.HeightOneSpectrum.asIdeal Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield commRing EuclideanDomain.toCommRing Field.toEuclideanDomain idealX Ideal.span semiring Set Set.instSingletonSet X	—	—
valuation_X_eq_neg_one 📖	mathematical	—	DFunLike.coe Valuation RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield Valuation.instFunLike IsDedekindDomain.HeightOneSpectrum.valuation Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring commRing IsPrincipalIdealRing.isDedekindDomain instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd AddGroup.toAddCancelMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne EuclideanDomain.to_principal_ideal_domain instEuclideanDomain RatFunc.instAlgebraOfPolynomial CommRing.toCommSemiring Algebra.id RatFunc.instIsFractionRingPolynomial idealX RatFunc.X WithZero.exp	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing instIsDomain IsPrincipalIdealRing.isDedekindDomain instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd EuclideanDomain.to_principal_ideal_domain RatFunc.instIsFractionRingPolynomial RatFunc.algebraMap_X IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap IsDedekindDomain.HeightOneSpectrum.intValuation_singleton X_ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing idealX_span
valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X 📖	mathematical	DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder	AlgHom Polynomial semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval Monoid.toNatPow MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero natDegree	—	valuation_aeval_monomial_eq_valuation_pow leadingCoeff_ne_zero as_sum_range map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass Valuation.map_sum_eq_of_lt IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Nat.instZeroLEOneClass map_mul NonUnitalAlgSemiHomClass.toMulHomClass aeval_C map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass aeval_X MonoidHomClass.toMulHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass map_zero MonoidWithZeroHomClass.toZeroHomClass RingHom.instRingHomClass MulZeroClass.zero_mul one_mul pow_pos LinearOrderedCommMonoidWithZero.toPosMulStrictMono LinearOrderedCommMonoidWithZero.toZeroLeOneClass lt_trans zero_lt_one NeZero.one GroupWithZero.toNontrivial pow_lt_pow_right₀
valuation_aeval_monomial_eq_valuation_pow 📖	mathematical	DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.instFunLike algebraMap InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	AlgHom Polynomial semiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial Monoid.toNatPow MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero	—	map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass aeval_C map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass aeval_X MonoidHomClass.toMulHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass one_mul
valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X 📖	mathematical	DFunLike.coe Valuation RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield Valuation.instFunLike RatFunc.coePolynomial RingHom Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Semiring.toNonAssocSemiring semiring RingHom.instFunLike C InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder RatFunc.X	Monoid.toNatPow MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero natDegree	—	instIsDomain RatFunc.X.eq_1 aeval_X_left_apply aeval_algebraMap_apply RatFunc.instIsScalarTowerPolynomial valuation_aeval_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X
valuation_inv_monomial_eq_valuation_X_zpow 📖	mathematical	DFunLike.coe Valuation RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield Valuation.instFunLike RatFunc.coePolynomial RingHom Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Semiring.toNonAssocSemiring semiring RingHom.instFunLike C InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	RatFunc.instDiv RatFunc.instOne LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid CommGroupWithZero.toGroupWithZero RatFunc.X	—	instIsDomain one_div map_inv₀ ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass zpow_neg zpow_natCast valuation_monomial_eq_valuation_X_pow
valuation_le_one_of_valuation_X_le_one 📖	—	DFunLike.coe Valuation RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield Valuation.instFunLike RatFunc.coePolynomial RingHom Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Semiring.toNonAssocSemiring semiring RingHom.instFunLike C InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder RatFunc.X	—	—	instIsDomain as_sum_range RatFunc.coePolynomial.eq_1 map_sum RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Valuation.map_sum_le Nat.instNoMaxOrder monomial_zero_right map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass valuation_monomial_eq_valuation_X_pow IsOrderedMonoid.toMulLeftMono LinearOrderedCommMonoidWithZero.toIsOrderedMonoid
valuation_monomial_eq_valuation_X_pow 📖	mathematical	DFunLike.coe Valuation RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield Valuation.instFunLike RatFunc.coePolynomial RingHom Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Semiring.toNonAssocSemiring semiring RingHom.instFunLike C InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial Monoid.toNatPow MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero RatFunc.X	—	instIsDomain map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass MonoidHomClass.toMulHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass one_mul
valuation_of_mk 📖	mathematical	—	DFunLike.coe Valuation RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero Multiplicative WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Int.instAddCommMonoid Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedCancelMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield Valuation.instFunLike IsDedekindDomain.HeightOneSpectrum.valuation Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring commRing IsPrincipalIdealRing.isDedekindDomain instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd AddGroup.toAddCancelMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne EuclideanDomain.to_principal_ideal_domain instEuclideanDomain RatFunc.instAlgebraOfPolynomial CommRing.toCommSemiring Algebra.id RatFunc.instIsFractionRingPolynomial idealX WithZero.div Multiplicative.div CommRing.toRing IsDedekindDomain.HeightOneSpectrum.intValuation	—	Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing instIsDomain IsPrincipalIdealRing.isDedekindDomain instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd EuclideanDomain.to_principal_ideal_domain RatFunc.instIsFractionRingPolynomial mem_nonZeroDivisors_iff_ne_zero instNoZeroDivisors IsDomain.to_noZeroDivisors nontrivial IsDomain.toNontrivial RatFunc.mk_eq_mk' IsDedekindDomain.HeightOneSpectrum.valuation_of_mk'

RatFunc

Definitions

Name	Category	Theorems
C 📖	CompOp	16 math math: laurent_X, num_C, smul_eq_C_mul, intDegree_C, algebraMap_eq_C, eval_C, algebraMap_C, liftRingHom_C, laurent_C, denom_C, C_injective, eq_C_iff, FunctionField.inftyValuation.C, algebraMap_monomial, Polynomial.residueFieldMapCAlgEquiv_symm_C, algebraMap_comp_C
X 📖	CompOp	19 math math: laurent_X, transcendental_X, FunctionField.inftyValuation.X_inv, coe_X, eval_X, Polynomial.valuation_inv_monomial_eq_valuation_X_zpow, algebraMap_X, LaurentSeries.coe_X_compare, num_X, denom_X, FunctionField.inftyValuation.X_zpow, FunctionField.inftyValuation.X, Polynomial.valuation_monomial_eq_valuation_X_pow, liftRingHom_X, intDegree_X, aeval_X_left_eq_algebraMap, Polynomial.residueFieldMapCAlgEquiv_symm_X, algebraMap_monomial, Polynomial.valuation_X_eq_neg_one
eval 📖	CompOp	8 math math: eval_mul, eval_one, eval_X, eval_eq_zero_of_eval₂_denom_eq_zero, eval_C, eval_add, eval_zero, eval_algebraMap
instValuedWithZeroMultiplicativeInt 📖	CompOp	12 math math: LaurentSeries.LaurentSeriesRingEquiv_def, LaurentSeries.inducing_coe, LaurentSeries.continuous_coe, LaurentSeries.valuation_LaurentSeries_equal_extension, v_def, LaurentSeries.LaurentSeries_coe, LaurentSeries.valuation_coe_ratFunc, LaurentSeries.valuation_compare, LaurentSeries.tendsto_valuation, LaurentSeries.comparePkg_eq_extension, LaurentSeries.ratfuncAdicComplRingEquiv_apply, LaurentSeries.exists_ratFunc_eq_v

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
C_injective 📖	mathematical	—	RatFunc DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField RingHom.instFunLike C	—	algebraMap_comp_C RingHom.coe_comp algebraMap_injective Polynomial.C_injective
X_ne_zero 📖	—	—	—	—	algebraMap_ne_zero instIsDomain Polynomial.X_ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing
aeval_X_left_eq_algebraMap 📖	mathematical	—	DFunLike.coe AlgHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring RatFunc Polynomial.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField Polynomial.algebraOfAlgebra Algebra.id instAlgebraOfPolynomial AlgHom.funLike Polynomial.aeval X RingHom Semiring.toNonAssocSemiring Polynomial.commSemiring RingHom.instFunLike algebraMap	—	Polynomial.induction_on' map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass Polynomial.aeval_monomial algebraMap_monomial
algebraMap_C 📖	mathematical	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring RatFunc Semiring.toNonAssocSemiring Polynomial.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id Polynomial.semiring Polynomial.C C	—	—
algebraMap_X 📖	mathematical	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring RatFunc Semiring.toNonAssocSemiring Polynomial.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id Polynomial.X X	—	—
algebraMap_comp_C 📖	mathematical	—	RingHom.comp Polynomial CommSemiring.toSemiring CommRing.toCommSemiring RatFunc Semiring.toNonAssocSemiring Polynomial.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField algebraMap instAlgebraOfPolynomial Algebra.id Polynomial.C C	—	—
algebraMap_eq_C 📖	mathematical	—	algebraMap RatFunc CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField instAlgebraOfPolynomial Polynomial.algebraOfAlgebra CommSemiring.toSemiring Algebra.id C	—	—
algebraMap_monomial 📖	mathematical	—	DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring RatFunc Semiring.toNonAssocSemiring Polynomial.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id LinearMap RingHom.id NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Polynomial.semiring Semiring.toModule Polynomial.module LinearMap.instFunLike Polynomial.monomial instMul C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X	—	map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
denom_C 📖	mathematical	—	denom DFunLike.coe RingHom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField instIsDomain RingHom.instFunLike C Polynomial Polynomial.instOne	—	denom_algebraMap
denom_X 📖	mathematical	—	denom X EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Polynomial.instOne	—	denom_algebraMap
eq_C_iff 📖	mathematical	—	DFunLike.coe RingHom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField instIsDomain RingHom.instFunLike C Polynomial.natDegree num denom	—	instIsDomain num_C Polynomial.natDegree_C denom_C Polynomial.natDegree_one Polynomial.natDegree_eq_zero num_div_denom algebraMap_C map_div₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
eval_C 📖	mathematical	—	eval DFunLike.coe RingHom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField instIsDomain RingHom.instFunLike C	—	instIsDomain num_C Polynomial.eval₂_C denom_C Polynomial.eval₂_one div_one
eval_X 📖	mathematical	—	eval X EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield	—	instIsDomain num_X Polynomial.eval₂_X denom_X Polynomial.eval₂_one div_one
eval_add 📖	mathematical	—	eval RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain instAdd Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero denom_add_dvd mul_eq_zero IsDomain.to_noZeroDivisors instIsDomain Polynomial.eval₂_mul div_add_div eq_div_iff mul_ne_zero div_eq_mul_inv mul_right_comm div_eq_iff num_denom_add
eval_algebraMap 📖	mathematical	—	eval DFunLike.coe RingHom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toNonAssocSemiring CommSemiring.toSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField instIsDomain RingHom.instFunLike algebraMap instAlgebraOfPolynomial Polynomial.eval₂ Polynomial Polynomial.semiring	—	instIsDomain IsScalarTower.algebraMap_apply instIsScalarTowerPolynomial num_algebraMap denom_algebraMap Polynomial.eval₂_one div_one
eval_eq_zero_of_eval₂_denom_eq_zero 📖	mathematical	Polynomial.eval₂ DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield denom MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	eval	—	eval.eq_1 div_zero
eval_mul 📖	mathematical	—	eval RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	Polynomial.eval₂_eq_zero_of_dvd_of_eval₂_eq_zero denom_mul_dvd mul_eq_zero IsDomain.to_noZeroDivisors instIsDomain Polynomial.eval₂_mul div_mul_div_comm eq_div_iff mul_ne_zero div_eq_mul_inv mul_right_comm div_eq_iff num_denom_mul
eval_one 📖	mathematical	—	eval RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain instOne AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing	—	num_one Polynomial.eval₂_one denom_one div_self NeZero.one IsLocalRing.toNontrivial Field.instIsLocalRing
eval_zero 📖	mathematical	—	eval RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain instZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	num_zero Polynomial.eval₂_zero denom_zero Polynomial.eval₂_one div_one
eval₂_denom_ne_zero 📖	—	—	—	—	eval_eq_zero_of_eval₂_denom_eq_zero
liftRingHom_C 📖	mathematical	Submonoid Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero Polynomial.semiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Submonoid.comap NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass	DFunLike.coe RatFunc instCommRing liftRingHom instField C Polynomial.C	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass liftRingHom_algebraMap
liftRingHom_X 📖	mathematical	Submonoid Polynomial CommSemiring.toSemiring CommRing.toCommSemiring MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero Polynomial.semiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Submonoid.comap NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass	DFunLike.coe RatFunc instCommRing liftRingHom X Polynomial.X	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass liftRingHom_algebraMap
num_C 📖	mathematical	—	num DFunLike.coe RingHom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField instIsDomain RingHom.instFunLike C Polynomial Polynomial.semiring Polynomial.C	—	num_algebraMap
num_X 📖	mathematical	—	num X EuclideanDomain.toCommRing Field.toEuclideanDomain instIsDomain Field.toSemifield Polynomial.X DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	num_algebraMap
smul_eq_C_mul 📖	mathematical	—	RatFunc instSMulOfFractionRingPolynomial OreLocalization.instSMulOfIsScalarTower Polynomial CommSemiring.toSemiring CommRing.toCommSemiring CommMonoid.toMonoid CommRing.toCommMonoid Polynomial.commRing nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm Monoid.toMulAction Algebra.toSMul Polynomial.semiring Polynomial.algebraOfAlgebra Algebra.id IsScalarTower.right instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField RingHom.instFunLike C	—	IsScalarTower.right Algebra.smul_def algebraMap_eq_C
transcendental 📖	mathematical	—	Algebra.Transcendental RatFunc DivisionRing.toRing Field.toDivisionRing instField instAlgebraOfPolynomial CommRing.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring Algebra.id	—	transcendental_X
transcendental_X 📖	mathematical	—	Transcendental RatFunc DivisionRing.toRing Field.toDivisionRing instField instAlgebraOfPolynomial CommRing.toCommSemiring Polynomial.algebraOfAlgebra CommSemiring.toSemiring Algebra.id X	—	algebraMap_X transcendental_algebraMap_iff instIsScalarTowerPolynomial algebraMap_injective Polynomial.transcendental_X
v_def 📖	mathematical	—	DFunLike.coe Valuation RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero Multiplicative LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid DivisionRing.toRing Field.toDivisionRing instField instIsDomain Field.toSemifield Valuation.instFunLike Valued.v instValuedWithZeroMultiplicativeInt WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring Int.instIsStrictOrderedRing IsDedekindDomain.HeightOneSpectrum.valuation Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Polynomial.commRing IsPrincipalIdealRing.isDedekindDomain Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd AddGroup.toAddCancelMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne EuclideanDomain.to_principal_ideal_domain Polynomial.instEuclideanDomain instAlgebraOfPolynomial CommRing.toCommSemiring Algebra.id instIsFractionRingPolynomial Polynomial.idealX	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid instIsDomain

---

← Back to Index