Basic

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

Statistics

Metric	Count
Definitions add, coePolynomial, denom, div, instAdd, instAddCommGroup, instAlgebraOfPolynomial, instCoePolynomial, instCommMonoid, instCommRing, instDiv, instField, instInhabited, instInv, instMul, instNeg, instOne, instSMulOfFractionRingPolynomial, instSub, instZero, inv, liftAlgHom, liftAlgebra, liftMonoidWithZeroHom, liftRingHom, map, mapAlgHom, mapRingHom, mul, neg, num, numDenom, one, smul, sub, tacticFrac_tac, tacticSmul_tac, toFractionRingAlgEquiv, toFractionRingRingEquiv, zero	40
Theorems add_def, algebraMap_apply, algebraMap_injective, algebraMap_ne_zero, associated_denom_inv, associated_num_inv, coe_mapAlgHom_eq_coe_map, coe_mapRingHom_eq_coe_map, denom_add_dvd, denom_algebraMap, denom_div, denom_div_dvd, denom_dvd, denom_inv_dvd, denom_mul_dvd, denom_ne_zero, denom_one, denom_zero, div_def, div_smul, faithfulSMul, finrank_ratFunc_ratFunc, induction_on, instCharP, instCharZero, instExpChar, instIsFractionRingPolynomial, instIsScalarTowerOfIsDomainOfPolynomial, instIsScalarTowerOfPolynomial, instIsScalarTowerOfPolynomial_1, instIsScalarTowerPolynomial, instNontrivial, instSubsingleton, inv_def, isCoprime_num_denom, isScalarTower_liftAlgebra, liftAlgHom_apply, liftAlgHom_apply_div, liftAlgHom_apply_div', liftAlgHom_apply_ofFractionRing_mk, liftAlgHom_injective, liftMonoidWithZeroHom_apply, liftMonoidWithZeroHom_apply_div, liftMonoidWithZeroHom_apply_div', liftMonoidWithZeroHom_apply_ofFractionRing_mk, liftMonoidWithZeroHom_injective, liftOn'_div, liftOn_div, liftRingHom_algebraMap, liftRingHom_apply, liftRingHom_apply_div, liftRingHom_apply_div', liftRingHom_apply_ofFractionRing_mk, liftRingHom_comp_algebraMap, liftRingHom_injective, liftRingHom_ofFractionRing_algebraMap, map_apply, map_apply_div, map_apply_div_ne_zero, map_apply_ofFractionRing_mk, map_denom_ne_zero, map_injective, mk_eq_div, mk_eq_mk', mk_one, mk_smul, monic_denom, mul_def, mul_inv_cancel, neg_def, numDenom_div, num_algebraMap, num_denom_add, num_denom_mul, num_denom_neg, num_div, num_div_denom, num_div_dvd, num_div_dvd', num_dvd, num_eq_zero_iff, num_inv_dvd, num_mul_denom_add_denom_mul_num_ne_zero, num_mul_dvd, num_mul_eq_mul_denom_iff, num_ne_zero, num_one, num_zero, ofFractionRing_add, ofFractionRing_algebraMap, ofFractionRing_comp_algebraMap, ofFractionRing_div, ofFractionRing_eq, ofFractionRing_inv, ofFractionRing_mk', ofFractionRing_mul, ofFractionRing_neg, ofFractionRing_one, ofFractionRing_smul, ofFractionRing_sub, ofFractionRing_zero, one_def, rank_ratFunc_ratFunc, smul_def, smul_eq_C_smul, sub_def, toFractionRingAlgEquiv_apply, toFractionRingRingEquiv_apply, toFractionRingRingEquiv_symm_eq, toFractionRing_eq, toFractionRing_smul, zero_def	112
Total	152

RatFunc

Definitions

Name	Category	Theorems
add 📖	CompOp	1 math math: add_def
coePolynomial 📖	CompOp	1 math math: coe_coe
denom 📖	CompOp	28 math math: liftMonoidWithZeroHom_apply, denom_one, denom_mul_dvd, isCoprime_num_denom, map_apply, num_denom_add, num_inv_dvd, num_denom_mul, liftRingHom_apply, intDegree_add, denom_X, denom_div, denom_div_dvd, denom_inv_dvd, denom_C, natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree, liftAlgHom_apply, denom_algebraMap, eq_C_iff, num_mul_eq_mul_denom_iff, denom_add_dvd, num_div_denom, associated_num_inv, denom_dvd, denom_zero, associated_denom_inv, num_denom_neg, monic_denom
div 📖	CompOp	1 math math: div_def
instAdd 📖	CompOp	10 math math: laurent_X, num_denom_add, FunctionField.InftyValuation.map_add_le_max', ofFractionRing_add, intDegree_add_le, intDegree_add, eval_add, denom_add_dvd, toFractionRingRingEquiv_symm_eq, toFractionRingRingEquiv_apply
instAddCommGroup 📖	CompOp	—
instAlgebraOfPolynomial 📖	CompOp	83 math math: laurent_injective, ofFractionRing_mk', num_div, coe_mapAlgHom_eq_coe_map, num_div_dvd, laurent_X, LaurentSeries.LaurentSeriesRingEquiv_def, transcendental_X, laurent_algebraMap, laurent_div, liftAlgHom_injective, liftMonoidWithZeroHom_apply_div', FunctionField.inftyValuation.polynomial, Polynomial.valuation_of_mk, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, map_apply, mk_eq_mk', instIsFractionRingPolynomial, laurent_at_zero, numDenom_div, laurent_laurent, num_algebraMap, liftMonoidWithZeroHom_apply_div, num_dvd, laurentAux_div, mk_eq_div, liftOn_div, ofFractionRing_comp_algebraMap, algebraMap_X, valuation_eq_LaurentSeries_valuation, map_apply_div, liftRingHom_apply_div', LaurentSeries.coe_X_compare, laurentAux_algebraMap, algebraMap_eq_C, algebraMap_apply_div, div_smul, liftRingHom_apply_div, algebraMap_C, liftAlgHom_apply_div, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, denom_div, intDegree_polynomial, v_def, LaurentSeries.powerSeries_ext_subring, liftAlgHom_apply_ofFractionRing_mk, denom_div_dvd, laurent_C, rank_ratFunc_ratFunc, LaurentSeries.powerSeriesRingEquiv_coe_apply, Polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebius, liftOn'_div, LaurentSeries.valuation_compare, algebraMap_apply, liftAlgHom_apply, LaurentSeries.tendsto_valuation, transcendental, mk_one, algebraMap_injective, finrank_ratFunc_ratFunc, ofFractionRing_eq, denom_algebraMap, liftRingHom_comp_algebraMap, num_mul_eq_mul_denom_iff, liftAlgHom_apply_div', liftRingHom_algebraMap, LaurentSeries.ratfuncAdicComplRingEquiv_apply, num_div_denom, toFractionRingRingEquiv_symm_eq, aeval_X_left_eq_algebraMap, Polynomial.residueFieldMapCAlgEquiv_symm_X, LaurentSeries.mem_integers_of_powerSeries, algebraMap_monomial, denom_dvd, Polynomial.residueFieldMapCAlgEquiv_algebraMap, toFractionRingAlgEquiv_apply, map_apply_div_ne_zero, Polynomial.residueFieldMapCAlgEquiv_symm_C, algebraMap_comp_C, ofFractionRing_algebraMap, eval_algebraMap, Polynomial.valuation_X_eq_neg_one, toFractionRing_eq
instCoePolynomial 📖	CompOp	—
instCommMonoid 📖	CompOp	—
instCommRing 📖	CompOp	35 math math: liftMonoidWithZeroHom_apply, coe_mapAlgHom_eq_coe_map, liftMonoidWithZeroHom_apply_ofFractionRing_mk, LaurentSeries.LaurentSeriesRingEquiv_def, map_apply_ofFractionRing_mk, liftMonoidWithZeroHom_apply_div', map_injective, coe_mapRingHom_eq_coe_map, map_apply, liftRingHom_injective, liftMonoidWithZeroHom_apply_div, laurentAux_div, liftRingHom_apply, map_apply_div, liftRingHom_apply_div', LaurentSeries.coe_X_compare, liftRingHom_ofFractionRing_algebraMap, laurentAux_algebraMap, liftRingHom_apply_div, LaurentSeries.exists_powerSeries_of_memIntegers, liftRingHom_C, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, liftMonoidWithZeroHom_injective, rank_ratFunc_ratFunc, LaurentSeries.powerSeriesRingEquiv_coe_apply, liftRingHom_apply_ofFractionRing_mk, Polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebius, liftRingHom_X, finrank_ratFunc_ratFunc, liftRingHom_comp_algebraMap, liftRingHom_algebraMap, LaurentSeries.ratfuncAdicComplRingEquiv_apply, LaurentSeries.mem_integers_of_powerSeries, laurentAux_ofFractionRing_mk, map_apply_div_ne_zero
instDiv 📖	CompOp	26 math math: num_div, num_div_dvd, FunctionField.inftyValuation.X_inv, laurent_div, map_apply, ofFractionRing_div, numDenom_div, liftMonoidWithZeroHom_apply_div, num_dvd, laurentAux_div, mk_eq_div, Polynomial.valuation_inv_monomial_eq_valuation_X_zpow, liftOn_div, map_apply_div, algebraMap_apply_div, div_smul, liftRingHom_apply_div, liftAlgHom_apply_div, denom_div, denom_div_dvd, liftOn'_div, algebraMap_apply, num_mul_eq_mul_denom_iff, num_div_denom, denom_dvd, map_apply_div_ne_zero
instField 📖	CompOp	115 math math: laurent_injective, ofFractionRing_mk', num_div, coe_mapAlgHom_eq_coe_map, num_div_dvd, laurent_X, LaurentSeries.LaurentSeriesRingEquiv_def, transcendental_X, FunctionField.inftyValuation.X_inv, laurent_algebraMap, laurent_div, liftAlgHom_injective, FunctionField.instIsNontrivialRatFuncWithZeroMultiplicativeIntInftyValuation, liftMonoidWithZeroHom_apply_div', coe_X, FunctionField.inftyValuation.polynomial, coe_coe, Polynomial.valuation_of_mk, LaurentSeries.inducing_coe, LaurentSeries.continuous_coe, LaurentSeries.algebraMap_C_mem_adicCompletionIntegers, map_apply, mk_eq_mk', FunctionField.valuedFqtInfty.def, instIsFractionRingPolynomial, laurent_at_zero, numDenom_div, instIsScalarTowerOfPolynomial_1, num_C, smul_eq_C_mul, laurent_laurent, LaurentSeries.exists_ratFunc_val_lt, num_algebraMap, liftMonoidWithZeroHom_apply_div, num_dvd, laurentAux_div, mk_eq_div, liftOn_div, ofFractionRing_comp_algebraMap, algebraMap_X, intDegree_C, valuation_eq_LaurentSeries_valuation, map_apply_div, liftRingHom_apply_div', LaurentSeries.coe_X_compare, laurentAux_algebraMap, algebraMap_eq_C, algebraMap_apply_div, div_smul, eval_C, liftRingHom_apply_div, algebraMap_C, liftAlgHom_apply_div, liftRingHom_C, LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring, denom_div, LaurentSeries.valuation_LaurentSeries_equal_extension, intDegree_polynomial, v_def, instCharZero, LaurentSeries.LaurentSeries_coe, LaurentSeries.powerSeries_ext_subring, liftAlgHom_apply_ofFractionRing_mk, denom_div_dvd, laurent_C, FunctionField.inftyValuation.X_zpow, rank_ratFunc_ratFunc, LaurentSeries.powerSeriesRingEquiv_coe_apply, instIsScalarTowerOfPolynomial, FunctionField.inftyValuation.X, FunctionField.inftyValuedFqt.def, Polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebius, instExpChar, liftOn'_div, denom_C, instCharP, C_injective, LaurentSeries.valuation_coe_ratFunc, LaurentSeries.valuation_compare, algebraMap_apply, liftAlgHom_apply, LaurentSeries.tendsto_valuation, transcendental, mk_one, algebraMap_injective, LaurentSeries.coe_range_dense, finrank_ratFunc_ratFunc, ofFractionRing_eq, denom_algebraMap, eq_C_iff, num_mul_eq_mul_denom_iff, LaurentSeries.comparePkg_eq_extension, liftAlgHom_apply_div', FunctionField.inftyValuation.C, liftRingHom_algebraMap, isScalarTower_liftAlgebra, LaurentSeries.ratfuncAdicComplRingEquiv_apply, num_div_denom, toFractionRingRingEquiv_symm_eq, aeval_X_left_eq_algebraMap, Polynomial.residueFieldMapCAlgEquiv_symm_X, LaurentSeries.mem_integers_of_powerSeries, algebraMap_monomial, denom_dvd, FunctionField.inftyValuation_apply, Polynomial.residueFieldMapCAlgEquiv_algebraMap, toFractionRingAlgEquiv_apply, LaurentSeries.exists_ratFunc_eq_v, map_apply_div_ne_zero, Polynomial.residueFieldMapCAlgEquiv_symm_C, algebraMap_comp_C, ofFractionRing_algebraMap, eval_algebraMap, Polynomial.valuation_X_eq_neg_one, toFractionRing_eq
instInhabited 📖	CompOp	—
instInv 📖	CompOp	7 math math: intDegree_inv, num_inv_dvd, denom_inv_dvd, ofFractionRing_inv, associated_num_inv, mul_inv_cancel, associated_denom_inv
instMul 📖	CompOp	12 math math: eval_mul, denom_mul_dvd, smul_eq_C_mul, intDegree_mul, num_denom_mul, FunctionField.InftyValuation.map_mul', num_mul_dvd, toFractionRingRingEquiv_symm_eq, toFractionRingRingEquiv_apply, algebraMap_monomial, mul_inv_cancel, ofFractionRing_mul
instNeg 📖	CompOp	3 math math: ofFractionRing_neg, intDegree_neg, num_denom_neg
instOne 📖	CompOp	9 math math: num_one, denom_one, FunctionField.inftyValuation.X_inv, eval_one, ofFractionRing_one, Polynomial.valuation_inv_monomial_eq_valuation_X_zpow, FunctionField.InftyValuation.map_one', intDegree_one, mul_inv_cancel
instSMulOfFractionRingPolynomial 📖	CompOp	11 math math: mk_smul, toFractionRing_smul, smul_eq_C_mul, smul_eq_C_smul, instIsScalarTowerOfIsDomainOfPolynomial, div_smul, faithfulSMul, instIsScalarTowerPolynomial, ofFractionRing_smul, instIsScalarTowerOfPolynomial, isScalarTower_liftAlgebra
instSub 📖	CompOp	1 math math: ofFractionRing_sub
instZero 📖	CompOp	7 math math: FunctionField.InftyValuation.map_zero', ofFractionRing_zero, num_zero, num_eq_zero_iff, eval_zero, denom_zero, intDegree_zero
inv 📖	CompOp	1 math math: inv_def
liftAlgHom 📖	CompOp	5 math math: liftAlgHom_injective, liftAlgHom_apply_div, liftAlgHom_apply_ofFractionRing_mk, liftAlgHom_apply, liftAlgHom_apply_div'
liftAlgebra 📖	CompOp	15 math math: coe_X, coe_coe, LaurentSeries.inducing_coe, LaurentSeries.continuous_coe, instIsScalarTowerOfPolynomial_1, LaurentSeries.exists_ratFunc_val_lt, valuation_eq_LaurentSeries_valuation, algebraMap_apply_div, LaurentSeries.LaurentSeries_coe, rank_ratFunc_ratFunc, instIsScalarTowerOfPolynomial, LaurentSeries.valuation_coe_ratFunc, LaurentSeries.coe_range_dense, finrank_ratFunc_ratFunc, isScalarTower_liftAlgebra
liftMonoidWithZeroHom 📖	CompOp	5 math math: liftMonoidWithZeroHom_apply, liftMonoidWithZeroHom_apply_ofFractionRing_mk, liftMonoidWithZeroHom_apply_div', liftMonoidWithZeroHom_apply_div, liftMonoidWithZeroHom_injective
liftRingHom 📖	CompOp	10 math math: liftRingHom_injective, liftRingHom_apply, liftRingHom_apply_div', liftRingHom_ofFractionRing_algebraMap, liftRingHom_apply_div, liftRingHom_C, liftRingHom_apply_ofFractionRing_mk, liftRingHom_X, liftRingHom_comp_algebraMap, liftRingHom_algebraMap
map 📖	CompOp	7 math math: coe_mapAlgHom_eq_coe_map, map_apply_ofFractionRing_mk, map_injective, coe_mapRingHom_eq_coe_map, map_apply, map_apply_div, map_apply_div_ne_zero
mapAlgHom 📖	CompOp	1 math math: coe_mapAlgHom_eq_coe_map
mapRingHom 📖	CompOp	1 math math: coe_mapRingHom_eq_coe_map
mul 📖	CompOp	1 math math: mul_def
neg 📖	CompOp	1 math math: neg_def
num 📖	CompOp	27 math math: liftMonoidWithZeroHom_apply, num_div, num_div_dvd, num_one, isCoprime_num_denom, map_apply, num_denom_add, num_C, num_algebraMap, num_dvd, num_zero, num_inv_dvd, num_denom_mul, liftRingHom_apply, num_X, num_eq_zero_iff, intDegree_add, denom_inv_dvd, num_mul_dvd, natDegree_num_mul_right_sub_natDegree_denom_mul_left_eq_intDegree, liftAlgHom_apply, eq_C_iff, num_mul_eq_mul_denom_iff, num_div_denom, associated_num_inv, associated_denom_inv, num_denom_neg
numDenom 📖	CompOp	1 math math: numDenom_div
one 📖	CompOp	1 math math: one_def
smul 📖	CompOp	1 math math: smul_def
sub 📖	CompOp	1 math math: sub_def
tacticFrac_tac 📖	CompOp	—
tacticSmul_tac 📖	CompOp	—
toFractionRingAlgEquiv 📖	CompOp	1 math math: toFractionRingAlgEquiv_apply
toFractionRingRingEquiv 📖	CompOp	2 math math: toFractionRingRingEquiv_symm_eq, toFractionRingRingEquiv_apply
zero 📖	CompOp	1 math math: zero_def

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_def 📖	mathematical	—	add RatFunc ofFractionRing FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing OreLocalization.instAdd CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Semiring.toModule	—	—
algebraMap_apply 📖	mathematical	—	DFunLike.coe RingHom RatFunc Semiring.toNonAssocSemiring CommSemiring.toSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial instDiv Polynomial CommRing.toCommSemiring Polynomial.commSemiring Algebra.id Polynomial.semiring Polynomial.instOne	—	mk_eq_div
algebraMap_injective 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring RatFunc DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id	—	ofFractionRing_comp_algebraMap ofFractionRing_injective IsFractionRing.injective Localization.isLocalization
algebraMap_ne_zero 📖	—	—	—	—	Module.IsTorsionFree.to_faithfulSMul Polynomial.instIsCancelMulZeroOfIsCancelAdd AddCancelMonoid.toIsCancelAdd IsDomain.toIsCancelMulZero instNontrivial IsDomain.toNontrivial FaithfulSMul.to_isTorsionFree IsFractionRing.instFaithfulSMul instIsFractionRingPolynomial Polynomial.nontrivial instIsDomain
associated_denom_inv 📖	mathematical	—	Associated Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring denom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain instInv instIsDomain num	—	Associated.symm instIsDomain inv_inv associated_num_inv inv_ne_zero
associated_num_inv 📖	mathematical	—	Associated Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MonoidWithZero.toMonoid Semiring.toMonoidWithZero Polynomial.semiring num RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain instInv instIsDomain denom	—	associated_of_dvd_dvd Polynomial.instIsLeftCancelMulZeroOfIsCancelAdd AddCancelMonoid.toIsCancelAdd IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero instIsDomain num_inv_dvd inv_inv denom_inv_dvd inv_ne_zero
coe_mapAlgHom_eq_coe_map 📖	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 AlgHom AlgHom.funLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass	DFunLike.coe RatFunc DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField instAlgebraOfPolynomial mapAlgHom MonoidHom MulOneClass.toMulOne instCommRing MonoidHom.instFunLike map	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
coe_mapRingHom_eq_coe_map 📖	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 MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass	DFunLike.coe RingHom RatFunc instCommRing RingHom.instFunLike mapRingHom MonoidHom MulOneClass.toMulOne MonoidHom.instFunLike map	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
denom_add_dvd 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain denom RatFunc instAdd Polynomial.instMul	—	instIsDomain denom_dvd mul_ne_zero Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors denom_ne_zero map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass div_add_div algebraMap_ne_zero num_div_denom
denom_algebraMap 📖	mathematical	—	denom DFunLike.coe RingHom Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toNonAssocSemiring CommSemiring.toSemiring Polynomial.commSemiring Semifield.toCommSemiring instField instIsDomain RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id Polynomial.instOne	—	instIsDomain map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass div_one gcd_one_right EuclideanDomain.div_self NeZero.one Polynomial.nontrivial EuclideanDomain.toNontrivial Polynomial.Monic.leadingCoeff inv_one mul_one denom_div one_ne_zero
denom_div 📖	mathematical	—	denom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain instDiv instIsDomain Field.toSemifield DFunLike.coe RingHom Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Polynomial.commSemiring Semifield.toCommSemiring instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id Polynomial.instMul Polynomial.semiring Polynomial.C InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Polynomial.leadingCoeff Polynomial.instDiv GCDMonoid.gcd CommSemiring.toCommMonoidWithZero NormalizedGCDMonoid.toGCDMonoid Polynomial.normalizedGcdMonoid CommGroupWithZero.instNormalizedGCDMonoid	—	instIsDomain denom.eq_1 numDenom_div
denom_div_dvd 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain denom RatFunc instDiv instIsDomain DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Polynomial.commSemiring Semifield.toCommSemiring instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id	—	instIsDomain map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass div_zero denom_zero denom_div Polynomial.C_mul_dvd right_div_gcd_ne_zero EuclideanDomain.div_dvd_of_dvd GCDMonoid.gcd_dvd_right
denom_dvd 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain denom RatFunc instDiv instIsDomain DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Polynomial.commSemiring Semifield.toCommSemiring instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id	—	instIsDomain mul_ne_zero_iff Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass div_mul_div_comm div_self algebraMap_ne_zero mul_one num_div_denom denom_div_dvd
denom_inv_dvd 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain denom RatFunc instInv instIsDomain num	—	instIsDomain denom_dvd num_ne_zero num_div_denom inv_div
denom_mul_dvd 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain denom RatFunc instMul Polynomial.instMul	—	instIsDomain denom_dvd mul_ne_zero Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors denom_ne_zero map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass div_mul_div_comm num_div_denom
denom_ne_zero 📖	—	—	—	—	Polynomial.Monic.ne_zero EuclideanDomain.toNontrivial monic_denom
denom_one 📖	mathematical	—	denom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain instOne Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instOne	—	instIsDomain map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass div_self NeZero.one instNontrivial EuclideanDomain.toNontrivial gcd_same MonoidWithZeroHom.monoidWithZeroHomClass EuclideanDomain.div_self Polynomial.nontrivial Polynomial.Monic.leadingCoeff inv_one mul_one denom_div one_ne_zero
denom_zero 📖	mathematical	—	denom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain instZero Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instOne	—	instIsDomain map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass div_one gcd_one_right EuclideanDomain.div_self NeZero.one Polynomial.nontrivial EuclideanDomain.toNontrivial Polynomial.Monic.leadingCoeff inv_one mul_one denom_div one_ne_zero
div_def 📖	mathematical	—	div RatFunc 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	—	—
div_smul 📖	mathematical	—	RatFunc instDiv DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Semiring.toNonAssocSemiring Polynomial.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Polynomial.ring CommRing.toRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul instSMulOfFractionRingPolynomial OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid CommRing.toCommMonoid Polynomial.commRing nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm Monoid.toMulAction	—	mk_eq_div mk_smul
faithfulSMul 📖	mathematical	—	FaithfulSMul Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain instSMulOfFractionRingPolynomial OreLocalization.instSMulOfIsScalarTower CommSemiring.toSemiring CommRing.toCommSemiring CommMonoid.toMonoid CommRing.toCommMonoid Polynomial.commRing nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm Monoid.toMulAction Algebra.toSMul Polynomial.commSemiring Semifield.toCommSemiring Polynomial.semiring Polynomial.algebra IsScalarTower.right	—	instIsDomain faithfulSMul_iff_algebraMap_injective IsFractionRing.injective instIsFractionRingPolynomial Polynomial.map_injective FaithfulSMul.algebraMap_injective
finrank_ratFunc_ratFunc 📖	mathematical	—	Module.finrank RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField instIsDomain NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing Algebra.toModule Semifield.toCommSemiring liftAlgebra instAlgebraOfPolynomial Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commSemiring Polynomial.algebra faithfulSMul Module.Free.instFaithfulSMulOfNontrivial NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Module.Free.of_divisionRing Field.toDivisionRing Ring.toAddCommGroup DivisionRing.toRing EuclideanDomain.toNontrivial	—	instIsDomain faithfulSMul Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing EuclideanDomain.toNontrivial rank_ratFunc_ratFunc Module.finrank_eq_of_rank_eq Module.finrank_eq_rank IsNoetherianRing.strongRankCondition instNontrivial PrincipalIdealRing.isNoetherianRing EuclideanDomain.to_principal_ideal_domain Module.rank_lt_aleph0_iff Module.finrank_of_not_finite
induction_on 📖	—	RatFunc instDiv DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Semiring.toNonAssocSemiring Polynomial.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id	—	—	induction_on' mk_eq_div
instCharP 📖	mathematical	—	CharP RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing instField instIsDomain Field.toSemifield	—	charP_of_injective_algebraMap' instIsDomain Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing instNontrivial EuclideanDomain.toNontrivial
instCharZero 📖	mathematical	—	CharZero RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing instField instIsDomain Field.toSemifield	—	Algebra.charZero_of_charZero instIsDomain Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing instNontrivial EuclideanDomain.toNontrivial
instExpChar 📖	mathematical	—	ExpChar RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing instField instIsDomain Field.toSemifield	—	ExpChar.of_injective_algebraMap' instIsDomain Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing instNontrivial EuclideanDomain.toNontrivial
instIsFractionRingPolynomial 📖	mathematical	—	IsFractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commSemiring RatFunc Semifield.toCommSemiring Field.toSemifield instField instAlgebraOfPolynomial Algebra.id	—	ofFractionRing_algebraMap RingHom.isUnit_map IsLocalization.map_units Localization.isLocalization IsLocalization.surj IsLocalization.exists_of_eq RingEquiv.injective
instIsScalarTowerOfIsDomainOfPolynomial 📖	mathematical	—	IsScalarTower 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 IsScalarTower.right	—	IsScalarTower.to₁₂₄ IsScalarTower.right instIsScalarTowerPolynomial
instIsScalarTowerOfPolynomial 📖	mathematical	—	IsScalarTower 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 IsScalarTower.right Semifield.toCommSemiring Field.toSemifield instField DivisionSemiring.toSemiring Semifield.toDivisionSemiring liftAlgebra	—	IsScalarTower.to₁₃₄ IsScalarTower.right instIsScalarTowerPolynomial isScalarTower_liftAlgebra
instIsScalarTowerOfPolynomial_1 📖	mathematical	—	IsScalarTower RatFunc Algebra.toSMul Semifield.toCommSemiring Field.toSemifield instField DivisionSemiring.toSemiring Semifield.toDivisionSemiring liftAlgebra	—	induction_on FaithfulSMul.to_isTorsionFree Polynomial.nontrivial IsDomain.toNontrivial IsDomain.toIsCancelMulZero instIsDomain Polynomial.instIsCancelMulZeroOfIsCancelAdd AddCancelMonoid.toIsCancelAdd IsScalarTower.right isScalarTower_liftAlgebra Algebra.smul_def Mathlib.Tactic.FieldSimp.eq_eq_cancel_eq IsCancelMulZero.toIsLeftCancelMulZero instIsCancelMulZero Mathlib.Tactic.FieldSimp.eq_mul_of_eq_eq_eq_mul Mathlib.Tactic.FieldSimp.NF.mul_eq_eval Mathlib.Tactic.FieldSimp.NF.atom_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval Mathlib.Tactic.FieldSimp.NF.div_eq_eval₁ Mathlib.Tactic.FieldSimp.NF.one_div_eq_eval Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₃ Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₂ one_mul Mathlib.Tactic.FieldSimp.NF.eval_cons_eq_eval_of_eq_of_eq Mathlib.Tactic.FieldSimp.NF.eval_cons_of_pow_eq_zero Module.IsTorsionFree.to_faithfulSMul instNontrivial IsFractionRing.instFaithfulSMul instIsFractionRingPolynomial Mathlib.Tactic.FieldSimp.eq_div_of_eq_one_of_subst Mathlib.Tactic.FieldSimp.NF.cons_eq_div_of_eq_div div_one Mathlib.Tactic.FieldSimp.NF.eval_cons Mathlib.Tactic.FieldSimp.zpow'_one Mathlib.Tactic.FieldSimp.NF.eval_mul_eval_cons one_ne_zero NeZero.one GroupWithZero.toNontrivial algebraMap_smul smul_assoc
instIsScalarTowerPolynomial 📖	mathematical	—	IsScalarTower Polynomial CommSemiring.toSemiring CommRing.toCommSemiring RatFunc SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Polynomial.ring CommRing.toRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul instSMulOfFractionRingPolynomial OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid CommRing.toCommMonoid Polynomial.commRing nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm Monoid.toMulAction Algebra.toSMul Polynomial.commSemiring Algebra.id IsScalarTower.right	—	IsScalarTower.right induction_on' mk_smul smul_assoc
instNontrivial 📖	mathematical	—	Nontrivial RatFunc	—	Function.Injective.nontrivial FractionRing.instNontrivial Polynomial.nontrivial ofFractionRing_injective
instSubsingleton 📖	mathematical	—	RatFunc	—	Function.Injective.subsingleton toFractionRing_injective LocalizedModule.instSubsingleton Unique.instSubsingleton
inv_def 📖	mathematical	—	inv RatFunc ofFractionRing FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing OreLocalization.inv' Semiring.toMonoidWithZero OreLocalization.oreSetComm CommRing.toCommMonoid nonZeroDivisors	—	—
isCoprime_num_denom 📖	mathematical	—	IsCoprime Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.commSemiring Semifield.toCommSemiring num denom	—	induction_on instIsDomain num_div denom_div isCoprime_mul_unit_left IsUnit.map MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass IsUnit.inv Ne.isUnit Polynomial.leadingCoeff_ne_zero right_div_gcd_ne_zero isCoprime_div_gcd_div_gcd
isScalarTower_liftAlgebra 📖	mathematical	—	IsScalarTower Polynomial CommSemiring.toSemiring CommRing.toCommSemiring RatFunc instSMulOfFractionRingPolynomial OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid CommRing.toCommMonoid Polynomial.commRing nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm Monoid.toMulAction Algebra.toSMul Polynomial.commSemiring Algebra.id IsScalarTower.right Semifield.toCommSemiring Field.toSemifield instField DivisionSemiring.toSemiring Semifield.toDivisionSemiring liftAlgebra	—	IsScalarTower.of_algebraMap_eq instIsFractionRingPolynomial FaithfulSMul.algebraMap_injective IsFractionRing.lift_algebraMap
liftAlgHom_apply 📖	mathematical	Submonoid Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero Polynomial.semiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Submonoid.comap NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring AlgHom AlgHom.funLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass	DFunLike.coe RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain instField instIsDomain instAlgebraOfPolynomial liftAlgHom DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing num denom	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass liftMonoidWithZeroHom_apply
liftAlgHom_apply_div 📖	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 AlgHom AlgHom.funLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass	DFunLike.coe RatFunc instField instAlgebraOfPolynomial liftAlgHom instDiv RingHom Polynomial.commSemiring RingHom.instFunLike algebraMap Algebra.id DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass liftMonoidWithZeroHom_apply_div
liftAlgHom_apply_div' 📖	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 AlgHom AlgHom.funLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing DFunLike.coe RatFunc instField instAlgebraOfPolynomial liftAlgHom RingHom Polynomial.commSemiring RingHom.instFunLike algebraMap Algebra.id	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass liftMonoidWithZeroHom_apply_div'
liftAlgHom_apply_ofFractionRing_mk 📖	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 AlgHom AlgHom.funLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass	DFunLike.coe RatFunc instField instAlgebraOfPolynomial liftAlgHom ofFractionRing CommRing.toCommMonoid Polynomial.commRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing SetLike.instMembership Submonoid.instSetLike	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass
liftAlgHom_injective 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe AlgHom Polynomial.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield AlgHom.funLike Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Submonoid.comap NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass nonZeroDivisors_le_comap_nonZeroDivisors_of_injective IsDomain.to_noZeroDivisors instIsDomain	RatFunc instField instAlgebraOfPolynomial liftAlgHom	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass AlgHom.algHomClass liftMonoidWithZeroHom_injective IsDomain.toNontrivial nonZeroDivisors_le_comap_nonZeroDivisors_of_injective GroupWithZero.noZeroDivisors MonoidWithZeroHom.monoidWithZeroHomClass
liftMonoidWithZeroHom_apply 📖	mathematical	Submonoid Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero Polynomial.semiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Submonoid.comap NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero MonoidWithZeroHom MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass	DFunLike.coe RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toSemiring CommRing.toCommSemiring instCommRing liftMonoidWithZeroHom DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid num denom	—	MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass instIsDomain num_div_denom liftMonoidWithZeroHom_apply_div
liftMonoidWithZeroHom_apply_div 📖	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 GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero MonoidWithZeroHom MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass	DFunLike.coe RatFunc instCommRing liftMonoidWithZeroHom instDiv RingHom Polynomial.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid	—	MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass eq_or_ne map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass div_zero mem_nonZeroDivisors_iff_ne_zero Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors Polynomial.nontrivial IsDomain.toNontrivial
liftMonoidWithZeroHom_apply_div' 📖	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 GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero MonoidWithZeroHom MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass	DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid DFunLike.coe RatFunc instCommRing liftMonoidWithZeroHom RingHom Polynomial.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id	—	MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass map_div₀ liftMonoidWithZeroHom_apply_div
liftMonoidWithZeroHom_apply_ofFractionRing_mk 📖	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 GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero MonoidWithZeroHom MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass	DFunLike.coe RatFunc instCommRing liftMonoidWithZeroHom ofFractionRing CommRing.toCommMonoid Polynomial.commRing DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid SetLike.instMembership Submonoid.instSetLike	—	MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass
liftMonoidWithZeroHom_injective 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe MonoidWithZeroHom NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring Polynomial.semiring MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero CommGroupWithZero.toGroupWithZero MonoidWithZeroHom.funLike Submonoid MulZeroOneClass.toMulOneClass Semiring.toMonoidWithZero Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Submonoid.comap MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass nonZeroDivisors_le_comap_nonZeroDivisors_of_injective GroupWithZero.noZeroDivisors	RatFunc instCommRing liftMonoidWithZeroHom	—	MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass Localization.induction_on Localization.mk_eq_mk_iff Localization.r_of_eq mul_eq_mul_of_div_eq_div map_ne_zero_of_mem_nonZeroDivisors Polynomial.nontrivial MonoidWithZeroHomClass.toZeroHomClass SetLike.coe_mem mul_comm map_mul MonoidHomClass.toMulHomClass
liftOn'_div 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instZero Polynomial.instOne Polynomial.instMul	liftOn' RatFunc instDiv DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id	—	liftOn'_def liftOn_condition_of_liftOn'_condition nonZeroDivisors.ne_zero Polynomial.nontrivial IsDomain.toNontrivial liftOn_div
liftOn_div 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instZero Polynomial.instOne nonZeroDivisors.ne_zero Semiring.toMonoidWithZero Polynomial.semiring Polynomial.nontrivial IsDomain.toNontrivial	liftOn RatFunc instDiv DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id	—	mk_eq_div nonZeroDivisors.ne_zero Polynomial.nontrivial IsDomain.toNontrivial
liftRingHom_algebraMap 📖	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 Polynomial.commSemiring instField algebraMap instAlgebraOfPolynomial Algebra.id	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_one MonoidHomClass.toOneHomClass div_one liftRingHom_apply_div'
liftRingHom_apply 📖	mathematical	Submonoid Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero Polynomial.semiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Submonoid.comap NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring RingHom RingHom.instFunLike MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass	DFunLike.coe RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain CommSemiring.toSemiring CommRing.toCommSemiring instCommRing liftRingHom DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing num denom	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass liftMonoidWithZeroHom_apply
liftRingHom_apply_div 📖	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 instDiv Polynomial.commSemiring instField algebraMap instAlgebraOfPolynomial Algebra.id DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass liftMonoidWithZeroHom_apply_div
liftRingHom_apply_div' 📖	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	DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing DFunLike.coe RatFunc instCommRing liftRingHom Polynomial.commSemiring instField algebraMap instAlgebraOfPolynomial Algebra.id	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass liftMonoidWithZeroHom_apply_div'
liftRingHom_apply_ofFractionRing_mk 📖	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 ofFractionRing CommRing.toCommMonoid Polynomial.commRing DivInvMonoid.toDiv DivisionRing.toDivInvMonoid Field.toDivisionRing SetLike.instMembership Submonoid.instSetLike	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
liftRingHom_comp_algebraMap 📖	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	RingHom.comp RatFunc Polynomial.commSemiring instCommRing liftRingHom algebraMap instAlgebraOfPolynomial Algebra.id	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass RingHom.ext liftRingHom_algebraMap
liftRingHom_injective 📖	mathematical	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RingHom.instFunLike Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Submonoid.comap NonAssocSemiring.toMulZeroOneClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass nonZeroDivisors_le_comap_nonZeroDivisors_of_injective IsDomain.to_noZeroDivisors instIsDomain	RatFunc instCommRing liftRingHom	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass liftMonoidWithZeroHom_injective nonZeroDivisors_le_comap_nonZeroDivisors_of_injective GroupWithZero.noZeroDivisors MonoidWithZeroHom.monoidWithZeroHomClass
liftRingHom_ofFractionRing_algebraMap 📖	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 ofFractionRing FractionRing Polynomial.commRing Polynomial.commSemiring OreLocalization.instSemiring OreLocalization.oreSetComm CommRing.toCommMonoid algebraMap OreLocalization.instAlgebra Algebra.id	—	MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Localization.mk_one_eq_algebraMap map_one MonoidHomClass.toOneHomClass div_one
map_apply 📖	mathematical	Submonoid Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero Polynomial.semiring Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder nonZeroDivisors Submonoid.comap CommSemiring.toSemiring CommRing.toCommSemiring NonAssocSemiring.toMulZeroOneClass Semiring.toNonAssocSemiring	DFunLike.coe MonoidHom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain MulOneClass.toMulOne instCommRing MonoidHom.instFunLike map instDiv RingHom Polynomial.commSemiring instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id num denom	—	instIsDomain num_div_denom map_apply_div_ne_zero denom_ne_zero
map_apply_div 📖	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 MonoidWithZeroHomClass.toMonoidHomClass	DFunLike.coe MonoidHom RatFunc MulOneClass.toMulOne instCommRing MonoidHom.instFunLike map instDiv RingHom Polynomial.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id	—	MonoidWithZeroHomClass.toMonoidHomClass eq_or_ne map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_one MonoidHomClass.toOneHomClass div_one div_zero map_apply_div_ne_zero one_ne_zero NeZero.one Polynomial.nontrivial IsDomain.toNontrivial
map_apply_div_ne_zero 📖	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	DFunLike.coe MonoidHom RatFunc MulOneClass.toMulOne instCommRing MonoidHom.instFunLike map instDiv RingHom Polynomial.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id	—	nonZeroDivisors.ne_zero Polynomial.nontrivial IsDomain.toNontrivial mem_nonZeroDivisors_iff_ne_zero Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors Subtype.prop
map_apply_ofFractionRing_mk 📖	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	DFunLike.coe MonoidHom RatFunc MulOneClass.toMulOne instCommRing MonoidHom.instFunLike map ofFractionRing CommRing.toCommMonoid Polynomial.commRing Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Submonoid.instSetLike Subtype.prop	—	Subtype.prop Submonoid.mem_comap
map_denom_ne_zero 📖	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield DFunLike.coe	—	—	denom_ne_zero map_eq_zero_iff
map_injective 📖	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 DFunLike.coe	RatFunc MonoidHom MulOneClass.toMulOne instCommRing MonoidHom.instFunLike map	—	Localization.induction_on ofFractionRing_injective One.instNonempty Subtype.prop MonoidHomClass.toMulHomClass
mk_eq_div 📖	mathematical	—	RatFunc instDiv DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Semiring.toNonAssocSemiring Polynomial.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id	—	Polynomial.nontrivial IsDomain.toNontrivial Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors mk_eq_div' ofFractionRing_div ofFractionRing_algebraMap
mk_eq_mk' 📖	mathematical	—	IsLocalization.mk' Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commSemiring nonZeroDivisors Semiring.toMonoidWithZero Polynomial.semiring RatFunc Semifield.toCommSemiring Field.toSemifield instField instAlgebraOfPolynomial Algebra.id instIsFractionRingPolynomial 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	—	instIsFractionRingPolynomial mem_nonZeroDivisors_iff_ne_zero Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors Polynomial.nontrivial IsDomain.toNontrivial mk_eq_div IsFractionRing.mk'_eq_div
mk_one 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instOne DFunLike.coe RingHom RatFunc Semiring.toNonAssocSemiring Polynomial.commSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id	—	—
mk_smul 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Polynomial.ring CommRing.toRing DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul RatFunc instSMulOfFractionRingPolynomial OreLocalization.instSMulOfIsScalarTower CommMonoid.toMonoid CommRing.toCommMonoid Polynomial.commRing nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm Monoid.toMulAction	—	mk_zero ofFractionRing_smul smul_zero mem_nonZeroDivisors_iff_ne_zero Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors Polynomial.nontrivial IsDomain.toNontrivial
monic_denom 📖	mathematical	—	Polynomial.Monic DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield denom	—	induction_on instIsDomain denom_div mul_comm Polynomial.monic_mul_leadingCoeff_inv right_div_gcd_ne_zero
mul_def 📖	mathematical	—	mul RatFunc ofFractionRing FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing OreLocalization.instMul CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm	—	—
mul_inv_cancel 📖	mathematical	—	RatFunc instMul instInv instOne	—	ofFractionRing_zero Polynomial.nontrivial IsDomain.toNontrivial Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors mul_inv_cancel₀
neg_def 📖	mathematical	—	neg RatFunc ofFractionRing FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing OreLocalization.instNegOreLocalization CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Polynomial.ring CommRing.toRing Module.toDistribMulAction Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule	—	—
numDenom_div 📖	mathematical	—	numDenom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain instDiv instIsDomain Field.toSemifield DFunLike.coe RingHom Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Polynomial.commSemiring Semifield.toCommSemiring instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id Polynomial.instMul Polynomial.semiring Polynomial.C InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Polynomial.leadingCoeff Polynomial.instDiv GCDMonoid.gcd CommSemiring.toCommMonoidWithZero NormalizedGCDMonoid.toGCDMonoid Polynomial.normalizedGcdMonoid CommGroupWithZero.instNormalizedGCDMonoid	—	instIsDomain numDenom.eq_1 liftOn'_div one_ne_zero' NeZero.one Polynomial.nontrivial EuclideanDomain.toNontrivial gcd_one_right EuclideanDomain.div_self Polynomial.Monic.leadingCoeff inv_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass EuclideanDomain.div_one MulZeroClass.mul_zero mul_one
num_algebraMap 📖	mathematical	—	num DFunLike.coe RingHom Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain Semiring.toNonAssocSemiring CommSemiring.toSemiring Polynomial.commSemiring Semifield.toCommSemiring instField instIsDomain RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id	—	instIsDomain map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass div_one gcd_one_right EuclideanDomain.div_self NeZero.one Polynomial.nontrivial EuclideanDomain.toNontrivial Polynomial.Monic.leadingCoeff inv_one EuclideanDomain.div_one one_mul num_div
num_denom_add 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instMul num RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain instAdd denom Polynomial.instAdd	—	instIsDomain num_mul_eq_mul_denom_iff mul_ne_zero Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors denom_ne_zero num_div_denom div_add_div algebraMap_ne_zero map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass
num_denom_mul 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instMul num RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain instMul denom	—	instIsDomain num_mul_eq_mul_denom_iff mul_ne_zero Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors denom_ne_zero num_div_denom div_mul_div_comm map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass
num_denom_neg 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instMul num RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain instNeg denom Polynomial.instNeg DivisionRing.toRing Field.toDivisionRing	—	instIsDomain num_mul_eq_mul_denom_iff denom_ne_zero map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass neg_div num_div_denom
num_div 📖	mathematical	—	num RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain instDiv instIsDomain Field.toSemifield DFunLike.coe RingHom Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Polynomial.commSemiring Semifield.toCommSemiring instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id Polynomial.instMul Polynomial.semiring Polynomial.C InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Polynomial.leadingCoeff Polynomial.instDiv GCDMonoid.gcd CommSemiring.toCommMonoidWithZero NormalizedGCDMonoid.toGCDMonoid Polynomial.normalizedGcdMonoid CommGroupWithZero.instNormalizedGCDMonoid	—	instIsDomain map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass div_zero num_zero gcd_zero_right EuclideanDomain.zero_div inv_zero MulZeroClass.zero_mul
num_div_denom 📖	mathematical	—	RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain instDiv instIsDomain Field.toSemifield DFunLike.coe RingHom Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring Polynomial.commSemiring Semifield.toCommSemiring instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id num denom	—	induction_on instIsDomain right_div_gcd_ne_zero num_div denom_div map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass mul_div_mul_left algebraMap_ne_zero Polynomial.C_eq_zero inv_ne_zero Polynomial.leadingCoeff_ne_zero div_eq_div_iff mul_comm EuclideanDomain.mul_div_assoc GCDMonoid.gcd_dvd_left GCDMonoid.gcd_dvd_right
num_div_dvd 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain num RatFunc instDiv instIsDomain DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Polynomial.commSemiring Semifield.toCommSemiring instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id	—	instIsDomain num_div Polynomial.C_mul_dvd right_div_gcd_ne_zero EuclideanDomain.div_dvd_of_dvd GCDMonoid.gcd_dvd_left
num_div_dvd' 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain Polynomial.instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.semiring RingHom.instFunLike Polynomial.C InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid DivisionCommMonoid.toDivisionMonoid CommGroupWithZero.toDivisionCommMonoid Semifield.toCommGroupWithZero Polynomial.leadingCoeff Polynomial.instDiv GCDMonoid.gcd CommSemiring.toCommMonoidWithZero Polynomial.commSemiring Semifield.toCommSemiring NormalizedGCDMonoid.toGCDMonoid Polynomial.normalizedGcdMonoid CommGroupWithZero.instNormalizedGCDMonoid	—	instIsDomain num_div num_div_dvd
num_dvd 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain num RatFunc instDiv instIsDomain DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Polynomial.commSemiring Semifield.toCommSemiring instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id	—	instIsDomain mul_ne_zero_iff Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass div_mul_div_comm div_self algebraMap_ne_zero mul_one num_div_denom mul_ne_zero denom_ne_zero num_div_dvd
num_eq_zero_iff 📖	mathematical	—	num Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instZero RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain instZero	—	instIsDomain num_div_denom map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass zero_div num_zero
num_inv_dvd 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain num RatFunc instInv instIsDomain denom	—	instIsDomain num_dvd denom_ne_zero num_ne_zero num_div_denom inv_div
num_mul_denom_add_denom_mul_num_ne_zero 📖	—	—	—	—	num_denom_add mul_ne_zero Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors instIsDomain num_ne_zero denom_ne_zero MulZeroClass.zero_mul
num_mul_dvd 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing Polynomial.commRing EuclideanDomain.toCommRing Field.toEuclideanDomain num RatFunc instMul Polynomial.instMul	—	MulZeroClass.zero_mul num_zero MulZeroClass.mul_zero instIsDomain num_dvd mul_ne_zero Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors num_ne_zero denom_ne_zero map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass div_mul_div_comm num_div_denom
num_mul_eq_mul_denom_iff 📖	mathematical	—	Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instMul num denom RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain instDiv instIsDomain DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring Polynomial.commSemiring Semifield.toCommSemiring instField RingHom.instFunLike algebraMap instAlgebraOfPolynomial Algebra.id	—	instIsDomain algebraMap_injective eq_div_iff algebraMap_ne_zero num_div_denom map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass div_eq_mul_inv mul_assoc mul_comm div_eq_iff denom_ne_zero
num_ne_zero 📖	—	—	—	—	num_eq_zero_iff
num_one 📖	mathematical	—	num RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain instOne Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instOne	—	instIsDomain map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass div_self NeZero.one instNontrivial EuclideanDomain.toNontrivial gcd_same MonoidWithZeroHom.monoidWithZeroHomClass EuclideanDomain.div_self Polynomial.nontrivial Polynomial.Monic.leadingCoeff inv_one mul_one num_div
num_zero 📖	mathematical	—	num RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain instZero Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Polynomial.instZero	—	instIsDomain map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass div_one gcd_one_right EuclideanDomain.div_self NeZero.one Polynomial.nontrivial EuclideanDomain.toNontrivial Polynomial.Monic.leadingCoeff inv_one EuclideanDomain.div_one MulZeroClass.mul_zero one_ne_zero
ofFractionRing_add 📖	mathematical	—	ofFractionRing FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing OreLocalization.instAdd CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Semiring.toModule RatFunc instAdd	—	add_def
ofFractionRing_algebraMap 📖	mathematical	—	ofFractionRing DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring FractionRing Polynomial.commRing Semiring.toNonAssocSemiring Polynomial.commSemiring OreLocalization.instSemiring nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm CommRing.toCommMonoid RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id RatFunc DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField instAlgebraOfPolynomial	—	mk_one mk_one'
ofFractionRing_comp_algebraMap 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring FractionRing Polynomial.commRing RatFunc ofFractionRing DFunLike.coe RingHom Semiring.toNonAssocSemiring Polynomial.commSemiring OreLocalization.instSemiring nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm CommRing.toCommMonoid RingHom.instFunLike algebraMap OreLocalization.instAlgebra Algebra.id DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField instAlgebraOfPolynomial	—	ofFractionRing_algebraMap
ofFractionRing_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 RatFunc instDiv	—	div_def
ofFractionRing_eq 📖	mathematical	—	ofFractionRing DFunLike.coe AlgEquiv Polynomial CommSemiring.toSemiring CommRing.toCommSemiring FractionRing Polynomial.commRing RatFunc Polynomial.commSemiring OreLocalization.instCommSemiring nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm CommRing.toCommMonoid Semifield.toCommSemiring Field.toSemifield instField OreLocalization.instAlgebra Algebra.id instAlgebraOfPolynomial AlgEquiv.instFunLike IsLocalization.algEquiv Polynomial.semiring Localization.isLocalization instIsFractionRingPolynomial	—	Localization.isLocalization instIsFractionRingPolynomial Localization.induction_on Localization.mk_eq_mk'_apply ofFractionRing_mk' IsLocalization.map_mk'
ofFractionRing_inv 📖	mathematical	—	ofFractionRing FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing OreLocalization.inv' Semiring.toMonoidWithZero Polynomial.nontrivial IsDomain.toNontrivial OreLocalization.oreSetComm CommRing.toCommMonoid nonZeroDivisors Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors RatFunc instInv	—	inv_def
ofFractionRing_mk' 📖	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 RatFunc Semifield.toCommSemiring Field.toSemifield instField instAlgebraOfPolynomial instIsFractionRingPolynomial	—	Localization.isLocalization instIsFractionRingPolynomial Polynomial.instIsDomainOfIsCancelAdd AddCancelMonoid.toIsCancelAdd IsFractionRing.mk'_eq_div Polynomial.nontrivial IsDomain.toNontrivial Polynomial.instNoZeroDivisors IsDomain.to_noZeroDivisors mk_eq_div' mk_eq_div
ofFractionRing_mul 📖	mathematical	—	ofFractionRing FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing OreLocalization.instMul CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm RatFunc instMul	—	mul_def
ofFractionRing_neg 📖	mathematical	—	ofFractionRing FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing OreLocalization.instNegOreLocalization CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Polynomial.ring CommRing.toRing Module.toDistribMulAction Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule RatFunc instNeg	—	neg_def
ofFractionRing_one 📖	mathematical	—	ofFractionRing FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing OreLocalization.instOne CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm Monoid.toMulAction Polynomial.instOne RatFunc instOne	—	one_def
ofFractionRing_smul 📖	mathematical	—	ofFractionRing FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing RatFunc instSMulOfFractionRingPolynomial	—	smul_def
ofFractionRing_sub 📖	mathematical	—	ofFractionRing FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing SubNegMonoid.toSub AddGroup.toSubNegMonoid OreLocalization.instAddGroupOreLocalization CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Polynomial.ring CommRing.toRing Module.toDistribMulAction Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule RatFunc instSub	—	sub_def
ofFractionRing_zero 📖	mathematical	—	ofFractionRing FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing OreLocalization.instZero CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm Polynomial.instZero Monoid.toMulAction RatFunc instZero	—	zero_def
one_def 📖	mathematical	—	one ofFractionRing FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing OreLocalization.instOne CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm Monoid.toMulAction Polynomial.instOne	—	—
rank_ratFunc_ratFunc 📖	mathematical	—	Module.rank RatFunc EuclideanDomain.toCommRing Field.toEuclideanDomain DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField instIsDomain NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRing Algebra.toModule Semifield.toCommSemiring liftAlgebra instAlgebraOfPolynomial Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commSemiring Polynomial.algebra faithfulSMul Module.Free.instFaithfulSMulOfNontrivial NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Module.Free.of_divisionRing Field.toDivisionRing Ring.toAddCommGroup DivisionRing.toRing EuclideanDomain.toNontrivial	—	instIsDomain faithfulSMul Module.Free.instFaithfulSMulOfNontrivial Module.Free.of_divisionRing EuclideanDomain.toNontrivial Algebra.IsAlgebraic.rank_of_isFractionRing instIsFractionRingPolynomial instFaithfulSMulPolynomial instIsAlgebraicPolynomialOfNoZeroDivisors_1 IsDomain.to_noZeroDivisors Polynomial.instNoZeroDivisors isScalarTower_liftAlgebra instIsScalarTowerPolynomial rank_polynomial_polynomial
smul_def 📖	mathematical	—	smul RatFunc ofFractionRing FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing	—	—
smul_eq_C_smul 📖	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 Polynomial.commSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike Polynomial.C	—	IsScalarTower.right Localization.induction_on ofFractionRing_smul smul_eq_mul Polynomial.smul_eq_C_mul
sub_def 📖	mathematical	—	sub RatFunc ofFractionRing FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing SubNegMonoid.toSub AddGroup.toSubNegMonoid OreLocalization.instAddGroupOreLocalization CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne Polynomial.ring CommRing.toRing Module.toDistribMulAction Ring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule	—	—
toFractionRingAlgEquiv_apply 📖	mathematical	—	DFunLike.coe AlgEquiv RatFunc FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield instField OreLocalization.instSemiring nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm CommRing.toCommMonoid instAlgebraOfPolynomial OreLocalization.instAlgebra AlgEquiv.instFunLike toFractionRingAlgEquiv toFractionRing	—	—
toFractionRingRingEquiv_apply 📖	mathematical	—	DFunLike.coe RingEquiv RatFunc FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing instMul OreLocalization.instMul CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm instAdd OreLocalization.instAdd AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Semiring.toModule EquivLike.toFunLike RingEquiv.instEquivLike toFractionRingRingEquiv toFractionRing	—	—
toFractionRingRingEquiv_symm_eq 📖	mathematical	—	RingEquiv.symm RatFunc FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing instMul OreLocalization.instMul CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm instAdd OreLocalization.instAdd AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Module.toDistribMulAction Ring.toSemiring CommRing.toRing Semiring.toModule toFractionRingRingEquiv AlgEquiv.toRingEquiv Polynomial.commSemiring OreLocalization.instCommSemiring Semifield.toCommSemiring Field.toSemifield instField OreLocalization.instAlgebra Algebra.id instAlgebraOfPolynomial IsLocalization.algEquiv Polynomial.semiring Localization.isLocalization instIsFractionRingPolynomial	—	RingEquiv.ext Localization.isLocalization instIsFractionRingPolynomial Equiv.left_inv ofFractionRing_eq toFractionRing_eq Equiv.right_inv RingEquiv.map_mul' RingEquiv.map_add'
toFractionRing_eq 📖	mathematical	—	toFractionRing DFunLike.coe AlgEquiv Polynomial CommSemiring.toSemiring CommRing.toCommSemiring RatFunc FractionRing Polynomial.commRing Polynomial.commSemiring Semifield.toCommSemiring Field.toSemifield instField OreLocalization.instCommSemiring nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm CommRing.toCommMonoid instAlgebraOfPolynomial Algebra.id OreLocalization.instAlgebra AlgEquiv.instFunLike IsLocalization.algEquiv Polynomial.semiring instIsFractionRingPolynomial Localization.isLocalization	—	instIsFractionRingPolynomial Localization.isLocalization Localization.induction_on Localization.mk_eq_mk'_apply ofFractionRing_mk' IsLocalization.map_mk'
toFractionRing_smul 📖	mathematical	—	toFractionRing RatFunc instSMulOfFractionRingPolynomial FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing	—	ofFractionRing_smul
zero_def 📖	mathematical	—	zero ofFractionRing FractionRing Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.commRing OreLocalization.instZero CommMonoid.toMonoid CommRing.toCommMonoid nonZeroDivisors Semiring.toMonoidWithZero OreLocalization.oreSetComm Polynomial.instZero Monoid.toMulAction	—	—

---

← Back to Index