Basic

📁 Source: Mathlib/RingTheory/Polynomial/Resultant/Basic.lean

Statistics

Metric	Count
Definitions adjSylvester, disc, discr, resultant, sylvester, sylvesterDeriv, sylvesterMap	7
Theorems adjSylvester_comp_sylveserMap, disc_C, disc_of_degree_eq_one, disc_of_degree_eq_three, disc_of_degree_eq_two, discr_C, discr_of_degree_eq_one, discr_of_degree_eq_three, discr_of_degree_eq_two, exists_mul_add_mul_eq_C_resultant, induction_of_Splits_of_injective_of_surjective, isUnit_resultant_iff_isCoprime, resultant_C_left, resultant_C_mul_left, resultant_C_mul_right, resultant_C_right, resultant_C_zero_left, resultant_C_zero_right, resultant_X_add_C_left, resultant_X_add_C_right, resultant_X_pow_left, resultant_X_pow_right, resultant_X_sub_C_left, resultant_X_sub_C_pow_left, resultant_X_sub_C_pow_right, resultant_X_sub_C_right, resultant_add_left_deg, resultant_add_mul_left, resultant_add_mul_right, resultant_add_right_deg, resultant_comm, resultant_deriv, resultant_dvd_leadingCoeff_pow, resultant_eq_prod_eval, resultant_eq_prod_roots_sub, resultant_eq_zero_iff, resultant_eq_zero_of_lt_lt, resultant_integralNormalization, resultant_map_map, resultant_mul_left, resultant_mul_right, resultant_ne_zero, resultant_one_left, resultant_one_right, resultant_pow_left, resultant_pow_right, resultant_prod_left, resultant_prod_right, resultant_scaleRoots, resultant_self, resultant_self_eq_zero, resultant_succ_left_deg, resultant_taylor, resultant_zero_left, resultant_zero_left_deg, resultant_zero_right, resultant_zero_right_deg, resultant_zero_zero, sylveserMap_comp_adjSylvester, sylvesterDeriv_updateRow, sylvesterMap_apply_coe, sylvester_comm, sylvester_map_map, sylvester_zero_left_deg, toMatrix_sylvesterMap, toMatrix_sylvesterMap'	66
Total	73

Polynomial

Definitions

Name	Category	Theorems
adjSylvester 📖	CompOp	2 math math: adjSylvester_comp_sylveserMap, sylveserMap_comp_adjSylvester
disc 📖	CompOp	—
discr 📖	CompOp	9 math math: disc_of_degree_eq_two, disc_of_degree_eq_three, discr_of_degree_eq_one, discr_C, disc_C, resultant_deriv, disc_of_degree_eq_one, discr_of_degree_eq_two, discr_of_degree_eq_three
resultant 📖	CompOp	51 math math: resultant_X_add_C_right, resultant_one_right, resultant_eq_zero_of_lt_lt, resultant_add_left_deg, resultant_zero_right, resultant_comm, resultant_X_sub_C_right, resultant_X_pow_right, resultant_C_zero_right, resultant_self_eq_zero, UniversalFactorizationRing.jacobian_resentation, resultant_eq_prod_eval, resultant_C_right, resultant_dvd_leadingCoeff_pow, adjSylvester_comp_sylveserMap, isUnit_resultant_iff_isCoprime, resultant_mul_left, resultant_X_sub_C_pow_left, resultant_scaleRoots, resultant_X_sub_C_pow_right, resultant_succ_left_deg, resultant_pow_right, resultant_taylor, resultant_C_left, resultant_add_mul_right, resultant_zero_left, resultant_X_add_C_left, resultant_map_map, resultant_add_right_deg, resultant_eq_prod_roots_sub, resultant_prod_right, resultant_C_zero_left, resultant_deriv, resultant_prod_left, resultant_add_mul_left, resultant_mul_right, resultant_self, resultant_one_left, resultant_X_sub_C_left, resultant_C_mul_left, resultant_pow_left, resultant_X_pow_left, sylveserMap_comp_adjSylvester, resultant_eq_zero_iff, resultant_C_mul_right, resultant_zero_left_deg, resultant_zero_right_deg, resultant_integralNormalization, resultant_zero_zero, exists_mul_add_mul_eq_C_resultant, MvPolynomial.universalFactorizationMapPresentation_jacobian
sylvester 📖	CompOp	7 math math: toMatrix_sylvesterMap', sylvester_comm, sylvester_zero_left_deg, sylvesterDeriv_updateRow, sylvester_map_map, toMatrix_sylvesterMap, MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix
sylvesterDeriv 📖	CompOp	1 math math: sylvesterDeriv_updateRow
sylvesterMap 📖	CompOp	5 math math: toMatrix_sylvesterMap', adjSylvester_comp_sylveserMap, toMatrix_sylvesterMap, sylvesterMap_apply_coe, sylveserMap_comp_adjSylvester

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
adjSylvester_comp_sylveserMap 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	LinearMap.comp Polynomial Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring module Semiring.toModule SetLike.instMembership Submodule.setLike degreeLT Prod.instAddCommMonoid Submodule.addCommMonoid Prod.instModule Submodule.module RingHom.id RingHomCompTriple.ids adjSylvester sylvesterMap LinearMap LinearMap.instSMul Prod.distribSMul AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid AddCommGroup.toAddGroup Submodule.addCommGroup CommRing.toRing Ring.toAddCommGroup ring DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Prod.smulCommClass SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction DistribMulAction.toMulAction AddCommMonoid.toAddMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero DistribSMul.toSMulZeroClass smulCommClass_self CommRing.toCommMonoid CommMonoid.toMonoid Ring.toSemiring resultant LinearMap.id	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype Matrix.adjugate_mul RingHomCompTriple.ids Prod.smulCommClass resultant.eq_1 Matrix.toLin_one toMatrix_sylvesterMap' map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Matrix.toLin_toMatrix Matrix.toLin_mul
disc_C 📖	mathematical	—	discr DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Semiring.toNonAssocSemiring semiring RingHom.instFunLike C AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	discr_C
disc_of_degree_eq_one 📖	mathematical	degree CommSemiring.toSemiring CommRing.toCommSemiring WithBot WithBot.one Nat.instOne	discr AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	discr_of_degree_eq_one
disc_of_degree_eq_three 📖	mathematical	degree CommSemiring.toSemiring CommRing.toCommSemiring WithBot instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	discr Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero coeff AddGroupWithOne.toAddMonoidWithOne	—	discr_of_degree_eq_three
disc_of_degree_eq_two 📖	mathematical	degree CommSemiring.toSemiring CommRing.toCommSemiring WithBot instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	discr SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero coeff Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddGroupWithOne.toAddMonoidWithOne	—	discr_of_degree_eq_two
discr_C 📖	mathematical	—	discr DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Semiring.toNonAssocSemiring semiring RingHom.instFunLike C AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	natDegree_C zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub add_zero Matrix.det_reindex_self Matrix.det.congr_simp Matrix.submatrix_empty Matrix.det_fin_zero MulZeroClass.mul_zero pow_zero mul_one
discr_of_degree_eq_one 📖	mathematical	degree CommSemiring.toSemiring CommRing.toCommSemiring WithBot WithBot.one Nat.instOne	discr AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne CommRing.toRing	—	degree_eq_iff_natDegree_eq_of_pos one_pos Nat.instZeroLEOneClass Nat.cast_one Matrix.ext mul_comm one_mul tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub Nat.instAtLeastTwoHAddOfNat IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instCharZero Matrix.updateRow_self Matrix.cons_val' Matrix.cons_val_fin_one Matrix.det_reindex_self Matrix.det.congr_simp Matrix.det_unique MulZeroClass.mul_zero pow_zero mul_one
discr_of_degree_eq_three 📖	mathematical	degree CommSemiring.toSemiring CommRing.toCommSemiring WithBot instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	discr Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Distrib.toMul Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero coeff AddGroupWithOne.toAddMonoidWithOne	—	Nat.instAtLeastTwoHAddOfNat natDegree_eq_of_degree_eq_some discr.eq_1 Matrix.det_reindex_self Matrix.det.congr_simp one_mul Matrix.det_succ_row_zero Finset.sum_congr Matrix.cons_val' Matrix.cons_val_fin_one Matrix.submatrix_submatrix Matrix.det_fin_three Finset.sum_fin_eq_sum_range Finset.sum_range_succ Finset.sum_singleton IsStrictOrderedRing.toIsOrderedRing Nat.instIsStrictOrderedRing Nat.instNontrivial pow_zero zero_add IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.instZeroLEOneClass Nat.instCharZero pow_one neg_mul Even.neg_pow one_pow MulZeroClass.mul_zero sub_zero MulZeroClass.zero_mul add_zero mul_one sub_self zero_sub mul_neg neg_neg neg_zero Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Meta.NormNum.isNat_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.pow_congr Nat.cast_one Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Meta.NormNum.isInt_pow Mathlib.Meta.NormNum.intPow_negOfNat_bit1 Mathlib.Meta.NormNum.one_natPow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.RingNF.nat_rawCast_1 Mathlib.Tactic.RingNF.mul_assoc_rev Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg Mathlib.Tactic.RingNF.add_assoc_rev Mathlib.Tactic.RingNF.add_neg Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow
discr_of_degree_eq_two 📖	mathematical	degree CommSemiring.toSemiring CommRing.toCommSemiring WithBot instOfNatAtLeastTwo AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Nat.instAtLeastTwoHAddOfNat	discr SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne CommRing.toRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero coeff Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing AddGroupWithOne.toAddMonoidWithOne	—	Nat.instAtLeastTwoHAddOfNat degree_eq_iff_natDegree_eq_of_pos two_pos Nat.instZeroLEOneClass IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Nat.cast_two discr.eq_1 Matrix.det_reindex_self Matrix.ext Fintype.complete Nat.instCharZero Nat.instOrderedSub coeff_derivative mul_comm tsub_self Nat.instCanonicallyOrderedAdd Matrix.updateRow_ne zero_add Matrix.cons_val' Matrix.cons_val_fin_one Matrix.updateRow.congr_simp Nat.cast_zero one_mul one_add_one_eq_two tsub_zero Nat.cast_one Matrix.updateRow_self Matrix.det.congr_simp Matrix.det_fin_three Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.sub_congr Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Mathlib.Meta.NormNum.instAtLeastTwo Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_one Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.cast_zero Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.sub_pf Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_mul Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.isInt_add Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Meta.NormNum.isNat_natDiv Mathlib.Meta.NormNum.isNat_natSub Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.pow_one_cast Mathlib.Tactic.Ring.pow_zero Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.int_rawCast_neg Mathlib.Tactic.RingNF.mul_neg Mathlib.Tactic.RingNF.mul_assoc_rev mul_one add_zero Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.add_pf_add_gt
exists_mul_add_mul_eq_C_resultant 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder degree AddMonoidWithOne.toNatCast WithBot.addMonoidWithOne Nat.instAddMonoidWithOne Polynomial instAdd instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C resultant	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim degree_of_subsingleton Unique.instSubsingleton degree_one Nat.instCanonicallyOrderedAdd IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instNontrivial WithBot.instIsOrderedRing IsStrictOrderedRing.toIsOrderedRing WithBot.nontrivial smulCommClass_self RingHomCompTriple.ids sylveserMap_comp_adjSylvester SMulMemClass.smul_mem Submodule.smulMemClass Algebra.smul_def mul_one Submodule.isScalarTower' isScalarTower IsScalarTower.right Mathlib.Tactic.TermCongr.cHole.congr_simp
induction_of_Splits_of_injective_of_surjective 📖	—	EuclideanDomain.toCommRing Field.toEuclideanDomain	—	—	RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing instIsDomain Field.toIsField SplittingField.splits FaithfulSMul.algebraMap_injective FractionRing.instFaithfulSMul Module.Free.instFaithfulSMulOfNontrivial Module.Free.self IsDomain.toNontrivial MvPolynomial.eval₂_X MvPolynomial.instIsDomainOfIsCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Int.instIsDomain
isUnit_resultant_iff_isCoprime 📖	mathematical	Monic CommSemiring.toSemiring CommRing.toCommSemiring	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero resultant natDegree IsCoprime Polynomial commSemiring	—	natDegree_one resultant_zero_left_deg coeff_one_zero one_pow eq_one_of_monic_natDegree_zero exists_mul_add_mul_eq_C_resultant le_rfl mul_assoc mul_comm Distrib.leftDistribClass NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass IsUnit.val_inv_mul map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass resultant_mul_right eq_or_ne Monic.leadingCoeff resultant_one_right MulZeroClass.zero_mul zero_add resultant_C_right mul_one RingHom.map_one add_comm resultant_add_mul_right LE.le.trans_lt natDegree_mul_le natDegree_add_eq_left_of_natDegree_lt Monic.natDegree_mul' isUnit_iff_exists_inv' instIsDedekindFiniteMonoid
resultant_C_left 📖	mathematical	—	resultant DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne coeff	—	zero_add resultant_add_left_deg natDegree_C mul_comm resultant_zero_left_deg coeff_C_zero
resultant_C_mul_left 📖	mathematical	—	resultant Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	resultant_comm resultant_C_mul_right mul_left_comm mul_assoc mul_comm mul_pow neg_one_mul neg_neg one_pow one_mul
resultant_C_mul_right 📖	mathematical	—	resultant Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instMul DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	Matrix.det.congr_simp Nat.instCanonicallyOrderedAdd pow_zero one_mul Matrix.ext Matrix.updateCol.congr_simp Matrix.updateCol_apply eq_or_ne IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Nat.instZeroLEOneClass coeff_C_mul mul_ite MulZeroClass.mul_zero Nat.instNoMaxOrder pow_succ' mul_assoc Matrix.det_updateCol_smul Matrix.updateCol_eq_self resultant.eq_1 le_rfl
resultant_C_right 📖	mathematical	—	resultant DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero coeff	—	zero_add resultant_add_right_deg natDegree_C resultant_zero_right_deg coeff_C_zero
resultant_C_zero_left 📖	mathematical	—	resultant DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	resultant_zero_left_deg coeff_C_zero
resultant_C_zero_right 📖	mathematical	—	resultant DFunLike.coe RingHom Polynomial CommSemiring.toSemiring CommRing.toCommSemiring Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	resultant_zero_right_deg coeff_C_zero
resultant_X_add_C_left 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	resultant Polynomial instAdd X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C eval NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing	—	resultant_X_sub_C_left map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass sub_neg_eq_add
resultant_X_add_C_right 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	resultant Polynomial instAdd X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne eval	—	resultant_X_sub_C_right map_neg RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass sub_neg_eq_add
resultant_X_pow_left 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	resultant Polynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X coeff	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass sub_zero coeff_zero_eq_eval_zero resultant_X_sub_C_pow_left
resultant_X_pow_right 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	resultant Polynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring X Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne coeff	—	map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass sub_zero coeff_zero_eq_eval_zero resultant_X_sub_C_pow_right
resultant_X_sub_C_left 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	resultant Polynomial instSub CommRing.toRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C eval	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim natDegree_eq_zero resultant_C_right coeff_sub coeff_X_one coeff_C_succ sub_zero one_pow pow_one one_mul eval_C modByMonic_add_div monic_X_sub_C resultant_add_mul_right natDegree_divByMonic natDegree_sub_C natDegree_X natDegree_X_sub_C_le modByMonic_X_sub_C_eq_C_eval
resultant_X_sub_C_pow_left 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	resultant Polynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instSub CommRing.toRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C eval	—	Mathlib.Tactic.Nontriviality.subsingleton_or_nontrivial_elim natDegree_pow' leadingCoeff_X_sub_C one_pow NeZero.one natDegree_sub_C natDegree_X mul_one resultant_X_sub_C_left resultant_pow_left
resultant_X_sub_C_pow_right 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	resultant Polynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring instSub CommRing.toRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike C Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne eval	—	resultant_comm resultant_X_sub_C_pow_left
resultant_X_sub_C_right 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	resultant Polynomial instSub CommRing.toRing X DFunLike.coe RingHom Semiring.toNonAssocSemiring semiring RingHom.instFunLike C Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne eval	—	resultant_comm resultant_X_sub_C_left mul_one
resultant_add_left_deg 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	resultant Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne coeff	—	add_zero MulZeroClass.mul_zero pow_zero mul_one one_mul resultant_succ_left_deg LE.le.trans IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le Nat.instCanonicallyOrderedAdd Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_one_cast
resultant_add_mul_left 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	resultant Polynomial instAdd instMul	—	resultant_comm resultant_add_mul_right mul_assoc pow_add mul_comm Nat.instAtLeastTwoHAddOfNat two_mul pow_mul Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.IsInt.to_isNat Mathlib.Meta.NormNum.isInt_pow Mathlib.Meta.NormNum.intPow_negOfNat_bit0 Mathlib.Meta.NormNum.one_natPow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_pow
resultant_add_mul_right 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	resultant Polynomial instAdd instMul	—	LE.le.trans_lt le_natDegree_of_mem_supp sum_monomial_eq sum_eq_of_subset monomial_zero_right le_rfl MulZeroClass.mul_zero add_zero Finset.sum_range_succ mul_add Distrib.leftDistribClass add_assoc
resultant_add_right_deg 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	resultant Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero coeff	—	resultant_comm resultant_add_left_deg mul_assoc mul_left_comm mul_comm Distrib.leftDistribClass Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_pf_add_gt Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.add_pf_add_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.int_rawCast_neg add_zero Mathlib.Tactic.RingNF.mul_assoc_rev Even.neg_pow one_pow one_mul
resultant_comm 📖	mathematical	—	resultant 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	—	resultant.eq_1 add_comm sylvester_comm Matrix.det_reindex Equiv.Perm.sign_eq_prod_prod_Ioi Finset.prod_congr Units.coe_prod Int.cast_prod Int.cast_one Int.cast_neg Equiv.prod_comp Finset.prod_map_equiv Equiv.symm_apply_apply Finset.prod_ite_mem_eq Fintype.prod_sum_type IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono AddLeftCancelSemigroup.toIsLeftCancelAdd IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid contravariant_lt_of_covariant_le Finset.prod_const_one LT.lt.trans_le IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT Nat.instCanonicallyOrderedAdd LE.le.trans LT.lt.le Finset.prod_const Fintype.card_fin one_mul mul_one pow_mul
resultant_deriv 📖	mathematical	WithBot Preorder.toLT WithBot.instPreorder Nat.instPreorder WithBot.zero MulZeroClass.toZero Nat.instMulZeroClass degree CommSemiring.toSemiring CommRing.toCommSemiring	resultant DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike derivative natDegree Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne leadingCoeff discr	—	resultant_comm resultant.eq_1 natDegree_pos_iff_degree_pos sylvesterDeriv_updateRow Matrix.det_updateRow_smul Matrix.updateRow_eq_self discr.eq_1 mul_comm Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.int_rawCast_neg add_zero mul_one Mathlib.Tactic.RingNF.mul_assoc_rev Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Nat.two_dvd_mul_add_one
resultant_dvd_leadingCoeff_pow 📖	mathematical	IsCoprime Polynomial CommSemiring.toSemiring CommRing.toCommSemiring commSemiring	semigroupDvd SemigroupWithZero.toSemigroup NonUnitalSemiring.toSemigroupWithZero NonUnitalCommSemiring.toNonUnitalSemiring NonUnitalCommRing.toNonUnitalCommSemiring CommRing.toNonUnitalCommRing resultant natDegree Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero leadingCoeff	—	eq_or_ne resultant_zero_left_deg IsDomain.to_noZeroDivisors natDegree_C pow_zero resultant_zero_right_deg leadingCoeff_C isUnit_iff IsUnit.of_mul_eq_one_right instIsDedekindFiniteMonoid MulZeroClass.zero_mul zero_add coeff_C_zero IsUnit.pow add_zero resultant_mul_right le_rfl resultant_one_right mul_comm add_comm resultant_add_mul_right natDegree_add_eq_left_of_natDegree_lt natDegree_mul natDegree_one
resultant_eq_prod_eval 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring Splits	resultant Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero leadingCoeff Multiset.prod CommRing.toCommMonoid Multiset.map eval roots	—	resultant_zero_left_deg Multiset.map_congr roots.congr_simp roots_zero mul_one Monic.leadingCoeff one_pow one_mul Monic.natDegree_eq_zero natDegree_one coeff_one_zero roots_one eval_zero resultant_zero_right zero_pow MulZeroClass.zero_mul Multiset.map_const' Splits.natDegree_eq_card_roots Multiset.prod_replicate RingHom.injective DivisionRing.isSimpleRing IsLocalRing.toNontrivial Field.instIsLocalRing instIsDomain resultant_eq_prod_roots_sub Monic.map Splits.map SplittingField.splits resultant_map_map resultant_add_right_deg natDegree_map coeff_map coeff_natDegree map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_sub_sprod_roots_eq_prod_map_eval Splits.roots_map map_multiset_prod Multiset.map_map eval_map_algebraMap aeval_algebraMap_apply natDegree_C_mul IsDomain.to_noZeroDivisors instNoZeroDivisors nontrivial Monic.eq_1 coeff_C_mul inv_mul_cancel₀ eval_mul eval_C Multiset.prod_map_mul inv_pow mul_inv_cancel_left₀ isReduced_of_noZeroDivisors inv_mul_eq_iff_eq_mul₀ resultant_C_mul_right Splits.mul Splits.C resultant_C_mul_left roots_C_mul FaithfulSMul.algebraMap_injective FractionRing.instFaithfulSMul Module.Free.instFaithfulSMulOfNontrivial Module.Free.self IsDomain.toNontrivial LE.le.trans natDegree_map_le Field.toIsField map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_pow OreLocalization.instIsScalarTower IsScalarTower.right natDegree_map_eq_of_injective leadingCoeff_map_of_injective
resultant_eq_prod_roots_sub 📖	mathematical	Monic DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield Splits	resultant EuclideanDomain.toCommRing Field.toEuclideanDomain natDegree CommSemiring.toSemiring CommRing.toCommSemiring Multiset.prod CommRing.toCommMonoid Multiset.map SubNegMonoid.toSub AddGroup.toSubNegMonoid AddGroupWithOne.toAddGroup Ring.toAddGroupWithOne DivisionRing.toRing Field.toDivisionRing SProd.sprod Multiset Multiset.instSProd roots instIsDomain	—	instIsDomain Nat.strong_induction_on instNoZeroDivisors IsDomain.to_noZeroDivisors Monic.ne_zero IsLocalRing.toNontrivial Field.instIsLocalRing resultant_add_mul_left natDegree_mul natDegree_neg add_comm le_refl le_rfl mul_neg add_neg_cancel resultant_zero_left natDegree_one pow_zero coeff_one_zero one_mul one_pow mul_one Multiset.map_congr roots.congr_simp roots_one Multiset.product_zero Monic.natDegree_eq_zero zero_pow not_forall_not Multiset.eq_zero_iff_forall_notMem Multiset.card_eq_zero Splits.natDegree_eq_card_roots Multiset.prod_eq_zero Multiset.mem_product eval_mul MulZeroClass.zero_mul sub_self natDegree_C_mul natDegree_modByMonic_lt Monic.eq_1 leadingCoeff.eq_1 coeff_C_mul inv_mul_cancel₀ natDegree_map DivisionRing.isSimpleRing Monic.map Splits.map SplittingField.splits map_mul map_C map_inv₀ RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass LT.lt.le modByMonic_add_div natDegree_divByMonic LE.le.trans resultant_add_left_deg resultant_comm RingHom.injective map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass inv_mul_eq_iff_eq_mul₀ map_pow MonoidWithZeroHomClass.toMonoidHomClass isReduced_of_noZeroDivisors inv_pow resultant_C_mul_right resultant_map_map map_sub_roots_sprod_eq_prod_map_eval map_sub_sprod_roots_eq_prod_map_eval Splits.roots_map eval_C mul_inv_cancel_left₀ eval_add add_zero Multiset.prod_map_mul Multiset.map_const' Multiset.prod_replicate map_neg RingHomClass.toAddMonoidHomClass map_one MonoidHomClass.toOneHomClass Monic.leadingCoeff eval_map_algebraMap Multiset.map_map map_multiset_prod mul_comm Distrib.rightDistribClass aeval_algebraMap_apply le_of_not_ge Multiset.map_swap_product Multiset.card_product neg_mul neg_sub
resultant_eq_zero_iff 📖	mathematical	—	resultant EuclideanDomain.toCommRing Field.toEuclideanDomain natDegree CommSemiring.toSemiring CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing IsCoprime Polynomial DivisionSemiring.toSemiring Semifield.toDivisionSemiring Field.toSemifield commSemiring Semifield.toCommSemiring	—	eq_or_ne resultant_zero_right_deg pow_zero NeZero.one IsLocalRing.toNontrivial Field.instIsLocalRing resultant_zero_left_deg isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors instIsDomain nontrivial RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass Monic.eq_1 coeff_natDegree natDegree_C_mul coeff_C_mul inv_mul_cancel₀ isUnit_resultant_iff_isCoprime isCoprime_mul_unit_left_left isUnit_C IsUnit.mul_iff instIsDedekindFiniteMonoid resultant_C_mul_left inv_pow
resultant_eq_zero_of_lt_lt 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	resultant MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	resultant_add_left_deg resultant_add_right_deg mul_one coeff_eq_zero_of_natDegree_lt pow_one MulZeroClass.mul_zero MulZeroClass.zero_mul
resultant_integralNormalization 📖	mathematical	—	resultant scaleRoots CommSemiring.toSemiring CommRing.toCommSemiring leadingCoeff integralNormalization natDegree Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	natDegree_scaleRoots natDegree_integralNormalization resultant_zero_right_deg integralNormalization_zero zero_tsub Nat.instCanonicallyOrderedAdd Nat.instOrderedSub MulZeroClass.mul_zero pow_zero one_mul mul_right_injective₀ IsCancelMulZero.toIsLeftCancelMulZero IsDomain.toIsCancelMulZero isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors IsDomain.toNontrivial resultant_scaleRoots resultant_C_mul_right mul_comm integralNormalization_mul_C_leadingCoeff mul_assoc pow_add add_comm resultant_zero_left_deg zero_scaleRoots MulZeroClass.zero_mul MvPolynomial.eval₂_X mem_lifts_and_degree_eq map_surjective natDegree_eq_natDegree coeff_map map_scaleRoots integralNormalization_map resultant_map_map MvPolynomial.instIsDomainOfIsCancelAdd IsOrderedCancelAddMonoid.toIsCancelAdd IsStrictOrderedRing.toIsOrderedCancelAddMonoid Int.instIsStrictOrderedRing Int.instIsDomain map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass
resultant_map_map 📖	mathematical	—	resultant map CommSemiring.toSemiring CommRing.toCommSemiring DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike	—	Matrix.det.congr_simp sylvester_map_map RingHom.map_det
resultant_mul_left 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	resultant Polynomial instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	resultant_comm resultant_mul_right Nat.instAtLeastTwoHAddOfNat Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.mul_pp_pf_overlap Mathlib.Tactic.Ring.add_overlap_pf Mathlib.Meta.NormNum.IsNat.to_raw_eq Mathlib.Meta.NormNum.isNat_add Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one Mathlib.Tactic.RingNF.int_rawCast_neg add_zero Mathlib.Tactic.RingNF.mul_assoc_rev mul_one Even.neg_pow Distrib.leftDistribClass one_pow
resultant_mul_right 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	resultant Polynomial instMul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	induction_of_Splits_of_injective_of_surjective instIsDomain resultant_eq_prod_eval Multiset.map_congr eval_mul Multiset.prod_map_mul Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.add_congr Mathlib.Tactic.Ring.add_pf_add_lt Mathlib.Tactic.Ring.add_pf_zero_add Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul Mathlib.Tactic.RingNF.nat_rawCast_1 pow_one mul_one Mathlib.Tactic.RingNF.mul_assoc_rev add_zero natDegree_map_eq_of_injective resultant_map_map NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass map_mul mem_lifts_and_degree_eq map_surjective natDegree_eq_natDegree map_mul le_iff_exists_add Nat.instCanonicallyOrderedAdd resultant_add_left_deg coeff_mul_degree_add_degree Mathlib.Tactic.Ring.neg_congr Mathlib.Tactic.Ring.cast_pos Mathlib.Meta.NormNum.isNat_ofNat Nat.cast_one Mathlib.Tactic.Ring.neg_add Mathlib.Tactic.Ring.neg_one_mul Mathlib.Meta.NormNum.IsInt.to_raw_eq Mathlib.Meta.NormNum.isInt_mul Mathlib.Meta.NormNum.IsInt.of_raw Mathlib.Meta.NormNum.IsNat.to_isInt Mathlib.Meta.NormNum.IsNat.of_raw Mathlib.Tactic.Ring.neg_zero Mathlib.Tactic.Ring.pow_prod_atom Mathlib.Tactic.RingNF.int_rawCast_neg
resultant_ne_zero 📖	—	IsCoprime Polynomial CommSemiring.toSemiring CommRing.toCommSemiring commSemiring	—	—	eq_or_ne resultant_zero_left_deg isReduced_of_noZeroDivisors IsDomain.to_noZeroDivisors IsDomain.toNontrivial natDegree_C resultant_dvd_leadingCoeff_pow
resultant_one_left 📖	mathematical	—	resultant Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne coeff	—	one_pow mul_one resultant_C_left
resultant_one_right 📖	mathematical	—	resultant Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instOne Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero coeff	—	one_pow mul_one resultant_C_right
resultant_pow_left 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	resultant Polynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	Finset.prod_const Finset.card_range resultant_prod_left Finset.prod_congr
resultant_pow_right 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	resultant Polynomial Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero semiring	—	Finset.prod_const Finset.card_range resultant_prod_right Finset.prod_congr
resultant_prod_left 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	resultant Finset.prod Polynomial CommRing.toCommMonoid commRing	—	Finset.induction natDegree_one resultant_zero_left_deg coeff_one_zero one_pow MulZeroClass.mul_zero Finset.prod_insert natDegree_mul' leadingCoeff_prod' resultant_mul_left
resultant_prod_right 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	resultant Finset.prod Polynomial CommRing.toCommMonoid commRing	—	resultant_comm Finset.prod_congr resultant_prod_left Finset.prod_mul_distrib Finset.prod_pow_eq_pow_sum Finset.mul_sum natDegree_prod'
resultant_scaleRoots 📖	mathematical	—	resultant scaleRoots CommSemiring.toSemiring CommRing.toCommSemiring natDegree Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	natDegree_scaleRoots eq_or_ne resultant_zero_left_deg zero_scaleRoots MulZeroClass.zero_mul pow_zero one_mul resultant_zero_right_deg MulZeroClass.mul_zero induction_of_Splits_of_injective_of_surjective natDegree_eq_zero natDegree_C scaleRoots_C coeff_C_zero scaleRoots_zero Algebra.smul_def resultant_C_mul_right resultant_X_pow_right natDegree_mul_X_pow IsLocalRing.toNontrivial Field.instIsLocalRing nontrivial RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass zero_add mul_coeff_zero coeff_X_pow zero_pow IsStrictOrderedRing.noZeroDivisors Nat.instIsStrictOrderedRing CanonicallyOrderedAdd.toExistsAddOfLE Nat.instCanonicallyOrderedAdd instIsDomain resultant_eq_prod_eval le_rfl Splits.scaleRoots roots_scaleRoots isUnit_iff_ne_zero Multiset.map_map Multiset.map_congr scaleRoots_eval_mul leadingCoeff_scaleRoots Multiset.prod_map_mul Multiset.map_const' Splits.natDegree_eq_card_roots Multiset.prod_replicate Mathlib.Tactic.Ring.of_eq Mathlib.Tactic.Ring.mul_congr Mathlib.Tactic.Ring.pow_congr Mathlib.Tactic.Ring.atom_pf Mathlib.Tactic.Ring.pow_add Mathlib.Tactic.Ring.single_pow Mathlib.Tactic.Ring.mul_pow Mathlib.Tactic.Ring.mul_pf_right Mathlib.Tactic.Ring.one_mul Mathlib.Tactic.Ring.one_pow Mathlib.Tactic.Ring.pow_zero Mathlib.Tactic.Ring.add_mul Mathlib.Tactic.Ring.mul_add Mathlib.Tactic.Ring.mul_pf_left Mathlib.Tactic.Ring.mul_zero Mathlib.Tactic.Ring.add_pf_add_zero Mathlib.Tactic.Ring.zero_mul map_zero map_injective map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass map_pow MonoidWithZeroHomClass.toMonoidHomClass natDegree_map_eq_of_injective resultant_map_map map_scaleRoots map_eq_zero_iff MonoidWithZeroHomClass.toZeroHomClass mem_lifts_and_degree_eq map_surjective natDegree_eq_natDegree coeff_map
resultant_self 📖	mathematical	—	resultant natDegree CommSemiring.toSemiring CommRing.toCommSemiring Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	induction_of_Splits_of_injective_of_surjective natDegree_eq_zero natDegree_C resultant_zero_right_deg coeff_C_zero pow_zero instIsDomain resultant_eq_prod_eval le_rfl zero_pow IsDomain.to_noZeroDivisors isReduced_of_noZeroDivisors IsLocalRing.toNontrivial Field.instIsLocalRing Splits.exists_eval_eq_zero degree_ne_of_natDegree_ne eq_or_ne map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass map_zero MonoidWithZeroHomClass.toZeroHomClass natDegree_map_eq_of_injective resultant_map_map mem_lifts_and_degree_eq map_surjective natDegree_eq_natDegree
resultant_self_eq_zero 📖	mathematical	—	resultant natDegree CommSemiring.toSemiring CommRing.toCommSemiring MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	resultant_self zero_pow
resultant_succ_left_deg 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	resultant Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Ring.toAddCommGroup CommRing.toRing AddMonoidWithOne.toOne AddGroupWithOne.toAddMonoidWithOne Ring.toAddGroupWithOne coeff	—	resultant_zero_right_deg pow_succ' pow_zero one_mul resultant.eq_1 Matrix.det_succ_row Finset.sum_eq_single coeff_eq_zero_of_natDegree_lt MulZeroClass.mul_zero Matrix.det.congr_simp Fin.succAbove_last MulZeroClass.zero_mul instIsEmptyFalse Matrix.det_reindex_self Matrix.submatrix_submatrix pow_add Even.neg_pow Distrib.rightDistribClass Nat.instAtLeastTwoHAddOfNat one_pow pow_one mul_neg mul_one add_assoc add_comm add_tsub_cancel_left Nat.instOrderedSub IsLeftCancelAdd.addLeftReflectLE_of_addLeftReflectLT AddLeftCancelSemigroup.toIsLeftCancelAdd contravariant_lt_of_covariant_le IsOrderedAddMonoid.toAddLeftMono Nat.instIsOrderedAddMonoid Matrix.ext IsLeftCancelAdd.addLeftStrictMono_of_addLeftMono Nat.instCanonicallyOrderedAdd add_right_comm ite_and
resultant_taylor 📖	mathematical	—	resultant DFunLike.coe LinearMap CommSemiring.toSemiring CommRing.toCommSemiring RingHom.id Semiring.toNonAssocSemiring Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule LinearMap.instFunLike taylor natDegree	—	induction_of_Splits_of_injective_of_surjective Submonoid.closure_induction taylor_C natDegree_C natDegree_taylor resultant_zero_left_deg coeff_C_zero map_add SemilinearMapClass.toAddHomClass LinearMap.semilinearMapClass taylor_X add_assoc AddMonoidHomClass.toAddHomClass RingHomClass.toAddMonoidHomClass RingHom.instRingHomClass natDegree_add_C natDegree_X IsLocalRing.toNontrivial Field.instIsLocalRing resultant_X_add_C_left neg_add_rev taylor_eval neg_add_cancel_right taylor_one map_one MonoidHomClass.toOneHomClass MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass natDegree_one coeff_one_zero one_pow MulZeroClass.zero_mul map_zero AddMonoidHomClass.toZeroHomClass DistribMulActionSemiHomClass.toAddMonoidHomClass SemilinearMapClass.distribMulActionSemiHomClass MulZeroClass.mul_zero taylor_mul natDegree_mul' leadingCoeff_taylor IsDomain.to_noZeroDivisors instIsDomain resultant_mul_left le_rfl map_taylor natDegree_map_eq_of_injective resultant_map_map mem_lifts_and_degree_eq map_surjective natDegree_eq_natDegree coeff_map
resultant_zero_left 📖	mathematical	—	resultant Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass coeff	—	resultant_comm resultant_zero_right MulZeroClass.mul_zero pow_zero one_mul zero_pow MulZeroClass.zero_mul
resultant_zero_left_deg 📖	mathematical	—	resultant Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring coeff	—	Matrix.det.congr_simp sylvester_zero_left_deg Matrix.det_diagonal Finset.prod_const Fintype.card_congr' zero_add Fintype.card_fin
resultant_zero_right 📖	mathematical	—	resultant Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instZero Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass coeff	—	resultant_zero_left_deg pow_zero one_mul zero_pow MulZeroClass.zero_mul Matrix.det_eq_zero_of_column_eq_zero Nat.instCanonicallyOrderedAdd Nat.instNoMaxOrder
resultant_zero_right_deg 📖	mathematical	—	resultant Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring CommRing.toCommSemiring coeff	—	resultant_comm MulZeroClass.mul_zero pow_zero resultant_zero_left_deg one_mul
resultant_zero_zero 📖	mathematical	—	resultant Polynomial CommSemiring.toSemiring CommRing.toCommSemiring instZero Monoid.toNatPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing NonUnitalCommRing.toNonUnitalNonAssocCommRing CommRing.toNonUnitalCommRing	—	resultant_zero_right pow_add
sylveserMap_comp_adjSylvester 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	LinearMap.comp Polynomial Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring module Semiring.toModule SetLike.instMembership Submodule.setLike degreeLT Submodule.addCommMonoid Prod.instAddCommMonoid Submodule.module Prod.instModule RingHom.id RingHomCompTriple.ids sylvesterMap adjSylvester LinearMap LinearMap.instSMul DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero AddCommMonoid.toAddMonoid Module.toDistribMulAction smulCommClass_self CommRing.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid Ring.toSemiring CommRing.toRing resultant LinearMap.id	—	RingHomInvPair.ids smulCommClass_self Finite.of_fintype Matrix.mul_adjugate RingHomCompTriple.ids resultant.eq_1 Matrix.toLin_one toMatrix_sylvesterMap' map_smul SemilinearMapClass.toMulActionSemiHomClass SemilinearEquivClass.instSemilinearMapClass LinearEquiv.instSemilinearEquivClass Matrix.toLin_toMatrix Matrix.toLin_mul
sylvesterDeriv_updateRow 📖	mathematical	natDegree	Matrix.updateRow sylvesterDeriv Function.hasSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass NonUnitalNonAssocSemiring.toDistribSMul NonAssocSemiring.toNonUnitalNonAssocSemiring leadingCoeff sylvester DFunLike.coe LinearMap RingHom.id Polynomial NonUnitalNonAssocSemiring.toAddCommMonoid semiring module Semiring.toModule LinearMap.instFunLike derivative	—	Matrix.ext sylvesterDeriv.eq_1 ne_or_eq Matrix.updateRow_ne Matrix.updateRow.congr_simp coeff_derivative Matrix.updateRow_self Matrix.updateRow_apply mul_ite mul_one MulZeroClass.mul_zero Nat.instOrderedSub Nat.cast_one Nat.cast_add Mathlib.Meta.NormNum.IsNat.to_eq Mathlib.Meta.NormNum.isNat_natSub Mathlib.Meta.NormNum.isNat_mul Mathlib.Meta.NormNum.isNat_ofNat tsub_zero zero_tsub Nat.instCanonicallyOrderedAdd zero_add
sylvesterMap_apply_coe 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	Polynomial Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring semiring module Semiring.toModule SetLike.instMembership Submodule.setLike degreeLT DFunLike.coe LinearMap RingHom.id Prod.instAddCommMonoid Submodule.addCommMonoid Prod.instModule Submodule.module LinearMap.instFunLike sylvesterMap instAdd instMul	—	—
sylvester_comm 📖	mathematical	—	sylvester DFunLike.coe Equiv Matrix AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma Nat.instAddCommSemigroup EquivLike.toFunLike Equiv.instEquivLike Matrix.reindex finCongr add_comm Equiv.trans Equiv.symm finSumFinEquiv Equiv.sumComm	—	Matrix.ext add_comm finSumFinEquiv_symm_apply_castAdd finSumFinEquiv_symm_apply_natAdd
sylvester_map_map 📖	mathematical	—	sylvester map DFunLike.coe RingHom Matrix Matrix.nonAssocSemiring Semiring.toNonAssocSemiring Fin.fintype RingHom.instFunLike RingHom.mapMatrix	—	Matrix.ext coeff_map map_zero MonoidWithZeroHomClass.toZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
sylvester_zero_left_deg 📖	mathematical	—	sylvester Matrix.diagonal MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring coeff	—	Matrix.ext sylvester.eq_1 Matrix.of_apply Matrix.diagonal_apply tsub_self Nat.instCanonicallyOrderedAdd Nat.instOrderedSub add_zero Set.Icc_self
toMatrix_sylvesterMap 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Polynomial Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule SetLike.instMembership Submodule.setLike degreeLT Prod.instAddCommMonoid Submodule.addCommMonoid Prod.instModule Submodule.module Matrix LinearMap.addCommMonoid Matrix.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix instFintypeSum Fin.fintype Finite.of_fintype Module.Basis.prod degreeLT.basis sylvesterMap Equiv Equiv.instEquivLike Matrix.reindex Equiv.refl Equiv.symm finSumFinEquiv sylvester	—	Matrix.ext RingHomInvPair.ids smulCommClass_self Finite.of_fintype ite_and coeff_eq_zero_of_natDegree_lt LinearMap.toMatrix_apply Module.Basis.prod_apply MulZeroClass.mul_zero degreeLT.basis_val zero_add coeff_mul_X_pow' add_zero
toMatrix_sylvesterMap' 📖	mathematical	natDegree CommSemiring.toSemiring CommRing.toCommSemiring	DFunLike.coe LinearEquiv RingHom.id Semiring.toNonAssocSemiring RingHomInvPair.ids LinearMap Polynomial Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring semiring module Semiring.toModule SetLike.instMembership Submodule.setLike degreeLT Prod.instAddCommMonoid Submodule.addCommMonoid Prod.instModule Submodule.module Matrix LinearMap.addCommMonoid Matrix.addCommMonoid LinearMap.module smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Matrix.module EquivLike.toFunLike DFinsupp.instEquivLikeLinearEquiv LinearMap.toMatrix Fin.fintype Finite.of_fintype Module.Basis.reindex Module.Basis.prod degreeLT.basis finSumFinEquiv sylvesterMap sylvester	—	Matrix.ext RingHomInvPair.ids smulCommClass_self Finite.of_fintype Equiv.surjective LinearMap.toMatrix_apply Module.Basis.coe_reindex Equiv.symm_apply_apply Module.Basis.prod_apply coeff_add toMatrix_sylvesterMap

---

← Back to Index