UniversalFactorizationRing

📁 Source: Mathlib/RingTheory/Polynomial/UniversalFactorizationRing.lean

Statistics

Metric	Count
Definitions mapEquivMonic, universalFactorizationMap, universalFactorizationMapLiftEquiv, universalFactorizationMapPresentation, freeMonic, UniversalCoprimeFactorizationRing, factor₁, factor₂, homEquiv, UniversalFactorizationRing, factor₁, factor₂, fromTensor, homEquiv, monicDegreeEq, presentation, freeMonic, instAlgebraUniversalFactorizationRing, instCommRingUniversalFactorizationRing	19
Theorems exists_etale_bijective_residueFieldMap_and_map_eq_mul_and_isCoprime, coe_mapEquivMonic_comp, coe_mapEquivMonic_comp', finitePresentation_universalFactorizationMap, finite_universalFactorizationMap, ker_eval₂Hom_universalFactorizationMap, mapEquivMonic_symm_map, mapEquivMonic_symm_map_algebraMap, pderiv_inl_universalFactorizationMap_X, pderiv_inr_universalFactorizationMap_X, universalFactorizationMapPresentation_algebra_algebraMap, universalFactorizationMapPresentation_algebra_smul, universalFactorizationMapPresentation_jacobiMatrix, universalFactorizationMapPresentation_jacobian, universalFactorizationMapPresentation_map, universalFactorizationMapPresentation_relation, universalFactorizationMapPresentation_val, universalFactorizationMapPresentation_σ', universalFactorizationMap_comp_map, universalFactorizationMap_freeMonic, freeMonic_coe, exists_liesOver_residueFieldMap_bijective, factor₁_mul_factor₂, homEquiv_comp_fst, homEquiv_comp_snd, isCoprime_factor₁_factor₂, factor₁_mul_factor₂, fromTensor_comp_universalFactorizationMap, fromTensor_comp_universalFactorizationMap', jacobian_resentation, monicDegreeEq_coe, coeff_freeMonic, degree_freeMonic, instEtaleUniversalCoprimeFactorizationRing, instFinitePresentationUniversalFactorizationRing, instFiniteUniversalFactorizationRing, map_map_freeMonic, monic_freeMonic, natDegree_freeMonic	39
Total	58

Algebra

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_etale_bijective_residueFieldMap_and_map_eq_mul_and_isCoprime 📖	mathematical	Polynomial.Monic CommSemiring.toSemiring CommRing.toCommSemiring Ideal.ResidueField DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsLocalRing.ResidueField.field Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid Polynomial.map algebraMap IsLocalRing.ResidueField.algebra OreLocalization.instAlgebra id Polynomial Polynomial.instMul IsCoprime Polynomial.commSemiring Semifield.toCommSemiring	Function.Bijective DFunLike.coe AlgHom AlgHom.funLike Ideal.ResidueField.mapₐ ofId Ideal.over_def AlgHom.toRingHom	—	Polynomial.Monic.natDegree_map IsLocalRing.toNontrivial Field.instIsLocalRing Polynomial.Monic.natDegree_mul Ideal.over_def Polynomial.UniversalCoprimeFactorizationRing.exists_liesOver_residueFieldMap_bijective Polynomial.instEtaleUniversalCoprimeFactorizationRing Polynomial.MonicDegreeEq.monic Polynomial.UniversalCoprimeFactorizationRing.factor₁_mul_factor₂ Polynomial.UniversalCoprimeFactorizationRing.isCoprime_factor₁_factor₂

MvPolynomial

Definitions

Name	Category	Theorems
mapEquivMonic 📖	CompOp	6 math math: coe_mapEquivMonic_comp', mapEquivMonic_symm_map_algebraMap, mapEquivMonic_symm_map, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap', coe_mapEquivMonic_comp
universalFactorizationMap 📖	CompOp	17 math math: universalFactorizationMap_comp_map, finitePresentation_universalFactorizationMap, finite_universalFactorizationMap, universalFactorizationMapPresentation_map, universalFactorizationMapPresentation_relation, universalFactorizationMapPresentation_algebra_algebraMap, ker_eval₂Hom_universalFactorizationMap, pderiv_inr_universalFactorizationMap_X, universalFactorizationMapPresentation_algebra_smul, universalFactorizationMap_freeMonic, universalFactorizationMapPresentation_val, universalFactorizationMapPresentation_σ', universalFactorizationMapPresentation_jacobiMatrix, universalFactorizationMapPresentation_jacobian, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap', pderiv_inl_universalFactorizationMap_X
universalFactorizationMapLiftEquiv 📖	CompOp	—
universalFactorizationMapPresentation 📖	CompOp	8 math math: universalFactorizationMapPresentation_map, universalFactorizationMapPresentation_relation, universalFactorizationMapPresentation_algebra_algebraMap, universalFactorizationMapPresentation_algebra_smul, universalFactorizationMapPresentation_val, universalFactorizationMapPresentation_σ', universalFactorizationMapPresentation_jacobiMatrix, universalFactorizationMapPresentation_jacobian

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_mapEquivMonic_comp 📖	mathematical	—	Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.coeff AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DFunLike.coe Equiv AlgHom MvPolynomial commSemiring algebra Algebra.id Polynomial.MonicDegreeEq EquivLike.toFunLike Equiv.instEquivLike mapEquivMonic AlgHom.comp Polynomial.map RingHomClass.toRingHom AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass	—	Polynomial.map_map
coe_mapEquivMonic_comp' 📖	mathematical	—	DFunLike.coe Equiv AlgHom MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring commSemiring algebra Algebra.id Polynomial.MonicDegreeEq EquivLike.toFunLike Equiv.instEquivLike mapEquivMonic AlgHom.comp Polynomial.MonicDegreeEq.map RingHomClass.toRingHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass coe_mapEquivMonic_comp
finitePresentation_universalFactorizationMap 📖	mathematical	—	AlgHom.FinitePresentation MvPolynomial CommRing.toCommSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingMvPolynomial module CommSemiring.toSemiring Semiring.toModule Algebra.TensorProduct.instCommRing algebra Algebra.id commSemiring Algebra.TensorProduct.instAlgebra universalFactorizationMap	—	Algebra.Presentation.finitePresentation_of_isFinite Finite.of_fintype Finite.instSum
finite_universalFactorizationMap 📖	mathematical	—	AlgHom.Finite MvPolynomial CommRing.toCommSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingMvPolynomial module CommSemiring.toSemiring Semiring.toModule Algebra.TensorProduct.instCommRing algebra Algebra.id commSemiring Algebra.TensorProduct.instAlgebra universalFactorizationMap	—	RingHom.IsIntegral.to_finite MulEquiv.isDomain_iff smulCommClass Algebra.to_smulCommClass instIsDomainOfIsCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Int.instIsDomain AddGroup.int_smulCommClass' AddCommGroup.intIsScalarTower Commute.all Polynomial.coeff_map Polynomial.coeff_freeMonic Polynomial.isIntegral_coeff_of_dvd Polynomial.monic_freeMonic Polynomial.Monic.map AlgHomClass.toRingHomClass AlgHom.algHomClass universalFactorizationMap_freeMonic eval₂_X eval₂_one mul_one map_zero MonoidWithZeroHomClass.toZeroHomClass IsScalarTower.right RingHomClass.toMonoidWithZeroHomClass IsScalarTower.to_smulCommClass isScalarTower IsScalarTower.to_smulCommClass' TensorProduct.isScalarTower_right TensorProduct.CompatibleSMul.isScalarTower IsScalarTower.left TensorProduct.isScalarTower universalFactorizationMap_comp_map Polynomial.hom_eval₂ mul_comm one_mul TensorProduct.induction_on RingHom.isIntegralElem_zero RingHom.IsIntegralElem.mul induction_on algHom_C RingHom.isIntegralElem_map TensorProduct.add_tmul Algebra.algebraMap_eq_smul_one TensorProduct.tmul_smul map_smul SemilinearMapClass.toMulActionSemiHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass TensorProduct.tmul_add RingHom.IsIntegralElem.add RingHom.FiniteType.of_finitePresentation finitePresentation_universalFactorizationMap
ker_eval₂Hom_universalFactorizationMap 📖	mathematical	—	RingHom.ker MvPolynomial CommRing.toCommSemiring commSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingMvPolynomial module CommSemiring.toSemiring Semiring.toModule RingHom Semiring.toNonAssocSemiring Algebra.TensorProduct.instCommSemiring algebra Algebra.id RingHom.instFunLike RingHom.instRingHomClass eval₂Hom RingHomClass.toRingHom AlgHom Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass universalFactorizationMap TensorProduct.tmul X AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing Ideal.span Set.range SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup DFunLike.coe C map AlgEquiv NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule Algebra.TensorProduct.leftAlgebra smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.to_smulCommClass AlgEquiv.instFunLike tensorEquivSum	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.instRingHomClass smulCommClass Algebra.to_smulCommClass eval₂Hom_X' tensorEquivSum_X_tmul_one tensorEquivSum_one_tmul_X le_antisymm map_zero MonoidWithZeroHomClass.toZeroHomClass IsScalarTower.right RingHomClass.toMonoidWithZeroHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass sub_zero induction_on eval₂Hom_C algHom_C tensorEquivSum_C_tmul_one map_C sub_self AddSubmonoidClass.toZeroMemClass Submodule.addSubmonoidClass map_add AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass add_sub_add_comm AddMemClass.add_mem AddSubmonoidClass.toAddMemClass map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass NonUnitalAlgSemiHomClass.toMulHomClass Ideal.mul_sub_mul_mem Ideal.instIsTwoSided_1 Ideal.subset_span map_X Ideal.mul_mem_right map_sub eval₂Hom_map_hom AlgHom.comp_algebraMap_of_tower isScalarTower TensorProduct.isScalarTower Algebra.TensorProduct.ext algHom_ext IsScalarTower.to_smulCommClass aeval_X TensorProduct.isScalarTower_left
mapEquivMonic_symm_map 📖	mathematical	—	DFunLike.coe Equiv Polynomial.MonicDegreeEq CommSemiring.toSemiring CommRing.toCommSemiring AlgHom MvPolynomial commSemiring algebra Algebra.id EquivLike.toFunLike Equiv.instEquivLike Equiv.symm mapEquivMonic Polynomial.MonicDegreeEq.map RingHomClass.toRingHom AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.comp	—	AlgHomClass.toRingHomClass AlgHom.algHomClass Equiv.surjective Equiv.symm_apply_eq Equiv.symm_apply_apply coe_mapEquivMonic_comp'
mapEquivMonic_symm_map_algebraMap 📖	mathematical	—	DFunLike.coe Equiv Polynomial.MonicDegreeEq CommSemiring.toSemiring CommRing.toCommSemiring AlgHom MvPolynomial commSemiring algebra Algebra.id EquivLike.toFunLike Equiv.instEquivLike Equiv.symm mapEquivMonic Polynomial.MonicDegreeEq.map algebraMap AlgHom.comp IsScalarTower.toAlgHom	—	AlgHomClass.toRingHomClass AlgHom.algHomClass mapEquivMonic_symm_map IsScalarTower.coe_toAlgHom
pderiv_inl_universalFactorizationMap_X 📖	mathematical	—	DFunLike.coe Derivation MvPolynomial CommRing.toCommSemiring commSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring algebra Algebra.id Semiring.toModule module Derivation.instFunLike pderiv AlgEquiv TensorProduct Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.to_smulCommClass AlgEquiv.instFunLike tensorEquivSum AlgHom NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingMvPolynomial Algebra.TensorProduct.instAlgebra AlgHom.funLike universalFactorizationMap X MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	smulCommClass Algebra.to_smulCommClass IsScalarTower.right AlgHomClass.toRingHomClass AlgHom.algHomClass Polynomial.coeff_mul Finset.sum_congr Polynomial.coeff_map Polynomial.coeff_freeMonic TensorProduct.zero_tmul TensorProduct.tmul_zero dite_mul mul_one one_mul ite_mul MulZeroClass.zero_mul MulZeroClass.mul_zero aeval_X map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass tensorEquivSum_X_tmul_X tensorEquivSum_one_tmul_X map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass tensorEquivSum_X_tmul_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass Derivation.instAddMonoidHomClass Derivation.leibniz pderiv_X Pi.single_eq_of_ne Pi.single_apply zero_add add_zero AddMonoidHomClass.toZeroHomClass Derivation.map_one_eq_zero lt_or_ge Finset.sum_eq_zero Finset.sum_eq_single add_tsub_cancel_of_le CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instOrderedSub instIsEmptyFalse LE.le.not_gt
pderiv_inr_universalFactorizationMap_X 📖	mathematical	—	DFunLike.coe Derivation MvPolynomial CommRing.toCommSemiring commSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring CommSemiring.toSemiring algebra Algebra.id Semiring.toModule module Derivation.instFunLike pderiv AlgEquiv TensorProduct Algebra.toModule Algebra.TensorProduct.instSemiring Algebra.TensorProduct.leftAlgebra smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.to_smulCommClass AlgEquiv.instFunLike tensorEquivSum AlgHom NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingMvPolynomial Algebra.TensorProduct.instAlgebra AlgHom.funLike universalFactorizationMap X MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	smulCommClass Algebra.to_smulCommClass IsScalarTower.right AlgHomClass.toRingHomClass AlgHom.algHomClass Polynomial.coeff_mul Finset.sum_congr Polynomial.coeff_map Polynomial.coeff_freeMonic TensorProduct.zero_tmul TensorProduct.tmul_zero dite_mul mul_one one_mul ite_mul MulZeroClass.zero_mul MulZeroClass.mul_zero aeval_X map_sum DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass tensorEquivSum_X_tmul_X tensorEquivSum_one_tmul_X map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass tensorEquivSum_X_tmul_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass Derivation.instAddMonoidHomClass Derivation.leibniz pderiv_X Pi.single_apply Pi.single_eq_of_ne add_zero AddMonoidHomClass.toZeroHomClass Derivation.map_one_eq_zero lt_or_ge Finset.sum_eq_zero Finset.sum_eq_single instIsEmptyFalse LE.le.not_gt
universalFactorizationMapPresentation_algebra_algebraMap 📖	mathematical	—	Algebra.algebraMap MvPolynomial CommRing.toCommSemiring instCommRingMvPolynomial TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing module CommSemiring.toSemiring Semiring.toModule commSemiring Algebra.TensorProduct.instCommSemiring algebra Algebra.id Algebra.Generators.algebra Algebra.TensorProduct.instCommRing RingHom.toAlgebra AlgHom.toRingHom Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra universalFactorizationMap Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation universalFactorizationMapPresentation aeval TensorProduct.tmul X AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—
universalFactorizationMapPresentation_algebra_smul 📖	mathematical	—	MvPolynomial CommRing.toCommSemiring instCommRingMvPolynomial TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing module CommSemiring.toSemiring Semiring.toModule Algebra.toSMul commSemiring Algebra.TensorProduct.instCommSemiring algebra Algebra.id Algebra.Generators.algebra Algebra.TensorProduct.instCommRing RingHom.toAlgebra AlgHom.toRingHom Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra universalFactorizationMap Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation universalFactorizationMapPresentation Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DFunLike.coe RingHom RingHom.instFunLike aeval TensorProduct.tmul X AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—
universalFactorizationMapPresentation_jacobiMatrix 📖	mathematical	—	Algebra.PreSubmersivePresentation.jacobiMatrix MvPolynomial CommRing.toCommSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingMvPolynomial module CommSemiring.toSemiring Semiring.toModule Algebra.TensorProduct.instCommRing algebra Algebra.id commSemiring RingHom.toAlgebra Algebra.TensorProduct.instCommSemiring AlgHom.toRingHom Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra universalFactorizationMap universalFactorizationMapPresentation Fin.fintype Matrix Matrix.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing Matrix.transpose DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Matrix.reindex finCongr Polynomial.sylvester Polynomial.map AlgHom.comp mapAlgHom Algebra.ofId rename Polynomial.freeMonic	—	Matrix.ext AlgHomClass.toRingHomClass AlgHom.algHomClass Algebra.PreSubmersivePresentation.jacobiMatrix_apply Equiv.surjective finCongr_refl finSumFinEquiv_symm_apply_castAdd map_sub Derivation.instAddMonoidHomClass derivation_C pderiv_map smulCommClass Algebra.to_smulCommClass pderiv_inl_universalFactorizationMap_X map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_X map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass zero_sub Polynomial.coeff_map Polynomial.coeff_freeMonic rename_X eval₂_X eval₂_one eval₂_zero finSumFinEquiv_symm_apply_natAdd pderiv_inr_universalFactorizationMap_X
universalFactorizationMapPresentation_jacobian 📖	mathematical	—	Algebra.PreSubmersivePresentation.jacobian MvPolynomial CommRing.toCommSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingMvPolynomial module CommSemiring.toSemiring Semiring.toModule Algebra.TensorProduct.instCommRing algebra Algebra.id commSemiring RingHom.toAlgebra Algebra.TensorProduct.instCommSemiring AlgHom.toRingHom Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra universalFactorizationMap universalFactorizationMapPresentation Finite.of_fintype Fin.fintype Algebra.TensorProduct.instMul Algebra.to_smulCommClass IsScalarTower.right Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero TensorProduct.neg Ring.toAddCommGroup CommRing.toRing Algebra.TensorProduct.instOneTensorProduct NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Polynomial.resultant Polynomial.map Algebra.TensorProduct.includeLeftRingHom Polynomial.freeMonic NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule Algebra.TensorProduct.includeRight Polynomial.natDegree	—	subsingleton_or_nontrivial Finite.of_fintype Algebra.to_smulCommClass IsScalarTower.right Unique.instSubsingleton Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det universalFactorizationMapPresentation_jacobiMatrix AlgHomClass.toRingHomClass AlgHom.algHomClass Matrix.det_neg Fintype.card_fin Matrix.det_transpose Matrix.det_reindex_self map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_neg RingHomClass.toAddMonoidHomClass map_one MonoidHomClass.toOneHomClass Algebra.Generators.algebraMap_apply AlgHom.coe_toRingHom Polynomial.resultant_map_map Polynomial.map_map ringHom_ext' RingHom.ext AlgHom.commutes AlgHom.map_algebraMap isScalarTower IsScalarTower.of_algHom rename_X eval₂_X aeval_X AlgHom.comp_algebraMap_of_tower TensorProduct.isScalarTower Polynomial.Monic.natDegree_map Module.FaithfullyFlat.lTensor_nontrivial Module.FaithfullyFlat.instOfNontrivialOfFree nontrivial_of_nontrivial instFree Polynomial.monic_freeMonic Polynomial.natDegree_freeMonic
universalFactorizationMapPresentation_map 📖	mathematical	—	Algebra.PreSubmersivePresentation.map MvPolynomial CommRing.toCommSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingMvPolynomial module CommSemiring.toSemiring Semiring.toModule Algebra.TensorProduct.instCommRing algebra Algebra.id commSemiring RingHom.toAlgebra Algebra.TensorProduct.instCommSemiring AlgHom.toRingHom Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra universalFactorizationMap universalFactorizationMapPresentation DFunLike.coe Equiv EquivLike.toFunLike Equiv.instEquivLike Equiv.symm finSumFinEquiv finCongr	—	—
universalFactorizationMapPresentation_relation 📖	mathematical	—	Algebra.Presentation.relation MvPolynomial CommRing.toCommSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingMvPolynomial module CommSemiring.toSemiring Semiring.toModule Algebra.TensorProduct.instCommRing algebra Algebra.id commSemiring RingHom.toAlgebra Algebra.TensorProduct.instCommSemiring AlgHom.toRingHom Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra universalFactorizationMap Algebra.PreSubmersivePresentation.toPresentation universalFactorizationMapPresentation Algebra.Generators.Ring TensorProduct.tmul X AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike map C AlgEquiv NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule Algebra.TensorProduct.leftAlgebra AlgEquiv.instFunLike tensorEquivSum aeval SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup AlgHom AlgHom.funLike	—	—
universalFactorizationMapPresentation_val 📖	mathematical	—	Algebra.Generators.val MvPolynomial CommRing.toCommSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingMvPolynomial module CommSemiring.toSemiring Semiring.toModule Algebra.TensorProduct.instCommRing algebra Algebra.id commSemiring RingHom.toAlgebra Algebra.TensorProduct.instCommSemiring AlgHom.toRingHom Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra universalFactorizationMap Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation universalFactorizationMapPresentation TensorProduct.tmul X AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	—
universalFactorizationMapPresentation_σ' 📖	mathematical	—	Algebra.Generators.σ' MvPolynomial CommRing.toCommSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingMvPolynomial module CommSemiring.toSemiring Semiring.toModule Algebra.TensorProduct.instCommRing algebra Algebra.id commSemiring RingHom.toAlgebra Algebra.TensorProduct.instCommSemiring AlgHom.toRingHom Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra universalFactorizationMap Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation universalFactorizationMapPresentation DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike map C AlgEquiv NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule Algebra.TensorProduct.leftAlgebra AlgEquiv.instFunLike tensorEquivSum	—	—
universalFactorizationMap_comp_map 📖	mathematical	—	RingHom.comp MvPolynomial CommRing.toCommSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingMvPolynomial module CommSemiring.toSemiring Semiring.toModule Semiring.toNonAssocSemiring commSemiring Algebra.TensorProduct.instSemiring algebra Algebra.id AlgHom.toRingHom Algebra.TensorProduct.instAlgebra universalFactorizationMap map algebraMap NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule Algebra.TensorProduct.leftAlgebra IsScalarTower.to_smulCommClass isScalarTower Algebra.toSMul DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction IsScalarTower.right smulCommClass IsScalarTower.to_smulCommClass' Algebra.TensorProduct.lift TensorProduct.isScalarTower_right distribuMulAction TensorProduct.CompatibleSMul.isScalarTower AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing NonUnitalNonAssocSemiring.toDistribSMul IsScalarTower.left DistribMulAction.toMulAction AddCommMonoid.toAddMonoid AlgHom.comp Algebra.TensorProduct.includeLeft mapAlgHom Algebra.ofId AlgHom.restrictScalars TensorProduct.isScalarTower Algebra.TensorProduct.includeRight Commute.all NonUnitalNonAssocCommSemiring.toCommMagma NonUnitalNonAssocCommRing.toNonUnitalNonAssocCommSemiring Algebra.TensorProduct.instCommRing DFunLike.coe AlgHom AlgHom.funLike	—	ringHom_ext' IsScalarTower.to_smulCommClass isScalarTower IsScalarTower.right smulCommClass IsScalarTower.to_smulCommClass' TensorProduct.isScalarTower_right TensorProduct.CompatibleSMul.isScalarTower IsScalarTower.left TensorProduct.isScalarTower Commute.all RingHom.ext map_C algHom_C eval₂_one mul_one AlgHomClass.toRingHomClass AlgHom.algHomClass Polynomial.map_map_freeMonic Polynomial.map_map map_X aeval_X Polynomial.map_mul AlgHom.map_algebraMap eval₂_X one_mul
universalFactorizationMap_freeMonic 📖	mathematical	—	Polynomial.map MvPolynomial CommRing.toCommSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingMvPolynomial module CommSemiring.toSemiring Semiring.toModule commSemiring Algebra.TensorProduct.instSemiring algebra Algebra.id RingHomClass.toRingHom AlgHom Algebra.TensorProduct.instAlgebra AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass universalFactorizationMap Polynomial.freeMonic Polynomial NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule Polynomial.instMul algebraMap Algebra.TensorProduct.leftAlgebra Algebra.to_smulCommClass Algebra.TensorProduct.includeRight	—	AlgHomClass.toRingHomClass AlgHom.algHomClass Algebra.to_smulCommClass Equiv.apply_symm_apply

Polynomial

Definitions

Name	Category	Theorems
UniversalCoprimeFactorizationRing 📖	CompOp	6 math math: UniversalCoprimeFactorizationRing.exists_liesOver_residueFieldMap_bijective, UniversalCoprimeFactorizationRing.homEquiv_comp_snd, UniversalCoprimeFactorizationRing.homEquiv_comp_fst, UniversalCoprimeFactorizationRing.factor₁_mul_factor₂, UniversalCoprimeFactorizationRing.isCoprime_factor₁_factor₂, instEtaleUniversalCoprimeFactorizationRing
UniversalFactorizationRing 📖	CompOp	13 math math: instFinitePresentationUniversalFactorizationRing, UniversalCoprimeFactorizationRing.exists_liesOver_residueFieldMap_bijective, UniversalCoprimeFactorizationRing.homEquiv_comp_snd, UniversalFactorizationRing.jacobian_resentation, UniversalCoprimeFactorizationRing.homEquiv_comp_fst, UniversalFactorizationRing.monicDegreeEq_coe, UniversalFactorizationRing.factor₁_mul_factor₂, UniversalCoprimeFactorizationRing.factor₁_mul_factor₂, instFiniteUniversalFactorizationRing, UniversalCoprimeFactorizationRing.isCoprime_factor₁_factor₂, instEtaleUniversalCoprimeFactorizationRing, UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap, UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap'
freeMonic 📖	CompOp	9 math math: MonicDegreeEq.freeMonic_coe, degree_freeMonic, monic_freeMonic, natDegree_freeMonic, MvPolynomial.universalFactorizationMap_freeMonic, MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix, map_map_freeMonic, MvPolynomial.universalFactorizationMapPresentation_jacobian, coeff_freeMonic
instAlgebraUniversalFactorizationRing 📖	CompOp	12 math math: instFinitePresentationUniversalFactorizationRing, UniversalCoprimeFactorizationRing.exists_liesOver_residueFieldMap_bijective, UniversalCoprimeFactorizationRing.homEquiv_comp_snd, UniversalFactorizationRing.jacobian_resentation, UniversalCoprimeFactorizationRing.homEquiv_comp_fst, UniversalFactorizationRing.monicDegreeEq_coe, UniversalCoprimeFactorizationRing.factor₁_mul_factor₂, instFiniteUniversalFactorizationRing, UniversalCoprimeFactorizationRing.isCoprime_factor₁_factor₂, instEtaleUniversalCoprimeFactorizationRing, UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap, UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap'
instCommRingUniversalFactorizationRing 📖	CompOp	13 math math: instFinitePresentationUniversalFactorizationRing, UniversalCoprimeFactorizationRing.exists_liesOver_residueFieldMap_bijective, UniversalCoprimeFactorizationRing.homEquiv_comp_snd, UniversalFactorizationRing.jacobian_resentation, UniversalCoprimeFactorizationRing.homEquiv_comp_fst, UniversalFactorizationRing.monicDegreeEq_coe, UniversalFactorizationRing.factor₁_mul_factor₂, UniversalCoprimeFactorizationRing.factor₁_mul_factor₂, instFiniteUniversalFactorizationRing, UniversalCoprimeFactorizationRing.isCoprime_factor₁_factor₂, instEtaleUniversalCoprimeFactorizationRing, UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap, UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap'

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coeff_freeMonic 📖	mathematical	—	coeff MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring freeMonic MvPolynomial.X AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing MvPolynomial.instCommRingMvPolynomial MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	coeff_add coeff_X_pow finset_sum_coeff Finset.sum_congr coeff_C_mul mul_ite mul_one MulZeroClass.mul_zero LT.lt.ne' Finset.sum_eq_single instIsEmptyFalse zero_add Finset.sum_eq_zero add_zero
degree_freeMonic 📖	mathematical	—	degree MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring freeMonic WithBot AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne	—	degree_eq_of_le_of_coeff_ne_zero degree_le_iff_coeff_zero WithBot.addLeftMono IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid WithBot.zeroLEOneClass Nat.instZeroLEOneClass WithBot.charZero Nat.instCharZero coeff_freeMonic NeZero.one MvPolynomial.nontrivial_of_nontrivial
instEtaleUniversalCoprimeFactorizationRing 📖	mathematical	—	Algebra.Etale UniversalCoprimeFactorizationRing OreLocalization.instCommRing UniversalFactorizationRing instCommRingUniversalFactorizationRing Submonoid.powers CommMonoid.toMonoid CommRing.toCommMonoid Algebra.PreSubmersivePresentation.jacobian instAlgebraUniversalFactorizationRing UniversalFactorizationRing.presentation OreLocalization.oreSetComm OreLocalization.instAlgebra CommSemiring.toSemiring CommRing.toCommSemiring	—	Finite.of_fintype IsLocalization.Away.algebraMap_isUnit Localization.isLocalization Finite.instSum OreLocalization.instIsScalarTower IsScalarTower.right Algebra.PreSubmersivePresentation.comp_jacobian_eq_jacobian_smul_jacobian Algebra.PreSubmersivePresentation.localizationAway_jacobian Algebra.smul_def instIsDedekindFiniteMonoid Algebra.PreSubmersivePresentation.dimension_comp_eq_dimension_add_dimension Nat.card_eq_fintype_card Fintype.card_unique tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub Fintype.card_sum Fintype.card_fin add_zero Algebra.instEtaleOfIsStandardSmoothOfRelativeDimensionOfNatNat
instFinitePresentationUniversalFactorizationRing 📖	mathematical	—	Algebra.FinitePresentation UniversalFactorizationRing CommRing.toCommSemiring CommSemiring.toSemiring instCommRingUniversalFactorizationRing instAlgebraUniversalFactorizationRing	—	Algebra.FinitePresentation.baseChange MvPolynomial.finitePresentation_universalFactorizationMap
instFiniteUniversalFactorizationRing 📖	mathematical	—	Module.Finite UniversalFactorizationRing CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingUniversalFactorizationRing Algebra.toModule instAlgebraUniversalFactorizationRing	—	Module.Finite.base_change MvPolynomial.finite_universalFactorizationMap
map_map_freeMonic 📖	mathematical	—	map MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring MvPolynomial.map freeMonic	—	map_add map_pow map_X map_sum Finset.sum_congr map_mul map_C MvPolynomial.map_X
monic_freeMonic 📖	mathematical	—	Monic MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring freeMonic	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton Monic.leadingCoeff natDegree_freeMonic coeff_freeMonic
natDegree_freeMonic 📖	mathematical	—	natDegree MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring freeMonic	—	natDegree_eq_of_degree_eq_some degree_freeMonic

Polynomial.MonicDegreeEq

Definitions

Name	Category	Theorems
freeMonic 📖	CompOp	1 math math: freeMonic_coe

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
freeMonic_coe 📖	mathematical	—	Polynomial MvPolynomial CommRing.toCommSemiring CommSemiring.toSemiring MvPolynomial.commSemiring Polynomial.coeff AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring freeMonic Polynomial.freeMonic	—	—

Polynomial.UniversalCoprimeFactorizationRing

Definitions

Name	Category	Theorems
factor₁ 📖	CompOp	3 math math: exists_liesOver_residueFieldMap_bijective, factor₁_mul_factor₂, isCoprime_factor₁_factor₂
factor₂ 📖	CompOp	3 math math: exists_liesOver_residueFieldMap_bijective, factor₁_mul_factor₂, isCoprime_factor₁_factor₂
homEquiv 📖	CompOp	2 math math: homEquiv_comp_snd, homEquiv_comp_fst

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
exists_liesOver_residueFieldMap_bijective 📖	mathematical	Polynomial.map Ideal.ResidueField CommSemiring.toSemiring CommRing.toCommSemiring DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsLocalRing.ResidueField.field Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid algebraMap IsLocalRing.ResidueField.algebra OreLocalization.instAlgebra Algebra.id Polynomial Polynomial.coeff AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Polynomial.instMul IsCoprime Polynomial.commSemiring Semifield.toCommSemiring	Function.Bijective Polynomial.UniversalCoprimeFactorizationRing Polynomial.UniversalFactorizationRing Polynomial.instCommRingUniversalFactorizationRing Submonoid.powers CommMonoid.toMonoid CommRing.toCommMonoid Algebra.PreSubmersivePresentation.jacobian Polynomial.instAlgebraUniversalFactorizationRing Polynomial.UniversalFactorizationRing.presentation DFunLike.coe AlgHom AlgHom.funLike Ideal.ResidueField.mapₐ Algebra.ofId Ideal.over_def OreLocalization.instSemiring Polynomial.MonicDegreeEq.map AlgHom.toRingHom factor₁ OreLocalization.instCommSemiring factor₂	—	RingHom.instRingHomClass RingHom.ker_isPrime instIsDomain Ideal.under.eq_1 RingHom.comap_ker AlgHomClass.toRingHomClass AlgHom.algHomClass AlgHom.toRingHom_eq_coe AlgHom.comp_algebraMap Ideal.ker_algebraMap_residueField le_rfl MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass instIsConcreteLE Ideal.over_def AlgHom.ext RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing Ideal.ResidueField.algHom_ext Algebra.ext_id IsLocalRing.instIsScalarTowerResidueField OreLocalization.instIsScalarTower IsScalarTower.right AlgEquiv.eq_symm_apply Ideal.ResidueField.liftₐ_algebraMap AlgEquiv.bijective homEquiv_comp_fst Equiv.apply_symm_apply Polynomial.map_map homEquiv_comp_snd
factor₁_mul_factor₂ 📖	mathematical	—	Polynomial Polynomial.UniversalCoprimeFactorizationRing OreLocalization.instSemiring Polynomial.UniversalFactorizationRing CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instCommRingUniversalFactorizationRing Submonoid.powers CommMonoid.toMonoid CommRing.toCommMonoid Algebra.PreSubmersivePresentation.jacobian Polynomial.instAlgebraUniversalFactorizationRing Polynomial.UniversalFactorizationRing.presentation OreLocalization.oreSetComm Polynomial.instMul Polynomial.coeff AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring factor₁ factor₂ Polynomial.MonicDegreeEq.map algebraMap OreLocalization.instAlgebra	—	Polynomial.UniversalFactorizationRing.factor₁_mul_factor₂ Polynomial.map_map OreLocalization.instIsScalarTower IsScalarTower.right
homEquiv_comp_fst 📖	mathematical	—	Polynomial.MonicDegreeEq CommSemiring.toSemiring CommRing.toCommSemiring Polynomial Polynomial.instMul Polynomial.coeff AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Polynomial.map algebraMap IsCoprime Polynomial.commSemiring DFunLike.coe Equiv AlgHom Polynomial.UniversalCoprimeFactorizationRing OreLocalization.instSemiring Polynomial.UniversalFactorizationRing Polynomial.instCommRingUniversalFactorizationRing Submonoid.powers CommMonoid.toMonoid CommRing.toCommMonoid Algebra.PreSubmersivePresentation.jacobian Polynomial.instAlgebraUniversalFactorizationRing Polynomial.UniversalFactorizationRing.presentation OreLocalization.oreSetComm OreLocalization.instAlgebra EquivLike.toFunLike Equiv.instEquivLike homEquiv AlgHom.comp Polynomial.MonicDegreeEq.map RingHomClass.toRingHom AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass Polynomial.map_map
homEquiv_comp_snd 📖	mathematical	—	Polynomial.MonicDegreeEq CommSemiring.toSemiring CommRing.toCommSemiring Polynomial Polynomial.instMul Polynomial.coeff AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Polynomial.map algebraMap IsCoprime Polynomial.commSemiring DFunLike.coe Equiv AlgHom Polynomial.UniversalCoprimeFactorizationRing OreLocalization.instSemiring Polynomial.UniversalFactorizationRing Polynomial.instCommRingUniversalFactorizationRing Submonoid.powers CommMonoid.toMonoid CommRing.toCommMonoid Algebra.PreSubmersivePresentation.jacobian Polynomial.instAlgebraUniversalFactorizationRing Polynomial.UniversalFactorizationRing.presentation OreLocalization.oreSetComm OreLocalization.instAlgebra EquivLike.toFunLike Equiv.instEquivLike homEquiv AlgHom.comp Polynomial.MonicDegreeEq.map RingHomClass.toRingHom AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass	—	AlgHomClass.toRingHomClass AlgHom.algHomClass Polynomial.map_map
isCoprime_factor₁_factor₂ 📖	mathematical	—	IsCoprime Polynomial Polynomial.UniversalCoprimeFactorizationRing OreLocalization.instSemiring Polynomial.UniversalFactorizationRing CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instCommRingUniversalFactorizationRing Submonoid.powers CommMonoid.toMonoid CommRing.toCommMonoid Algebra.PreSubmersivePresentation.jacobian Polynomial.instAlgebraUniversalFactorizationRing Polynomial.UniversalFactorizationRing.presentation OreLocalization.oreSetComm Polynomial.commSemiring OreLocalization.instCommSemiring Polynomial.coeff AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring factor₁ factor₂	—	subsingleton_or_nontrivial Unique.instSubsingleton isCoprime_one_left Polynomial.isUnit_resultant_iff_isCoprime Polynomial.MonicDegreeEq.monic factor₁.eq_1 factor₂.eq_1 Polynomial.MonicDegreeEq.map_coe Polynomial.resultant_map_map Polynomial.Monic.natDegree_map IsUnit.mul_iff instIsDedekindFiniteMonoid map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Finite.of_fintype Polynomial.UniversalFactorizationRing.jacobian_resentation IsLocalization.Away.algebraMap_isUnit Localization.isLocalization

Polynomial.UniversalFactorizationRing

Definitions

Name	Category	Theorems
factor₁ 📖	CompOp	2 math math: jacobian_resentation, factor₁_mul_factor₂
factor₂ 📖	CompOp	2 math math: jacobian_resentation, factor₁_mul_factor₂
fromTensor 📖	CompOp	2 math math: fromTensor_comp_universalFactorizationMap, fromTensor_comp_universalFactorizationMap'
homEquiv 📖	CompOp	—
monicDegreeEq 📖	CompOp	3 math math: monicDegreeEq_coe, factor₁_mul_factor₂, fromTensor_comp_universalFactorizationMap'
presentation 📖	CompOp	7 math math: Polynomial.UniversalCoprimeFactorizationRing.exists_liesOver_residueFieldMap_bijective, Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_snd, jacobian_resentation, Polynomial.UniversalCoprimeFactorizationRing.homEquiv_comp_fst, Polynomial.UniversalCoprimeFactorizationRing.factor₁_mul_factor₂, Polynomial.UniversalCoprimeFactorizationRing.isCoprime_factor₁_factor₂, Polynomial.instEtaleUniversalCoprimeFactorizationRing

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
factor₁_mul_factor₂ 📖	mathematical	—	Polynomial Polynomial.UniversalFactorizationRing CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instCommRingUniversalFactorizationRing Polynomial.instMul Polynomial.coeff AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring factor₁ factor₂ monicDegreeEq	—	fromTensor_comp_universalFactorizationMap'
fromTensor_comp_universalFactorizationMap 📖	mathematical	—	AlgHom.comp MvPolynomial CommRing.toCommSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial MvPolynomial.module CommSemiring.toSemiring Semiring.toModule Polynomial.UniversalFactorizationRing MvPolynomial.commSemiring Algebra.TensorProduct.instSemiring MvPolynomial.algebra Algebra.id Polynomial.instCommRingUniversalFactorizationRing Algebra.TensorProduct.instAlgebra Polynomial.instAlgebraUniversalFactorizationRing fromTensor MvPolynomial.universalFactorizationMap Algebra.ofId DFunLike.coe Equiv Polynomial.MonicDegreeEq AlgHom EquivLike.toFunLike Equiv.instEquivLike Equiv.symm MvPolynomial.mapEquivMonic	—	AlgHom.ext Algebra.TensorProduct.tmul_one_eq_one_tmul
fromTensor_comp_universalFactorizationMap' 📖	mathematical	—	AlgHom.comp MvPolynomial CommRing.toCommSemiring TensorProduct NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing MvPolynomial.instCommRingMvPolynomial MvPolynomial.module CommSemiring.toSemiring Semiring.toModule Polynomial.UniversalFactorizationRing MvPolynomial.commSemiring Algebra.TensorProduct.instSemiring MvPolynomial.algebra Algebra.id Polynomial.instCommRingUniversalFactorizationRing Algebra.TensorProduct.instAlgebra Polynomial.instAlgebraUniversalFactorizationRing fromTensor MvPolynomial.universalFactorizationMap DFunLike.coe Equiv Polynomial.MonicDegreeEq AlgHom EquivLike.toFunLike Equiv.instEquivLike Equiv.symm MvPolynomial.mapEquivMonic monicDegreeEq	—	fromTensor_comp_universalFactorizationMap Equiv.eq_symm_apply AlgHomClass.toRingHomClass AlgHom.algHomClass MvPolynomial.coe_mapEquivMonic_comp Equiv.apply_symm_apply
jacobian_resentation 📖	mathematical	—	Algebra.PreSubmersivePresentation.jacobian Polynomial.UniversalFactorizationRing Polynomial.instCommRingUniversalFactorizationRing Polynomial.instAlgebraUniversalFactorizationRing presentation Finite.of_fintype Fin.fintype Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne Polynomial.resultant Polynomial Polynomial.coeff AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring factor₁ factor₂ Polynomial.natDegree	—	subsingleton_or_nontrivial Finite.of_fintype AlgHomClass.toRingHomClass AlgHom.algHomClass Unique.instSubsingleton Algebra.to_smulCommClass Algebra.PreSubmersivePresentation.baseChange_jacobian IsScalarTower.right MvPolynomial.universalFactorizationMapPresentation_jacobian map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass map_neg DistribMulActionSemiHomClass.toAddMonoidHomClass NonUnitalAlgSemiHomClass.toDistribMulActionSemiHomClass map_one MonoidHomClass.toOneHomClass AlgHom.coe_toRingHom Polynomial.resultant_map_map Polynomial.map_map Polynomial.Monic.natDegree_map Polynomial.monic_freeMonic Polynomial.MonicDegreeEq.natDegree Polynomial.natDegree_freeMonic
monicDegreeEq_coe 📖	mathematical	—	Polynomial Polynomial.UniversalFactorizationRing CommSemiring.toSemiring CommRing.toCommSemiring Polynomial.instCommRingUniversalFactorizationRing Polynomial.coeff AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring monicDegreeEq Polynomial.map algebraMap Polynomial.instAlgebraUniversalFactorizationRing	—	—

---

← Back to Index