Documentation Verification Report

Defs

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

Statistics

Metric	Count
Definitions `RatFunc`, `liftOn`, `liftOn'`, `mk`, `toFractionRing`	5
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	24

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`

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` `FractionRing` `Polynomial.commRing` `OreLocalization.instCommSemiring` `OreLocalization.oreSetComm` `CommRing.toCommMonoid` `OreLocalization.instAlgebra` `Algebra.id` `Localization.isLocalization` `NonAssocSemiring.toMulZeroOneClass` `Semiring.toNonAssocSemiring`	—	`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	186 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.num_div_dvd`, `RatFunc.liftMonoidWithZeroHom_apply_ofFractionRing_mk`, `RatFunc.laurent_X`, `RatFunc.num_one`, `RatFunc.smul_def`, `LaurentSeries.LaurentSeriesRingEquiv_def`, `RatFunc.transcendental_X`, `RatFunc.denom_one`, `RatFunc.denom_mul_dvd`, `FunctionField.inftyValuation.X_inv`, `RatFunc.map_apply_ofFractionRing_mk`, `RatFunc.laurent_algebraMap`, `RatFunc.mk_smul`, `FunctionField.InftyValuation.map_zero'`, `RatFunc.laurent_div`, `RatFunc.eval_one`, `RatFunc.liftAlgHom_injective`, `FunctionField.instIsNontrivialRatFuncWithZeroMultiplicativeIntInftyValuation`, `RatFunc.liftMonoidWithZeroHom_apply_div'`, `RatFunc.map_injective`, `RatFunc.coe_X`, `FunctionField.inftyValuation.polynomial`, `RatFunc.coe_mapRingHom_eq_coe_map`, `RatFunc.coe_coe`, `Polynomial.valuation_of_mk`, `LaurentSeries.inducing_coe`, `LaurentSeries.continuous_coe`, `LaurentSeries.algebraMap_C_mem_adicCompletionIntegers`, `RatFunc.map_apply`, `RatFunc.mk_eq_mk'`, `RatFunc.instNontrivial`, `RatFunc.ofFractionRing_div`, `RatFunc.toFractionRing_smul`, `RatFunc.num_denom_add`, `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.ofFractionRing_zero`, `RatFunc.ofFractionRing_add`, `RatFunc.liftMonoidWithZeroHom_apply_div`, `RatFunc.num_dvd`, `RatFunc.laurentAux_div`, `RatFunc.mk_eq_div`, `RatFunc.num_zero`, `RatFunc.intDegree_mul`, `RatFunc.liftOn_div`, `RatFunc.num_inv_dvd`, `RatFunc.ofFractionRing_comp_algebraMap`, `RatFunc.algebraMap_X`, `RatFunc.intDegree_C`, `FunctionField.InftyValuation.map_one'`, `RatFunc.num_denom_mul`, `RatFunc.intDegree_add_le`, `RatFunc.smul_eq_C_smul`, `RatFunc.valuation_eq_LaurentSeries_valuation`, `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.eval_C`, `RatFunc.inv_def`, `RatFunc.liftRingHom_apply_div`, `RatFunc.faithfulSMul`, `RatFunc.algebraMap_C`, `RatFunc.instIsScalarTowerPolynomial`, `RatFunc.num_eq_zero_iff`, `RatFunc.ofFractionRing_smul`, `RatFunc.intDegree_add`, `RatFunc.liftAlgHom_apply_div`, `RatFunc.liftRingHom_C`, `RatFunc.ofFractionRing_injective`, `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.denom_div_dvd`, `RatFunc.laurent_C`, `RatFunc.eval_add`, `FunctionField.inftyValuation.X_zpow`, `RatFunc.rank_ratFunc_ratFunc`, `LaurentSeries.powerSeriesRingEquiv_coe_apply`, `RatFunc.instIsScalarTowerOfPolynomial`, `FunctionField.inftyValuation.X`, `RatFunc.denom_inv_dvd`, `FunctionField.inftyValuedFqt.def`, `RatFunc.liftRingHom_apply_ofFractionRing_mk`, `RatFunc.num_mul_dvd`, `Polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebius`, `RatFunc.instExpChar`, `RatFunc.liftOn'_div`, `RatFunc.denom_C`, `RatFunc.eval_zero`, `RatFunc.instCharP`, `RatFunc.C_injective`, `LaurentSeries.valuation_coe_ratFunc`, `RatFunc.liftRingHom_X`, `LaurentSeries.valuation_compare`, `RatFunc.ofFractionRing_inv`, `RatFunc.algebraMap_apply`, `RatFunc.liftAlgHom_apply`, `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.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.isScalarTower_liftAlgebra`, `RatFunc.sub_def`, `LaurentSeries.ratfuncAdicComplRingEquiv_apply`, `RatFunc.div_def`, `RatFunc.add_def`, `RatFunc.denom_add_dvd`, `RatFunc.num_div_denom`, `RatFunc.toFractionRingRingEquiv_symm_eq`, `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.instSubsingleton`, `RatFunc.denom_dvd`, `RatFunc.mul_inv_cancel`, `RatFunc.intDegree_neg`, `RatFunc.mul_def`, `FunctionField.inftyValuation_apply`, `Polynomial.residueFieldMapCAlgEquiv_algebraMap`, `RatFunc.toFractionRingAlgEquiv_apply`, `RatFunc.laurentAux_ofFractionRing_mk`, `LaurentSeries.exists_ratFunc_eq_v`, `RatFunc.map_apply_div_ne_zero`, `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.num_denom_neg`, `Polynomial.valuation_X_eq_neg_one`, `RatFunc.ofFractionRing_mul`, `RatFunc.toFractionRing_eq`

---

← Back to Index