Defs

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

Statistics

Metric	Count
Definitions RatFunc, liftOn, liftOn', mk, toFractionRing, «term_⟮X⟯»	6
Theorems induction_on', liftOn'_def, liftOn'_mk, liftOn_condition_of_liftOn'_condition, liftOn_def, liftOn_mk, liftOn_ofFractionRing_mk, mk_coe_def, mk_def, mk_def_of_mem, mk_def_of_ne, mk_eq_div', mk_eq_localization_mk, mk_eq_mk, mk_one', mk_zero, ofFractionRing_injective, toFractionRing_inj, toFractionRing_injective	19
Total	25

RatFunc

Definitions

Name	Category	Theorems
liftOn 📖	CompOp	5 math math: liftOn_ofFractionRing_mk, liftOn_div, liftOn_def, liftOn'_def, liftOn_mk
liftOn' 📖	CompOp	3 math math: liftOn'_div, liftOn'_mk, liftOn'_def
mk 📖	CompOp	—
toFractionRing 📖	CompOp	7 math math: toFractionRing_injective, toFractionRing_inj, toFractionRing_smul, liftOn_def, toFractionRingRingEquiv_apply, toFractionRingAlgEquiv_apply, toFractionRing_eq
«term_⟮X⟯» 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
induction_on' 📖	—	—	—	—	Localization.induction_on Localization.isLocalization Localization.mk_eq_mk' mk_coe_def mem_nonZeroDivisors_iff_ne_zero Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors Polynomial.nontrivial IsDomain.toNontrivial
liftOn'_def 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instMul	liftOn' liftOn	—	—
liftOn'_mk 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instZero Polynomial.instOne Polynomial.instMul	liftOn'	—	liftOn'_def liftOn_condition_of_liftOn'_condition nonZeroDivisors.ne_zero Polynomial.nontrivial IsDomain.toNontrivial
liftOn_condition_of_liftOn'_condition 📖	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instMul	—	—	mul_comm
liftOn_def 📖	mathematical	—	liftOn Localization.liftOn Polynomial CommSemiring.toSemiring CommRing.toCommSemiring CommRing.toCommMonoid Polynomial.commRing nonZeroDivisors Semiring.toMonoidWithZero toFractionRing Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike	—	—
liftOn_mk 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instZero Polynomial.instOne nonZeroDivisors.ne_zero Semiring.toMonoidWithZero Polynomial.semiring Polynomial.nontrivial IsDomain.toNontrivial	liftOn	—	liftOn.congr_simp mk_zero Localization.mk_zero mem_nonZeroDivisors_iff_ne_zero Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors Polynomial.nontrivial IsDomain.toNontrivial
liftOn_ofFractionRing_mk 📖	mathematical	—	liftOn ofFractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring CommRing.toCommMonoid Polynomial.commRing nonZeroDivisors Semiring.toMonoidWithZero Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Polynomial.semiring SetLike.instMembership Submonoid.instSetLike	—	liftOn_def
mk_coe_def 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero Polynomial.semiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors ofFractionRing IsLocalization.mk' Polynomial.commSemiring FractionRing Polynomial.commRing OreLocalization.instCommSemiring OreLocalization.oreSetComm CommRing.toCommMonoid OreLocalization.instAlgebra Algebra.id Localization.isLocalization	—	Localization.isLocalization Polynomial.nontrivial IsDomain.toNontrivial Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd mk_eq_div' FractionRing.mk_eq_div
mk_def 📖	mathematical	—	ofFractionRing FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid OreLocalization.instDivisionRingNonZeroDivisors Polynomial.ring CommRing.toRing OreLocalization.oreSetComm CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.commSemiring OreLocalization.instSemiring RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id	—	—
mk_def_of_mem 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero Polynomial.semiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors	ofFractionRing IsLocalization.mk' Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commSemiring nonZeroDivisors Semiring.toMonoidWithZero Polynomial.semiring FractionRing Polynomial.commRing OreLocalization.instCommSemiring OreLocalization.oreSetComm CommRing.toCommMonoid OreLocalization.instAlgebra Algebra.id Localization.isLocalization Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike	—	Localization.isLocalization
mk_def_of_ne 📖	mathematical	—	ofFractionRing IsLocalization.mk' Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commSemiring nonZeroDivisors Semiring.toMonoidWithZero Polynomial.semiring FractionRing Polynomial.commRing OreLocalization.instCommSemiring OreLocalization.oreSetComm CommRing.toCommMonoid OreLocalization.instAlgebra Algebra.id Localization.isLocalization Submonoid MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring SetLike.instMembership Submonoid.instSetLike MonoidWithZero.toMulZeroOneClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass mem_nonZeroDivisors_iff_ne_zero Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors Polynomial.nontrivial IsDomain.toNontrivial	—	mk_def_of_mem mem_nonZeroDivisors_iff_ne_zero Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors Polynomial.nontrivial IsDomain.toNontrivial
mk_eq_div' 📖	mathematical	—	ofFractionRing FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid OreLocalization.instDivisionRingNonZeroDivisors Polynomial.ring CommRing.toRing Polynomial.nontrivial IsDomain.toNontrivial Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors OreLocalization.oreSetComm CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.commSemiring OreLocalization.instSemiring RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id	—	Polynomial.nontrivial IsDomain.toNontrivial Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors mk_def
mk_eq_localization_mk 📖	mathematical	—	ofFractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring CommRing.toCommMonoid Polynomial.commRing nonZeroDivisors Semiring.toMonoidWithZero Submonoid Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass MulZeroClass.toZero MulZeroOneClass.toMulZeroClass mem_nonZeroDivisors_iff_ne_zero Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors Polynomial.nontrivial IsDomain.toNontrivial	—	mem_nonZeroDivisors_iff_ne_zero Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors Polynomial.nontrivial IsDomain.toNontrivial Localization.isLocalization mk_def_of_ne Localization.mk_eq_mk'
mk_eq_mk 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instMul	—	Localization.isLocalization mem_nonZeroDivisors_iff_ne_zero Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors Polynomial.nontrivial IsDomain.toNontrivial mk_def_of_ne ofFractionRing_injective IsLocalization.mk'_eq_iff_eq' IsFractionRing.injective
mk_one' 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instOne ofFractionRing DFunLike.coe RingHom FractionRing Polynomial.commRing Semiring.toNonAssocSemiring Polynomial.commSemiring OreLocalization.instSemiring nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm CommRing.toCommMonoid RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id	—	Localization.isLocalization IsLocalization.mk'_one mk_coe_def Submonoid.coe_one
mk_zero 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instZero ofFractionRing FractionRing Polynomial.commRing OreLocalization.instZero CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm Monoid.toMulAction	—	Polynomial.nontrivial IsDomain.toNontrivial Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors mk_eq_div' map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass div_zero
ofFractionRing_injective 📖	mathematical	—	FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing RatFunc ofFractionRing	—	—
toFractionRing_inj 📖	mathematical	—	toFractionRing	—	toFractionRing_injective
toFractionRing_injective 📖	mathematical	—	RatFunc FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing toFractionRing	—	—

(root)

Definitions

Name	Category	Theorems
RatFunc 📖	CompData	241 math math: RatFunc.eval_mul, RatFunc.laurent_injective, RatFunc.ofFractionRing_mk', RatFunc.liftMonoidWithZeroHom_apply, RatFunc.toFractionRing_injective, RatFunc.num_div, RatFunc.coe_mapAlgHom_eq_coe_map, RatFunc.algEquivOfTranscendental_X, RatFunc.num_div_dvd, RatFunc.liftMonoidWithZeroHom_apply_ofFractionRing_mk, RatFunc.laurent_X, RatFunc.num_one, RatFunc.smul_def, LaurentSeries.LaurentSeriesRingEquiv_def, RatFunc.transcendental_X, RatFunc.exists_zpow_uniformizingPolynomial, RatFunc.denom_one, RatFunc.intDegree_div, RatFunc.denom_mul_dvd, FunctionField.inftyValuation.X_inv, RatFunc.map_apply_ofFractionRing_mk, RatFunc.laurent_algebraMap, RatFunc.irreducible_min_polynomial_valuation_lt_one_and_ne_zero, RatFunc.mk_smul, RatFunc.IntermediateField.adjoin_X, FunctionField.InftyValuation.map_zero', RatFunc.laurent_div, RatFunc.valuation_isEquiv_adic_of_valuation_X_le_one, RatFunc.eval_one, RatFunc.liftAlgHom_injective, FunctionField.instIsNontrivialRatFuncWithZeroMultiplicativeIntInftyValuation, RatFunc.liftMonoidWithZeroHom_apply_div', RatFunc.map_injective, RatFunc.coe_X, FunctionField.inftyValuation.polynomial, RatFunc.Luroth.algEquiv_apply, RatFunc.coe_mapRingHom_eq_coe_map, RatFunc.coe_coe, Polynomial.valuation_of_mk, LaurentSeries.inducing_coe, RatFunc.IntermediateField.isAlgebraic_X, LaurentSeries.continuous_coe, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, RatFunc.adicValuation_not_isEquiv_infty_valuation, RatFunc.map_apply, FunctionField.instIsTrivialOnWithZeroMultiplicativeIntRatFuncInftyValuation, RatFunc.mk_eq_mk', RatFunc.instNontrivial, RatFunc.ofFractionRing_div, RatFunc.toFractionRing_smul, RatFunc.num_denom_add, RatFunc.eq_C_of_minpolyX_coeff_eq_zero, FunctionField.valuedFqtInfty.def, RatFunc.instIsFractionRingPolynomial, RatFunc.intDegree_inv, RatFunc.ofFractionRing_one, RatFunc.laurent_at_zero, RatFunc.liftRingHom_injective, RatFunc.numDenom_div, RatFunc.instIsScalarTowerOfPolynomial_1, RatFunc.num_C, FunctionField.InftyValuation.map_add_le_max', RatFunc.smul_eq_C_mul, RatFunc.laurent_laurent, LaurentSeries.exists_ratFunc_val_lt, RatFunc.num_algebraMap, RatFunc.adjoin_X, RatFunc.ofFractionRing_zero, RatFunc.ofFractionRing_add, RatFunc.valuation_isEquiv_valuationIdeal_adic_of_valuation_X_le_one, RatFunc.liftMonoidWithZeroHom_apply_div, RatFunc.Luroth.algEquiv_algebraMap, RatFunc.num_dvd, RatFunc.laurentAux_div, RatFunc.algEquivOfTranscendental_symm_gen, RatFunc.Luroth.generator_mem, RatFunc.mk_eq_div, RatFunc.valuation_surjective, Polynomial.valuation_inv_monomial_eq_valuation_X_zpow, RatFunc.num_zero, RatFunc.intDegree_mul, RatFunc.liftOn_div, Polynomial.valuation_eq_valuation_X_pow_natDegree_of_one_lt_valuation_X, RatFunc.num_inv_dvd, RatFunc.ofFractionRing_comp_algebraMap, RatFunc.algebraMap_X, RatFunc.intDegree_C, FunctionField.InftyValuation.map_one', RatFunc.num_denom_mul, RatFunc.Luroth.generator_ne_C, RatFunc.intDegree_add_le, RatFunc.smul_eq_C_smul, RatFunc.valuation_eq_LaurentSeries_valuation, RatFunc.finrank_eq_max_natDegree, RatFunc.liftRingHom_apply, RatFunc.map_apply_div, RatFunc.instIsScalarTowerOfIsDomainOfPolynomial, RatFunc.liftRingHom_apply_div', LaurentSeries.coe_X_compare, FunctionField.InftyValuation.map_mul', RatFunc.liftRingHom_ofFractionRing_algebraMap, RatFunc.laurentAux_algebraMap, RatFunc.algebraMap_eq_C, RatFunc.algebraMap_apply_div, RatFunc.div_smul, RatFunc.Luroth.eq_adjoin_generator, RatFunc.minpolyX_aeval_X, RatFunc.algEquivOfTranscendental_symm_aeval, RatFunc.eval_C, RatFunc.inv_def, RatFunc.liftRingHom_apply_div, RatFunc.faithfulSMul, Polynomial.valuation_le_one_of_valuation_X_le_one, LaurentSeries.exists_powerSeries_of_memIntegers, LaurentSeries.continuous_coe', RatFunc.algebraMap_C, RatFunc.instIsScalarTowerPolynomial, RatFunc.num_eq_zero_iff, RatFunc.ofFractionRing_smul, RatFunc.irreducible_minpolyX, RatFunc.intDegree_add, RatFunc.Luroth.algEquiv_X, RatFunc.valuation_isEquiv_infty_or_adic, RatFunc.liftAlgHom_apply_div, RatFunc.liftRingHom_C, RatFunc.natDegree_minpolyX, RatFunc.ofFractionRing_injective, RatFunc.irreducible_minpolyX', LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, RatFunc.denom_div, LaurentSeries.valuation_LaurentSeries_equal_extension, RatFunc.ofFractionRing_sub, RatFunc.intDegree_polynomial, RatFunc.v_def, RatFunc.instCharZero, LaurentSeries.LaurentSeries_coe, RatFunc.ofFractionRing_neg, RatFunc.liftMonoidWithZeroHom_injective, LaurentSeries.powerSeries_ext_subring, RatFunc.liftAlgHom_apply_ofFractionRing_mk, RatFunc.minpolyX_eq_zero_iff, RatFunc.denom_div_dvd, RatFunc.laurent_C, RatFunc.eval_add, FunctionField.inftyValuation.X_zpow, RatFunc.rank_ratFunc_ratFunc, LaurentSeries.powerSeriesRingEquiv_coe_apply, RatFunc.transcendental_of_ne_C, RatFunc.instIsScalarTowerOfPolynomial, FunctionField.inftyValuation.X, Polynomial.valuation_monomial_eq_valuation_X_pow, RatFunc.denom_inv_dvd, RatFunc.setOf_polynomial_valuation_lt_one_and_ne_zero_nonempty, FunctionField.inftyValuedFqt.def, RatFunc.liftRingHom_apply_ofFractionRing_mk, RatFunc.num_mul_dvd, RatFunc.valuation_eq_valuation_X_zpow_intDegree_of_one_lt_valuation_X, Polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebius, RatFunc.instExpChar, RatFunc.valuation_isEquiv_adic_of_not_isEquiv_infty, RatFunc.liftOn'_div, RatFunc.denom_C, RatFunc.Luroth.generator_eq_zero, RatFunc.eval_zero, RatFunc.instCharP, RatFunc.natDegree_num_le_natDegree_minpolyX, RatFunc.C_injective, LaurentSeries.valuation_coe_ratFunc, RatFunc.liftRingHom_X, LaurentSeries.valuation_compare, RatFunc.coePolynomial_eq_algebraMap, RatFunc.ofFractionRing_inv, RatFunc.algebraMap_apply, RatFunc.Luroth.adjoin_generator_le, RatFunc.liftAlgHom_apply, RatFunc.Luroth.transcendental_generator, LaurentSeries.tendsto_valuation, RatFunc.transcendental, RatFunc.mk_one, RatFunc.algebraMap_injective, LaurentSeries.coe_range_dense, RatFunc.finrank_ratFunc_ratFunc, RatFunc.neg_def, RatFunc.ofFractionRing_eq, RatFunc.denom_algebraMap, RatFunc.liftRingHom_comp_algebraMap, RatFunc.isAlgebraic_adjoin_simple_X', RatFunc.valuation_isEquiv_inftyValuation_of_one_lt_valuation_X, RatFunc.intDegree_one, RatFunc.eq_C_iff, RatFunc.num_mul_eq_mul_denom_iff, LaurentSeries.comparePkg_eq_extension, RatFunc.liftAlgHom_apply_div', FunctionField.inftyValuation.C, RatFunc.liftRingHom_algebraMap, RatFunc.C_minpolyX, RatFunc.isScalarTower_liftAlgebra, RatFunc.valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one, RatFunc.sub_def, LaurentSeries.ratfuncAdicComplRingEquiv_apply, RatFunc.div_def, RatFunc.add_def, RatFunc.denom_add_dvd, RatFunc.valuation_uniformizingPolynomial_lt_one, RatFunc.num_div_denom, RatFunc.toFractionRingRingEquiv_symm_eq, RatFunc.algEquivOfTranscendental_algebraMap, RatFunc.aeval_X_left_eq_algebraMap, Polynomial.residueFieldMapCAlgEquiv_symm_X, RatFunc.associated_num_inv, RatFunc.toFractionRingRingEquiv_apply, LaurentSeries.mem_integers_of_powerSeries, RatFunc.algebraMap_monomial, RatFunc.isAlgebraic_adjoin_simple_X, RatFunc.instSubsingleton, RatFunc.denom_dvd, RatFunc.mul_inv_cancel, RatFunc.intDegree_neg, RatFunc.uniformizingPolynomial_isUniformizer, RatFunc.mul_def, RatFunc.natDegree_denom_le_natDegree_minpolyX, FunctionField.inftyValuation_apply, Polynomial.residueFieldMapCAlgEquiv_algebraMap, RatFunc.toFractionRingAlgEquiv_apply, RatFunc.laurentAux_ofFractionRing_mk, LaurentSeries.exists_ratFunc_eq_v, RatFunc.algEquivOfTranscendental_apply, RatFunc.map_apply_div_ne_zero, LaurentSeries.uniformContinuous_withVal_equiv, RatFunc.denom_zero, RatFunc.associated_denom_inv, Polynomial.residueFieldMapCAlgEquiv_symm_C, RatFunc.intDegree_zero, RatFunc.algebraMap_comp_C, RatFunc.ofFractionRing_algebraMap, RatFunc.eval_algebraMap, RatFunc.Luroth.generator_spec, RatFunc.num_denom_neg, Polynomial.valuation_X_eq_neg_one, RatFunc.ofFractionRing_mul, RatFunc.toFractionRing_eq

---

← Back to Index