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	CommRing Algebra CommRing.toCommSemiring CommSemiring.toSemiring Etale Ideal Ideal.IsPrime Ideal.LiesOver Polynomial Function.Bijective Ideal.ResidueField DFunLike.coe AlgHom DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsLocalRing.ResidueField.field Localization.AtPrime OreLocalization.instCommRing Ideal.primeCompl OreLocalization.oreSetComm CommSemiring.toCommMonoid IsLocalRing.ResidueField.algebra OreLocalization.instAlgebra id AlgHom.funLike Ideal.ResidueField.mapₐ ofId Ideal.over_def Polynomial.Monic Polynomial.map algebraMap Polynomial.instMul IsCoprime Polynomial.commSemiring 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 AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.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 AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.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 AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring instModuleMvPolynomialOfAlgebra Algebra.id AddMonoidAlgebra.commRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid Algebra.TensorProduct.instCommRing AddMonoidAlgebra.algebra AddCommMonoid.toAddMonoid AddMonoidAlgebra.commSemiring Finsupp.instAddMonoid Nat.instAddMonoid Algebra.TensorProduct.instAlgebra AddMonoidAlgebra.semiring universalFactorizationMap	—	Algebra.Presentation.finitePresentation_of_isFinite Finite.of_fintype Finite.instSum
finite_universalFactorizationMap 📖	mathematical	—	AlgHom.Finite MvPolynomial CommRing.toCommSemiring TensorProduct AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring instModuleMvPolynomialOfAlgebra Algebra.id AddMonoidAlgebra.commRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid Algebra.TensorProduct.instCommRing AddMonoidAlgebra.algebra AddCommMonoid.toAddMonoid AddMonoidAlgebra.commSemiring Finsupp.instAddMonoid Nat.instAddMonoid Algebra.TensorProduct.instAlgebra AddMonoidAlgebra.semiring universalFactorizationMap	—	RingHom.IsIntegral.to_finite MulEquiv.isDomain_iff AddMonoidAlgebra.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 AddMonoidAlgebra.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 AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid TensorProduct AddMonoidAlgebra.addAddCommMonoid CommSemiring.toSemiring instModuleMvPolynomialOfAlgebra Algebra.id RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring Algebra.TensorProduct.instCommSemiring AddMonoidAlgebra.algebra AddCommMonoid.toAddMonoid AddMonoidAlgebra.semiring Finsupp.instAddMonoid Algebra.TensorProduct.instSemiring RingHom.instFunLike RingHom.instRingHomClass eval₂Hom RingHomClass.toRingHom AlgHom Algebra.TensorProduct.instAlgebra AlgHom.funLike AlgHomClass.toRingHomClass AlgHom.algHomClass universalFactorizationMap TensorProduct.tmul X AddMonoidAlgebra.zero Finsupp.instZero Ideal.span Set.range SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidAlgebra.ring CommRing.toRing DFunLike.coe C map AlgEquiv AddMonoidAlgebra.module Algebra.toModule Semiring.toModule Algebra.TensorProduct.leftAlgebra AddMonoidAlgebra.smulCommClass DistribSMul.toSMulZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.to_smulCommClass AlgEquiv.instFunLike tensorEquivSum	—	AlgHomClass.toRingHomClass AlgHom.algHomClass RingHom.instRingHomClass AddMonoidAlgebra.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 AddMonoidAlgebra.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 AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.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 AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddMonoid Nat.instAddMonoid AddMonoidAlgebra.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 AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.addAddCommMonoid CommSemiring.toSemiring AddMonoidAlgebra.algebra Algebra.id AddCommMonoid.toAddMonoid Semiring.toModule AddMonoidAlgebra.module Derivation.instFunLike pderiv AlgEquiv TensorProduct Algebra.toModule Algebra.TensorProduct.instSemiring AddMonoidAlgebra.semiring Finsupp.instAddMonoid Nat.instAddMonoid Algebra.TensorProduct.leftAlgebra AddMonoidAlgebra.smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.to_smulCommClass AlgEquiv.instFunLike tensorEquivSum AlgHom instModuleMvPolynomialOfAlgebra Algebra.TensorProduct.instAlgebra AlgHom.funLike universalFactorizationMap X NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp.instAdd AddMonoidAlgebra.zero Finsupp.instZero	—	AddMonoidAlgebra.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 AddMonoidAlgebra.commSemiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.addAddCommMonoid CommSemiring.toSemiring AddMonoidAlgebra.algebra Algebra.id AddCommMonoid.toAddMonoid Semiring.toModule AddMonoidAlgebra.module Derivation.instFunLike pderiv AlgEquiv TensorProduct Algebra.toModule Algebra.TensorProduct.instSemiring AddMonoidAlgebra.semiring Finsupp.instAddMonoid Nat.instAddMonoid Algebra.TensorProduct.leftAlgebra AddMonoidAlgebra.smulCommClass DistribSMul.toSMulZeroClass AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.to_smulCommClass AlgEquiv.instFunLike tensorEquivSum AlgHom instModuleMvPolynomialOfAlgebra Algebra.TensorProduct.instAlgebra AlgHom.funLike universalFactorizationMap X NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp.instAdd AddMonoidAlgebra.zero Finsupp.instZero	—	AddMonoidAlgebra.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 AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid TensorProduct AddMonoidAlgebra.addAddCommMonoid CommSemiring.toSemiring instModuleMvPolynomialOfAlgebra Algebra.id AddMonoidAlgebra.commSemiring Algebra.TensorProduct.instCommSemiring AddMonoidAlgebra.algebra AddCommMonoid.toAddMonoid Algebra.Generators.algebra Algebra.TensorProduct.instCommRing RingHom.toAlgebra AlgHom.toRingHom AddMonoidAlgebra.semiring Finsupp.instAddMonoid Nat.instAddMonoid Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra universalFactorizationMap Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation universalFactorizationMapPresentation aeval TensorProduct.tmul X AddMonoidAlgebra.zero Finsupp.instZero	—	—
universalFactorizationMapPresentation_algebra_smul 📖	mathematical	—	MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.commRing Finsupp MulZeroClass.toZero Nat.instMulZeroClass Finsupp.instAddCommMonoid Nat.instAddCommMonoid TensorProduct AddMonoidAlgebra.addAddCommMonoid CommSemiring.toSemiring instModuleMvPolynomialOfAlgebra Algebra.id Algebra.toSMul AddMonoidAlgebra.commSemiring Algebra.TensorProduct.instCommSemiring AddMonoidAlgebra.algebra AddCommMonoid.toAddMonoid Algebra.Generators.algebra Algebra.TensorProduct.instCommRing RingHom.toAlgebra AlgHom.toRingHom AddMonoidAlgebra.semiring Finsupp.instAddMonoid Nat.instAddMonoid 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 AddMonoidAlgebra.zero Finsupp.instZero	—	—
universalFactorizationMapPresentation_jacobiMatrix 📖	mathematical	—	Algebra.PreSubmersivePresentation.jacobiMatrix MvPolynomial CommRing.toCommSemiring TensorProduct AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring instModuleMvPolynomialOfAlgebra Algebra.id AddMonoidAlgebra.commRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid Algebra.TensorProduct.instCommRing AddMonoidAlgebra.algebra AddCommMonoid.toAddMonoid AddMonoidAlgebra.commSemiring RingHom.toAlgebra Algebra.TensorProduct.instCommSemiring AlgHom.toRingHom AddMonoidAlgebra.semiring Finsupp.instAddMonoid Nat.instAddMonoid Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra universalFactorizationMap universalFactorizationMapPresentation Fin.fintype Matrix Matrix.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid AddMonoidAlgebra.addAddCommGroup AddMonoidAlgebra.ring 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 AddMonoidAlgebra.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 AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring instModuleMvPolynomialOfAlgebra Algebra.id AddMonoidAlgebra.commRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid Algebra.TensorProduct.instCommRing AddMonoidAlgebra.algebra AddCommMonoid.toAddMonoid AddMonoidAlgebra.commSemiring RingHom.toAlgebra Algebra.TensorProduct.instCommSemiring AlgHom.toRingHom AddMonoidAlgebra.semiring Finsupp.instAddMonoid Nat.instAddMonoid Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra universalFactorizationMap universalFactorizationMapPresentation Finite.of_fintype Fin.fintype Algebra.TensorProduct.instMul AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp.instAdd AddMonoid.toAddZeroClass Algebra.to_smulCommClass IsScalarTower.right Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero TensorProduct.neg AddMonoidAlgebra.addAddCommGroup CommRing.toRing Algebra.TensorProduct.instOneTensorProduct NonAssocSemiring.toAddCommMonoidWithOne AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass Polynomial.resultant Polynomial.map Algebra.TensorProduct.includeLeftRingHom Polynomial.freeMonic NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring 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 AddMonoidAlgebra.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 AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring instModuleMvPolynomialOfAlgebra Algebra.id AddMonoidAlgebra.commRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid Algebra.TensorProduct.instCommRing AddMonoidAlgebra.algebra AddCommMonoid.toAddMonoid AddMonoidAlgebra.commSemiring RingHom.toAlgebra Algebra.TensorProduct.instCommSemiring AlgHom.toRingHom AddMonoidAlgebra.semiring Finsupp.instAddMonoid Nat.instAddMonoid 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 AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring instModuleMvPolynomialOfAlgebra Algebra.id AddMonoidAlgebra.commRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid Algebra.TensorProduct.instCommRing AddMonoidAlgebra.algebra AddCommMonoid.toAddMonoid AddMonoidAlgebra.commSemiring RingHom.toAlgebra Algebra.TensorProduct.instCommSemiring AlgHom.toRingHom AddMonoidAlgebra.semiring Finsupp.instAddMonoid Nat.instAddMonoid Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra universalFactorizationMap Algebra.PreSubmersivePresentation.toPresentation universalFactorizationMapPresentation Algebra.Generators.Ring TensorProduct.tmul X AddMonoidAlgebra.zero Finsupp.instZero DFunLike.coe RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike map C AlgEquiv AddMonoidAlgebra.module Algebra.toModule Semiring.toModule Algebra.TensorProduct.leftAlgebra AlgEquiv.instFunLike tensorEquivSum aeval SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne AddMonoidAlgebra.ring CommRing.toRing Semiring.toNonAssocSemiring AlgHom AlgHom.funLike	—	—
universalFactorizationMapPresentation_val 📖	mathematical	—	Algebra.Generators.val MvPolynomial CommRing.toCommSemiring TensorProduct AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring instModuleMvPolynomialOfAlgebra Algebra.id AddMonoidAlgebra.commRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid Algebra.TensorProduct.instCommRing AddMonoidAlgebra.algebra AddCommMonoid.toAddMonoid AddMonoidAlgebra.commSemiring RingHom.toAlgebra Algebra.TensorProduct.instCommSemiring AlgHom.toRingHom AddMonoidAlgebra.semiring Finsupp.instAddMonoid Nat.instAddMonoid Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra universalFactorizationMap Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation universalFactorizationMapPresentation TensorProduct.tmul X AddMonoidAlgebra.zero Finsupp.instZero	—	—
universalFactorizationMapPresentation_σ' 📖	mathematical	—	Algebra.Generators.σ' MvPolynomial CommRing.toCommSemiring TensorProduct AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring instModuleMvPolynomialOfAlgebra Algebra.id AddMonoidAlgebra.commRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid Algebra.TensorProduct.instCommRing AddMonoidAlgebra.algebra AddCommMonoid.toAddMonoid AddMonoidAlgebra.commSemiring RingHom.toAlgebra Algebra.TensorProduct.instCommSemiring AlgHom.toRingHom AddMonoidAlgebra.semiring Finsupp.instAddMonoid Nat.instAddMonoid Algebra.TensorProduct.instSemiring Algebra.TensorProduct.instAlgebra universalFactorizationMap Algebra.Presentation.toGenerators Algebra.PreSubmersivePresentation.toPresentation universalFactorizationMapPresentation DFunLike.coe RingHom AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass RingHom.instFunLike map C AlgEquiv AddMonoidAlgebra.module Algebra.toModule Semiring.toModule Algebra.TensorProduct.leftAlgebra AlgEquiv.instFunLike tensorEquivSum	—	—
universalFactorizationMap_comp_map 📖	mathematical	—	RingHom.comp MvPolynomial CommRing.toCommSemiring TensorProduct AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring instModuleMvPolynomialOfAlgebra Algebra.id AddMonoidAlgebra.nonAssocSemiring Finsupp.instAddZeroClass AddMonoid.toAddZeroClass Nat.instAddMonoid Semiring.toNonAssocSemiring AddMonoidAlgebra.semiring Finsupp.instAddMonoid Algebra.TensorProduct.instSemiring AddMonoidAlgebra.algebra AlgHom.toRingHom Algebra.TensorProduct.instAlgebra universalFactorizationMap map algebraMap NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule Algebra.TensorProduct.leftAlgebra IsScalarTower.to_smulCommClass AddMonoidAlgebra.isScalarTower DistribSMul.toSMulZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Algebra.toSMul IsScalarTower.right AddMonoidAlgebra.smulCommClass IsScalarTower.to_smulCommClass' NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Semiring.toModule Algebra.TensorProduct.lift TensorProduct.isScalarTower_right AddMonoidAlgebra.distribMulAction 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 AddMonoidAlgebra.commRing Finsupp.instAddCommMonoid Nat.instAddCommMonoid AddMonoidAlgebra.commSemiring DFunLike.coe AlgHom AlgHom.funLike	—	ringHom_ext' IsScalarTower.to_smulCommClass AddMonoidAlgebra.isScalarTower IsScalarTower.right AddMonoidAlgebra.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 Polynomial.ext Polynomial.coeff_map one_mul
universalFactorizationMap_freeMonic 📖	mathematical	—	Polynomial.map MvPolynomial CommRing.toCommSemiring TensorProduct AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring instModuleMvPolynomialOfAlgebra Algebra.id AddMonoidAlgebra.semiring Finsupp.instAddMonoid Nat.instAddMonoid Algebra.TensorProduct.instSemiring AddMonoidAlgebra.algebra RingHomClass.toRingHom AlgHom Algebra.TensorProduct.instAlgebra AlgHom.funLike Semiring.toNonAssocSemiring AlgHomClass.toRingHomClass AlgHom.algHomClass universalFactorizationMap Polynomial.freeMonic Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Algebra.toModule Polynomial.instMul AddMonoidAlgebra.commSemiring Finsupp.instAddCommMonoid Nat.instAddCommMonoid 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 AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid freeMonic MvPolynomial.X AddMonoidAlgebra.zero Finsupp.instZero NonUnitalNonAssocSemiring.toMulZeroClass AddMonoidAlgebra.nonUnitalNonAssocSemiring Finsupp.instAdd AddMonoid.toAddZeroClass	—	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 AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid freeMonic WithBot WithBot.natCast	—	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 Ring.toSemiring CommRing.toRing 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	—	—
instFiniteUniversalFactorizationRing 📖	mathematical	—	Module.Finite UniversalFactorizationRing CommSemiring.toSemiring CommRing.toCommSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing instCommRingUniversalFactorizationRing Algebra.toModule instAlgebraUniversalFactorizationRing	—	—
map_map_freeMonic 📖	mathematical	—	map MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid 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 AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid freeMonic	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim Unique.instSubsingleton Monic.leadingCoeff natDegree_freeMonic coeff_freeMonic
natDegree_freeMonic 📖	mathematical	—	natDegree MvPolynomial CommRing.toCommSemiring AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid 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 AddMonoidAlgebra.semiring Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring Finsupp.instAddMonoid Nat.instAddMonoid 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	Ideal Polynomial.UniversalCoprimeFactorizationRing OreLocalization.instSemiring Polynomial.UniversalFactorizationRing Ring.toSemiring CommRing.toRing Polynomial.instCommRingUniversalFactorizationRing Submonoid.powers CommMonoid.toMonoid CommRing.toCommMonoid Algebra.PreSubmersivePresentation.jacobian Polynomial.instAlgebraUniversalFactorizationRing Polynomial.UniversalFactorizationRing.presentation OreLocalization.oreSetComm Ideal.IsPrime Ideal.LiesOver CommRing.toCommSemiring OreLocalization.instAlgebra Function.Bijective Ideal.ResidueField OreLocalization.instCommRing DFunLike.coe AlgHom DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield IsLocalRing.ResidueField.field Localization.AtPrime Ideal.primeCompl CommSemiring.toSemiring CommSemiring.toCommMonoid IsLocalRing.ResidueField.algebra Algebra.id AlgHom.funLike Ideal.ResidueField.mapₐ Algebra.ofId Ideal.over_def Polynomial.MonicDegreeEq.map AlgHom.toRingHom factor₁ algebraMap 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 Ring.toSemiring CommRing.toRing 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 CommSemiring.toSemiring CommRing.toCommSemiring 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 Ring.toSemiring CommRing.toRing 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 Ring.toSemiring CommRing.toRing 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 Ring.toSemiring CommRing.toRing Polynomial.instCommRingUniversalFactorizationRing Submonoid.powers CommMonoid.toMonoid CommRing.toCommMonoid Algebra.PreSubmersivePresentation.jacobian Polynomial.instAlgebraUniversalFactorizationRing Polynomial.UniversalFactorizationRing.presentation OreLocalization.oreSetComm Polynomial.commSemiring OreLocalization.instCommSemiring CommRing.toCommSemiring 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 AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring instModuleMvPolynomialOfAlgebra Algebra.id Polynomial.UniversalFactorizationRing AddMonoidAlgebra.semiring Finsupp.instAddMonoid Nat.instAddMonoid Algebra.TensorProduct.instSemiring AddMonoidAlgebra.algebra 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 AddMonoidAlgebra.addAddCommMonoid Finsupp MulZeroClass.toZero Nat.instMulZeroClass CommSemiring.toSemiring instModuleMvPolynomialOfAlgebra Algebra.id Polynomial.UniversalFactorizationRing AddMonoidAlgebra.semiring Finsupp.instAddMonoid Nat.instAddMonoid Algebra.TensorProduct.instSemiring AddMonoidAlgebra.algebra 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.toPow 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 Unique.instSubsingleton Algebra.to_smulCommClass Algebra.PreSubmersivePresentation.baseChange_jacobian IsScalarTower.right MvPolynomial.universalFactorizationMapPresentation_jacobian map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass AlgHomClass.toRingHomClass 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