AsPolynomial

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

Statistics

Metric	Count
Definitions idealX, C, X, algEquivOfTranscendental, eval, valuedRatFunc	6
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, algEquivOfTranscendental_X, algEquivOfTranscendental_algebraMap, algEquivOfTranscendental_apply, algEquivOfTranscendental_symm_aeval, algEquivOfTranscendental_symm_gen, algebraMap_C, algebraMap_X, algebraMap_comp_C, algebraMap_eq_C, algebraMap_monomial, coePolynomial_eq_algebraMap, 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, valuation_surjective	44
Total	50

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, LaurentSeries.coe_X_compare, LaurentSeries.exists_powerSeries_of_memIntegers, 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring instLatticeInt 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	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero DFunLike.coe Valuation DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike	DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Field.toDivisionRing Valuation.instFunLike AlgHom Polynomial CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval Monoid.toPow MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero 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 instIsLeftCancelAddOfAddLeftReflectLE IsOrderedCancelAddMonoid.toAddLeftReflectLE Nat.instIsOrderedCancelAddMonoid IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Nat.instNoMaxOrder Nat.instCanonicallyOrderedAdd 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 Valuation.IsTrivialOn.eq_one 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 AlgHom Polynomial CommSemiring.toSemiring Semifield.toCommSemiring Field.toSemifield semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring algebraOfAlgebra Algebra.id AlgHom.funLike aeval LinearMap RingHom.id Semiring.toNonAssocSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toModule module LinearMap.instFunLike monomial Monoid.toPow MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	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 Valuation.IsTrivialOn.eq_one one_mul
valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X 📖	mathematical	Preorder.toLT PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero DFunLike.coe Valuation RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield Valuation.instFunLike RatFunc.X	DFunLike.coe Valuation RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield Valuation.instFunLike RatFunc.coePolynomial Monoid.toPow MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero RatFunc.X natDegree DivisionSemiring.toSemiring Semifield.toDivisionSemiring	—	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.instDiv RatFunc.instOne RatFunc.coePolynomial LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Semiring.toModule module LinearMap.instFunLike monomial DivInvMonoid.toZPow GroupWithZero.toDivInvMonoid CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero RatFunc.X	—	instIsDomain RatFunc.algebraMap_monomial one_div mul_inv_rev map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass map_inv₀ map_pow Valuation.IsTrivialOn.eq_one inv_one mul_one zpow_neg zpow_natCast
valuation_le_one_of_valuation_X_le_one 📖	mathematical	Preorder.toLE PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder LinearOrderedCommMonoidWithZero.toLinearOrder LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield Valuation.instFunLike RatFunc.X 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 LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero DFunLike.coe Valuation RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing RatFunc.instField instIsDomain Field.toSemifield Valuation.instFunLike RatFunc.coePolynomial InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid LinearOrderedCommGroupWithZero.toCommGroupWithZero	—	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 RatFunc.algebraMap_monomial map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass Valuation.IsTrivialOn.eq_one map_pow one_mul 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 LinearMap DivisionSemiring.toSemiring Semifield.toDivisionSemiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring Semiring.toModule module LinearMap.instFunLike monomial Monoid.toPow MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero LinearOrderedCommGroupWithZero.toCommGroupWithZero RatFunc.X	—	instIsDomain RatFunc.algebraMap_monomial map_mul MonoidHomClass.toMulHomClass MonoidWithZeroHomClass.toMonoidHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass Valuation.IsTrivialOn.eq_one map_pow 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring instLatticeInt 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	20 math math: laurent_X, eq_C_of_minpolyX_coeff_eq_zero, num_C, smul_eq_C_mul, intDegree_C, Luroth.generator_ne_C, algebraMap_eq_C, eval_C, algebraMap_C, liftRingHom_C, minpolyX_eq_zero_iff, laurent_C, denom_C, C_injective, eq_C_iff, FunctionField.inftyValuation.C, C_minpolyX, algebraMap_monomial, Polynomial.residueFieldMapCAlgEquiv_symm_C, algebraMap_comp_C
X 📖	CompOp	29 math math: algEquivOfTranscendental_X, laurent_X, transcendental_X, FunctionField.inftyValuation.X_inv, IntermediateField.adjoin_X, coe_X, IntermediateField.isAlgebraic_X, eval_X, adjoin_X, algEquivOfTranscendental_symm_gen, Polynomial.valuation_inv_monomial_eq_valuation_X_zpow, Polynomial.valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X, algebraMap_X, LaurentSeries.coe_X_compare, minpolyX_aeval_X, num_X, Luroth.algEquiv_X, denom_X, FunctionField.inftyValuation.X_zpow, FunctionField.inftyValuation.X, Polynomial.valuation_monomial_eq_valuation_X_pow, valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X, liftRingHom_X, intDegree_X, aeval_X_left_eq_algebraMap, Polynomial.residueFieldMapCAlgEquiv_symm_X, algebraMap_monomial, isAlgebraic_adjoin_simple_X, Polynomial.valuation_X_eq_neg_one
algEquivOfTranscendental 📖	CompOp	5 math math: algEquivOfTranscendental_X, algEquivOfTranscendental_symm_gen, algEquivOfTranscendental_symm_aeval, algEquivOfTranscendental_algebraMap, algEquivOfTranscendental_apply
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
valuedRatFunc 📖	CompOp	8 math math: LaurentSeries.inducing_coe, LaurentSeries.continuous_coe, valuation_surjective, v_def, LaurentSeries.valuation_coe_ratFunc, LaurentSeries.tendsto_valuation, LaurentSeries.exists_ratFunc_eq_v, LaurentSeries.uniformContinuous_withVal_equiv

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
algEquivOfTranscendental_X 📖	mathematical	Transcendental EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet DFunLike.coe AlgEquiv RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring instField instIsDomain IntermediateField.toField instAlgebraOfPolynomial Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id IntermediateField.algebra' Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule AlgEquiv.instFunLike algEquivOfTranscendental X	—	instIsDomain IsScalarTower.left algEquivOfTranscendental_algebraMap Polynomial.aeval_X
algEquivOfTranscendental_algebraMap 📖	mathematical	Transcendental EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	DFunLike.coe AlgEquiv RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring instField instIsDomain IntermediateField.toField instAlgebraOfPolynomial Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id IntermediateField.algebra' Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule AlgEquiv.instFunLike algEquivOfTranscendental RingHom Polynomial Semiring.toNonAssocSemiring Polynomial.commSemiring RingHom.instFunLike algebraMap AlgHom Polynomial.semiring AlgHom.funLike Polynomial.aeval IntermediateField.AdjoinSimple.gen	—	instIsDomain IsScalarTower.left Algebra.self_mem_adjoin_singleton IsFractionRing.algEquivOfAlgEquiv_algebraMap Polynomial.coe_aeval_mk_apply IntermediateField.AdjoinSimple.coe_aeval_gen_apply
algEquivOfTranscendental_apply 📖	mathematical	Transcendental EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet DFunLike.coe AlgEquiv RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring instField instIsDomain IntermediateField.toField instAlgebraOfPolynomial Polynomial.algebraOfAlgebra CommSemiring.toSemiring CommRing.toCommSemiring Algebra.id IntermediateField.algebra' Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule AlgEquiv.instFunLike algEquivOfTranscendental DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing AlgHom Polynomial Polynomial.semiring AlgHom.funLike Polynomial.aeval num denom	—	instIsDomain IsScalarTower.left num_div_denom map_div₀ RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass algEquivOfTranscendental_algebraMap IntermediateField.AdjoinSimple.coe_aeval_gen_apply
algEquivOfTranscendental_symm_aeval 📖	mathematical	Transcendental EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	DFunLike.coe AlgEquiv IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.toField instField instIsDomain IntermediateField.algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule instAlgebraOfPolynomial Polynomial.algebraOfAlgebra CommRing.toCommSemiring AlgEquiv.instFunLike AlgEquiv.symm algEquivOfTranscendental AlgHom Polynomial Polynomial.semiring AlgHom.funLike Polynomial.aeval IntermediateField.AdjoinSimple.gen RingHom Semiring.toNonAssocSemiring Polynomial.commSemiring RingHom.instFunLike algebraMap	—	instIsDomain IsScalarTower.left Algebra.self_mem_adjoin_singleton Polynomial.aeval_algebraMap_apply IntermediateField.algebraAdjoinAdjoin.instIsScalarTowerSubtypeMemSubalgebraAdjoinAdjoin IsFractionRing.algEquivOfAlgEquiv_algebraMap Polynomial.algEquivOfTranscendental_symm_aeval
algEquivOfTranscendental_symm_gen 📖	mathematical	Transcendental EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionRing.toRing Field.toDivisionRing	DFunLike.coe AlgEquiv IntermediateField SetLike.instMembership IntermediateField.instSetLike IntermediateField.adjoin Set Set.instSingletonSet RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Semifield.toCommSemiring Field.toSemifield DivisionSemiring.toSemiring Semifield.toDivisionSemiring IntermediateField.toField instField instIsDomain IntermediateField.algebra' Algebra.toSMul CommSemiring.toSemiring Algebra.id IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Algebra.toModule instAlgebraOfPolynomial Polynomial.algebraOfAlgebra CommRing.toCommSemiring AlgEquiv.instFunLike AlgEquiv.symm algEquivOfTranscendental IntermediateField.AdjoinSimple.gen X	—	instIsDomain IsScalarTower.left Algebra.self_mem_adjoin_singleton IsFractionRing.algEquivOfAlgEquiv_algebraMap Polynomial.algEquivOfTranscendental_symm_gen
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.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero X	—	map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
coePolynomial_eq_algebraMap 📖	mathematical	—	coePolynomial 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	—	—
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 MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing EuclideanDomain.toCommRing Field.toEuclideanDomain	—	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 RingHom RatFunc Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike liftRingHom instField C Polynomial Polynomial.semiring 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 RingHom RatFunc Semiring.toNonAssocSemiring CommSemiring.toSemiring CommRing.toCommSemiring instCommRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike liftRingHom X Polynomial Polynomial.semiring 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 PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid DivisionRing.toRing Field.toDivisionRing instField instIsDomain Field.toSemifield Valuation.instFunLike Valued.v valuedRatFunc WithZero.instLinearOrderedCommMonoidWithZero Multiplicative.commMonoid Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instSemiring instLatticeInt 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
valuation_surjective 📖	mathematical	—	RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain WithZero Multiplicative DFunLike.coe Valuation LinearOrderedCommGroupWithZero.toLinearOrderedCommMonoidWithZero WithZero.instLinearOrderedCommGroupWithZero Multiplicative.commGroup Int.instAddCommGroup Multiplicative.linearOrder Int.instLinearOrder Multiplicative.isOrderedMonoid Int.instAddCommMonoid PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder Int.instIsOrderedAddMonoid DivisionRing.toRing Field.toDivisionRing instField instIsDomain Field.toSemifield Valuation.instFunLike Valued.v valuedRatFunc	—	Multiplicative.isOrderedMonoid Int.instIsOrderedAddMonoid instIsDomain map_zero Multiplicative.isOrderedCancelMonoid IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing MonoidWithZeroHomClass.toZeroHomClass ValuationClass.toMonoidWithZeroHomClass Valuation.instValuationClass IsPrincipalIdealRing.isDedekindDomain Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd EuclideanDomain.to_principal_ideal_domain instIsFractionRingPolynomial zpow_neg map_inv₀ map_zpow₀ Polynomial.valuation_X_eq_neg_one inv_zpow' mul_one WithZero.exp_log inv_inv

---

← Back to Index