Finsupp

📁 Source: Mathlib/SetTheory/Cardinal/Finsupp.lean

Statistics

Metric	Count
Definitions Finsupp	1
Theorems mk_finsupp_lift_of_fintype, mk_finsupp_lift_of_infinite, mk_finsupp_lift_of_infinite', mk_finsupp_nat, mk_finsupp_of_fintype, mk_finsupp_of_infinite, mk_finsupp_of_infinite', mk_multiset_of_countable, mk_multiset_of_infinite, mk_multiset_of_isEmpty, mk_multiset_of_nonempty	11
Total	12

Cardinal

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
mk_finsupp_lift_of_fintype 📖	mathematical	—	Finsupp Cardinal Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring commSemiring lift Fintype.card	—	mk_pi prod_const mk_fintype lift_natCast Equiv.cardinal_eq Finite.of_fintype
mk_finsupp_lift_of_infinite 📖	mathematical	—	Finsupp Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot lift	—	le_antisymm mk_le_of_injective Finsupp.graph_injective mk_finset_of_infinite Prod.infinite_of_left Nontrivial.to_nonempty mk_prod mul_eq_max_of_aleph0_le_left max_le lift_id lift_umax exists_ne lift_mk_le Finsupp.single_left_injective Infinite.instNontrivial Finsupp.single_injective
mk_finsupp_lift_of_infinite' 📖	mathematical	—	Finsupp Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot lift	—	mk_finsupp_lift_of_fintype aleph0_le_lift max_eq_right le_trans lift_le_aleph0 LT.lt.le lt_aleph0_of_finite Finite.of_fintype power_nat_eq Fintype.card_pos mk_finsupp_lift_of_infinite Infinite.instNontrivial
mk_finsupp_nat 📖	mathematical	—	Finsupp MulZeroClass.toZero Nat.instMulZeroClass Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot aleph0	—	mk_finsupp_lift_of_infinite' instInfiniteNat lift_uzero mk_eq_aleph0 instCountableNat lift_aleph0
mk_finsupp_of_fintype 📖	mathematical	—	Finsupp Cardinal Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring commSemiring Fintype.card	—	mk_finsupp_lift_of_fintype lift_id
mk_finsupp_of_infinite 📖	mathematical	—	Finsupp Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	mk_finsupp_lift_of_infinite lift_id
mk_finsupp_of_infinite' 📖	mathematical	—	Finsupp Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot	—	mk_finsupp_lift_of_infinite' lift_id
mk_multiset_of_countable 📖	mathematical	—	aleph0	—	mk_eq_aleph0
mk_multiset_of_infinite 📖	mathematical	—	Multiset	—	mk_multiset_of_nonempty Nontrivial.to_nonempty Infinite.instNontrivial sup_of_le_left
mk_multiset_of_isEmpty 📖	mathematical	—	Multiset Cardinal instOne	—	Equiv.cardinal_eq IsEmpty.instSubsingleton mk_fintype Fintype.card_unique Nat.cast_one
mk_multiset_of_nonempty 📖	mathematical	—	Multiset Cardinal SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice ConditionallyCompleteLinearOrder.toConditionallyCompleteLattice ConditionallyCompleteLinearOrderBot.toConditionallyCompleteLinearOrder instConditionallyCompleteLinearOrderBot aleph0	—	Equiv.cardinal_eq mk_finsupp_nat

(root)

Definitions

Name	Category	Theorems
Finsupp 📖	CompData	3886 math math: MvPolynomial.is_id, Finsupp.coe_neg, Finsupp.instSMulPosReflectLE, Finsupp.image_prodMap_embDomain_antidiagonal, MvPolynomial.pUnitAlgEquiv_symm_monomial, MvPowerSeries.coeff_zero_eq_constantCoeff_apply, MvPolynomial.funext_iff, MvPolynomial.eval_indicator_apply_eq_one, TensorProduct.finsuppRight_apply, Height.logHeight_eval_ge, AddMonoidAlgebra.modOf_apply_add_self, Finsupp.prod_eq_single, MvPolynomial.join₁_rename, Finsupp.range_mapRange, MvPolynomial.vanishingIdeal_anti_mono, SkewMonoidAlgebra.ofFinsupp_eq_zero, MvPolynomial.eval₂_mul_eq_zero_of_left, AlgebraicGeometry.AffineSpace.map_Spec_map, Finsupp.snd_sumFinsuppLEquivProdFinsupp, MvPolynomial.aeval_sum, Finsupp.sum_toMultiset, MvPolynomial.dvd_monomial_one_iff_exists, Finsupp.range_subset_insert_frange, WittVector.bind₁_frobeniusPoly_wittPolynomial, LinearMap.exists_finsupp_nat_of_fin_fun_injective, Finsupp.fst_sumFinsuppLEquivProdFinsupp, MonomialOrder.le_degree_of_mem_support, Finsupp.instCanonicallyOrderedAddOfAddLeftMono, Finsupp.finite_of_degree_le, groupHomology.π_comp_H2Iso_hom_assoc, MonoidAlgebra.ofCoeff_injective, Finsupp.toDFinsupp_add, KaehlerDifferential.mvPolynomialBasis_apply, Finsupp.mulHom_ext'_iff, AddMonoidAlgebra.supportedEquivFinsupp_apply_apply, Finsupp.support_finset_sum, MvPowerSeries.WithPiTopology.tendsto_trunc_atTop, Finsupp.linearCombination_apply_of_mem_supported, AddMonoidAlgebra.mul_single_apply, MvPolynomial.coeff_neg, MvPolynomial.support_sum, Module.Presentation.cokernelRelations_relation, MonomialOrder.sPolynomial_leadingTerm_mul', MvPolynomial.degrees_neg, MvPolynomial.coe_C, Algebra.PreSubmersivePresentation.jacobiMatrix_naive, MvPolynomial.isJacobsonRing, Module.Free.finsupp, Finsupp.mapRange_apply, Finsupp.coe_sumElim, MvPowerSeries.coeff_zero_eq_constantCoeff, MvPolynomial.support_mul, Finsupp.mapDomain_tendstoCofinite, MvPolynomial.algHom_ext_iff, MonomialOrder.span_leadingTerm_sdiff_singleton_zero, AddMonoidAlgebra.mapDomainRingEquiv_apply, MvPolynomial.map_bind₁, HahnSeries.instNoZeroDivisorsFinsuppNat, Finsupp.comapDomain_add, MvPolynomial.vars_sum_of_disjoint, groupHomology.mapCycles₂_comp_assoc, Orthonormal.inner_left_finsupp, MvPolynomial.totalDegree_monomial, Algebra.Generators.aeval_val_surjective, AlgebraicGeometry.AffineSpace.map_toSpecMvPoly_assoc, IsSMulRegular.finsupp, Finsupp.mapRange.linearEquiv_refl, Module.Basis.mem_submodule_iff, Finsupp.zero_update, MvPolynomial.mul_X_divMonomial, CommRingCat.HomTopology.mvPolynomialHomeomorph_apply_snd, Finsupp.Colex.addLeftStrictMono, Ordinal.CNF.coeff_injective, MvPolynomial.radical_le_vanishingIdeal_zeroLocus, Module.Relations.Solution.ofπ'_var, Finsupp.degree_eq_sum, Module.Basis.end_repr_apply, AddMonoidAlgebra.mul_apply, Algebra.Presentation.differentials.comm₁₂_single, wittPolynomial_zmod_self, Nat.coe_properDivisors_eq_prod_pow_lt_factorization, MvPolynomial.aeval_X_left, Finsupp.embDomain_apply, Nat.Prime.exists_orderOf_eq_pow_factorization_exponent, Finsupp.instPosSMulReflectLE, MvPolynomial.map_mapRange_eq_iff, MvPowerSeries.weightedOrder_monomial, MvPolynomial.map_comp_C, MvPolynomial.DirectSum.coeLinearMap_eq_dfinsuppSum, Finsupp.embDomain_some_some, MvPolynomial.coeffs_add, MvPowerSeries.eq_iff_frequently_trunc'_eq, MvPolynomial.pUnitAlgEquiv_apply, Finsupp.single_injective, sigmaFinsuppEquivDFinsupp_support, Nat.Primes.prodNatEquiv_symm_apply, Nat.multiplicity_eq_factorization, Finsupp.neLocus_neg, MvPolynomial.eval₂Hom_X, Nat.factorization_eq_zero_of_not_dvd, MvPolynomial.toMvPowerSeries_uniformContinuous, MvPolynomial.exists_finset_rename, MonomialOrder.monic_X_sub_C, MvPolynomial.hom_C, Finsupp.mem_supported_support, IsPrimePow.exists_ordCompl_eq_one, AlgebraicIndependent.of_aeval, MvPolynomial.weightedHomogeneousComponent_of_isWeightedHomogeneous_same, AddMonoidAlgebra.coeffEquiv_symm_apply, MvPowerSeries.truncFinset_one, List.toFinsupp_eq_sum_mapIdx_single, Polynomial.homogenize_map, MvPowerSeries.trunc'_trunc', MvPolynomial.support_finSuccEquiv, Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, MvPolynomial.rTensor_apply_tmul_apply, MvPolynomial.degrees_monomial, Submonoid.exists_finsupp_of_mem_closure_range, Nat.Prime.factorization_pos_of_dvd, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv, MvPolynomial.zero_divMonomial, Finsupp.mapDomain.addMonoidHom_comp, Ideal.mem_span_iff_exists_isHomogeneous, Finsupp.sumElim_inr, MvPolynomial.coeff_divMonomial, SkewMonoidAlgebra.toFinsupp_apply, Finsupp.sub_apply, WittVector.aeval_verschiebung_poly', SkewMonoidAlgebra.ofFinsupp_zero, groupHomology.d₁₀_single_one, MonomialOrder.degree_add_of_ne, Submodule.mem_ideal_smul_span_iff_exists_sum, MvPolynomial.sum_def, Finsupp.floorDiv_def, MvPolynomial.rTensorAlgEquiv_apply, MvPolynomial.one_def, Algebra.Generators.H1Cotangent.δAux_mul, MvPowerSeries.coeff_mul_monomial, Algebra.Presentation.naive_toGenerators, Finsupp.restrictDom_apply, groupHomology.boundaries₂_le_cycles₂, SkewMonoidAlgebra.ofFinsupp_smul, Multiset.toFinsupp_add, instIsOrderedCancelAddMonoidLexFinsupp, QuadraticMap.sum_polar_sub_repr_sq, Finsupp.curryEquiv_apply, Finsupp.card_Ioc, MvPolynomial.mem_image_support_coeff_finSuccEquiv, MvPolynomial.mapEquiv_symm, Finsupp.equivCongrLeft_apply, Finsupp.toMultiset_strictMono, MvPolynomial.scalarRTensor_apply_monomial_tmul, Finsupp.filter_smul, MvPolynomial.comapEquiv_symm_coe, MvPolynomial.homogeneousComponent_eq_zero', Module.basisUnique_repr_eq_zero_iff, WeierstrassCurve.Projective.eval_polynomial, Matrix.charpoly.univ_map_map, Nat.ordCompl_le, MvPolynomial.eval₂_expand, MvPolynomial.isOpenMap_comap_C, MvPolynomial.weightedDegree_eq_zero_iff, finsuppTensorFinsupp_apply, Finsupp.onFinset_apply, MvPolynomial.universalFactorizationMap_comp_map, MvPolynomial.aeval_algebraMap_eq_zero_iff, Representation.ofMulActionSelfAsModuleEquiv_symm_apply, Finsupp.mapDomain_le_mapDomain_iff_le, MvPowerSeries.support_expand, PolynomialModule.smul_def, instCountableFinsupp, MonomialOrder.degree_monomial, MvPolynomial.coeff_X_mul', IsBaseChange.finsuppPow, Finsupp.lmapDomain_id, IsPrimePow.minFac_pow_factorization_eq, Finsupp.coe_le_coe, NumberField.Units.fun_eq_repr, Algebra.PreSubmersivePresentation.ofHasCoeffs_map, Finsupp.singleAddHom_apply, MvPolynomial.expand_X, TensorProduct.equivFinsuppOfBasisLeft_symm_apply, algebraicIndependent_iff_ker_eq_bot, factorization_pow, IsBaseChange.basis_repr_comp_apply, SkewMonoidAlgebra.toFinsupp_smul, Module.DualBases.basis_repr_symm_apply, Module.Basis.toDual_linearCombination_left, groupHomology.chainsMap_f_3_comp_chainsIso₃_apply, MvPolynomial.IsSymmetric.map, LinearMap.prodOfFinsuppNat_injective, FreeAbelianGroup.toFinsupp_toFreeAbelianGroup, Finsupp.sumFinsuppLEquivProdFinsupp_apply, MvPolynomial.derivation_eq_of_forall_mem_vars, Algebra.Generators.cotangentSpaceBasis_apply, IsAdjoinRootMonic.coeff_apply, Module.Relations.Solution.surjective_π_iff_span_eq_top, Finsupp.supportedEquivFinsupp_symm_single, groupHomology.d₃₂_single, MvPolynomial.IsWeightedHomogeneous.pderiv, Rep.coindToInd_of_support_subset_orbit, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply, Representation.finsupp_apply, MvPolynomial.instIsReduced, MvPolynomial.X_pow_eq_monomial, MvPolynomial.isEmptyRingEquiv_apply, LinearMap.toMatrix_apply', WittVector.ghostComponent_apply, Finsupp.card_Ico, MvPolynomial.ker_map, Finsupp.toColex_monotone, Finsupp.filter_apply_neg, Finsupp.mapRange.linearEquiv_toAddEquiv, MvPolynomial.map_leftInverse, aeval_wittPolynomial, groupHomology.mapCycles₁_comp_apply, groupHomology.cyclesIso₀_inv_comp_iCycles_apply, AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop, MonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_apply, Matrix.repr_toLin, Finsupp.embSigma_zero, MvPolynomial.aeval_range, MvPowerSeries.coeff_pow, PolynomialModule.add_apply, KaehlerDifferential.mvPolynomialBasis_repr_D_X, Finsupp.multiset_sum_sum_index, PowerBasis.repr_pow_isIntegral, MvPolynomial.optionEquivLeft_C, MvPolynomial.rename_rename, Finsupp.linearCombination_id_surjective, TensorProduct.sum_tmul_basis_right_injective, Finsupp.mem_frange_of_mem, MvPolynomial.iterToSum_sumToIter, constantCoeff_wittStructureRat, Finsupp.isOrderedAddMonoid, Finsupp.sumElim_apply, Finset.finsuppAntidiagEquivSubtype_apply_coe, Algebra.Generators.toAlgHom_ofComp_localizationAway, MvPolynomial.leibniz_iff_X, Finsupp.domCongr_refl, Representation.freeLift_single_single, Finsupp.sum_zsmul, Finsupp.neLocus_neg_neg, Representation.finsuppTensorLeft_apply_tmul, MvPowerSeries.constantCoeff_subst, Finsupp.neLocus_add_left, Polynomial.homogenize_smul, Finsupp.sumFinsuppAddEquivProdFinsupp_symm_inl, MvPolynomial.divMonomial_add_modMonomial, Finsupp.mapDomain_nonneg, Finsupp.erase_same, groupHomology.eq_d₃₂_comp_inv, MvPowerSeries.trunc'_expand_trunc', AddCommMonCat.free_obj_coe, LinearMap.singularValues_zero, MvPolynomial.optionEquivLeft_X_some, Representation.LinearizeMonoidal.ε_η, AList.lookupFinsupp_eq_zero_iff, MonomialOrder.leadingCoeff_eq_zero_iff, rank_finsupp, MvPolynomial.eval₂Hom_monomial, MvPolynomial.homogeneousComponent_of_mem, LinearIndependent.linearCombination_repr, exteriorPower.basis_repr_ne, MvPolynomial.aeval_X_left_apply, Nat.factorization_le_factorization_mul_left, Polynomial.toPowerSeries_toMvPowerSeries, MvPolynomial.le_vanishingIdeal_zeroLocus, Finsupp.if_mem_support, Finsupp.filter_apply_pos, Algebra.Presentation.differentials.comm₂₃, rank_finsupp_self, MvPolynomial.homogeneousComponent_mem, Representation.ofCoinvariantsTprodLeftRegular_mk_tmul_single, MvPolynomial.pUnitAlgEquiv_symm_apply, Finsupp.prod_add_index_of_disjoint, MvPowerSeries.coeff_monomial_mul, Finsupp.weight_single_one_apply, MvPolynomial.expand_eq_zero, MvPowerSeries.exists_finsupp_eq_lexOrder_of_ne_zero, Module.Basis.mk_repr, Finsupp.span_single_eq_top, Module.Flat.finsupp, Finsupp.mapDomain_comapDomain_nat_add_one, MvPowerSeries.coeff_X_pow, WeierstrassCurve.Jacobian.baseChange_polynomialZ, AddSubgroup.exists_finsupp_of_mem_closure_range, MvPolynomial.support_monomial, Finsupp.instIsRightCancelAdd, Algebra.Presentation.localizationAway_relation, Ordinal.CNF.eval_single_add', sigmaFinsuppAddEquivDFinsupp_apply, List.toFinsupp_cons_eq_single_add_embDomain, MvPolynomial.monomial_finsupp_sum_index, MvPolynomial.weightedHomogeneousSubmodule_mul, Module.Relations.Solution.injective_fromQuotient_iff_ker_π_eq_span, Ideal.span_pow_eq_map_homogeneousSubmodule, MvPolynomial.coeffs_mul_X, Finsupp.sum_smul_index', MvPolynomial.mul_def, Finsupp.linearEquivFunOnFinite_symm_coe, Module.Basis.repr_isUnitSMul, MvPolynomial.natDegree_finSuccEquiv, Finsupp.prod_toMultiset, Finsupp.bot_eq_zero, StandardEtalePresentation.toPresentation_algebra_smul, Nat.coe_divisors_eq_prod_pow_le_factorization, Representation.linearize_single, MvPolynomial.totalDegree_X_pow, Ideal.span_eq_map_homogeneousSubmodule, Finsupp.toMultiset_zero, MvPolynomial.bind₂_comp_C, Span.repr_def, Finsupp.mapRange.addEquiv_refl, Submodule.mem_iSup_iff_exists_finsupp, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C, Finsupp.single_eq_same, MvPolynomial.eval₂_zero'_apply, MvPolynomial.image_comap_C_basicOpen, groupHomology.mem_cycles₂_iff, Finsupp.coe_ceilDiv_def, MvPolynomial.degreeOf_C, WeierstrassCurve.Projective.polynomial_relation, groupHomology.single_isCycle₂_iff_inv, Matrix.toMvPolynomial_add, Rep.coindToInd_indToCoind, Finsupp.le_weight_of_ne_zero', MvPolynomial.mem_support_iff, Finsupp.filter_eq_indicator, Ordinal.CNF.coeff_opow_mul_add, DFinsupp.toFinsupp_add, MvPolynomial.mvPolynomialEquivMvPolynomial_symm_apply, MvPolynomial.algHom_ext'_iff, Finsupp.subtypeDomain_add, IntermediateField.mem_adjoin_iff, Module.FaithfullyFlat.finsupp, AlgebraicIndependent.repr_ker, groupHomology.cyclesMap_comp_isoCycles₂_hom, MonomialOrder.leadingCoeff_mul_of_isRegular_right, chevalley_mvPolynomial_mvPolynomial, Finsupp.sum_smul_index_linearMap', MvPolynomial.mem_range_map_iff_coeffs_subset, Finsupp.support_single_add_single, linearIndependent_iff_injective_finsuppLinearCombination, MvPolynomial.notMem_support_iff, Finsupp.sum_single_add_single, AddMonoidAlgebra.exists, Finsupp.equivFunOnFinite_apply, MvPolynomial.aeval_X, MvPolynomial.comapEquiv_coe, MvPolynomial.vars_sub_of_disjoint, Finsupp.update_eq_add_single, MvPolynomial.exists_dvd_map_of_isAlgebraic, AddMonoidAlgebra.mapDomainAddEquiv_apply, Polynomial.pUnitAlgEquiv_symm_toPowerSeries, MvPolynomial.scalarRTensor_apply_X_tmul_apply, Nat.factorization_eq_of_coprime_right, groupHomology.comp_d₂₁_eq, Nat.factorization_mul_apply_of_coprime, MonoidAlgebra.exists, Finsupp.smulCommClass, Finsupp.support_zero, groupHomology.mapCycles₁_comp_assoc, Finsupp.mapRange_neg, MvPowerSeries.ext_trunc', Algebra.FormallyUnramified.finite_of_free_aux, MvPolynomial.smul_monomial, MvPolynomial.eval₂_pow, MvPolynomial.irreducible_mul_X_add, Module.Basis.prod_repr_inl, AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin, MvPowerSeries.LinearTopology.basis_le_iff, groupHomology.toCycles_comp_isoCycles₂_hom_assoc, MonomialOrder.leadingCoeff_mul, MonomialOrder.degree_sub_le, Finsupp.eq_indicator_iff, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, AnalyticOnNhd.eval_linearMap', Nat.ordCompl_dvd_ordCompl_iff_dvd, MvPolynomial.IsWeightedHomogeneous.weightedHomogeneousComponent_same, Finsupp.subtypeDomain_neg, Sym.coe_equivNatSum_apply_apply, MvPolynomial.optionEquivLeft_apply, MvPolynomial.instIsScalarTower, MvPolynomial.bind₂_C_left, MvPolynomial.totalDegree_coeff_finSuccEquiv_add_le, Finsupp.sigmaFinsuppAddEquivPiFinsupp_apply, Equiv.finsuppUnique_symm_apply_support_val, Finsupp.neLocus_self_add_left, MvPolynomial.map_comp_rename, Module.Relations.Solution.surjective_fromQuotient_iff_surjective_π, MvPolynomial.ACounit_X, WittVector.mul_polyOfInterest_aux2, MvPolynomial.prime_rename_iff, Nat.ordProj_of_not_prime, AddMonoidAlgebra.ofCoeff_eq_zero, Polynomial.eval_eq_div_eval_toTupleMvPolynomial, bind₁_xInTermsOfW_wittPolynomial, Finsupp.filter_neg, WeierstrassCurve.Jacobian.eval_polynomialY, AddMonoidAlgebra.supportedEquivFinsupp_apply_support_val, Finsupp.linearCombination_zero_apply, MvPowerSeries.min_lexOrder_le, Finset.mem_finsuppAntidiag, MvPolynomial.constantCoeff_rename, Finsupp.mem_supported, MonoidAlgebra.single_one_mul_apply, MvPolynomial.eval₂_prod, Module.Basis.repr_self_apply, Algebra.PreSubmersivePresentation.jacobiMatrix_reindex, groupHomology.mem_cycles₁_of_comp_eq_d₂₁, MvPolynomial.map_bind₂, Finsupp.mem_range_mapDomain_iff, FractionalIdeal.count_finsuppProd, Cardinal.mk_finsupp_lift_of_infinite, Finsupp.add_sub_single_one, Finsupp.mem_span_iff_linearCombination, MvPolynomial.iterToSum_C_X, AlgebraicClosure.maxIdeal.isMaximal, MvPolynomial.map_eval₂, Nat.pow_succ_factorization_not_dvd, MvPolynomial.eval_map, IsLocalFrameOn.coeff_apply_of_mem, CommRingCat.free_map_coe, Algebra.FinitePresentation.mvPolynomial_of_finitePresentation, Algebra.SubmersivePresentation.ofSubsingleton_algebra_algebraMap, MonoidAlgebra.coeff_smul, setBasisOfLinearIndependentOfCardEqFinrank_repr_apply, Algebra.Presentation.differentials.hom₁_single, Finsupp.Lex.addLeftMono, MvPolynomial.killCompl_comp_rename, MvPolynomial.map_eval₂Hom, MvPolynomial.supportedEquivMvPolynomial_symm_X, Finsupp.prod_add_index, Finsupp.Lex.single_strictAnti, LinearMap.sum_repr_mul_repr_mulₛₗ, Finsupp.single_smul, groupHomology.δ₀_apply, MvPolynomial.pderiv_one, MvPolynomial.mkDerivation_X, MvPolynomial.pderiv_mul, Representation.ofMulAction_apply, Finsupp.Colex.isOrderedCancelAddMonoid, Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp, char_dvd_card_solutions_of_add_lt, Finsupp.comapDomain_smul_of_injective, groupHomology.d₃₂_single_one_thd, MvPolynomial.comp_eval₂Hom, MvPolynomial.ACounit_surjective, Ideal.Filtration.mem_submodule, TopModuleCat.coe_freeObj, MvPolynomial.supported_eq_adjoin_X, MonomialOrder.degree_lt_iff, finTwoArrowEquiv'_apply, MvPolynomial.eval₂_zero, Finsupp.Colex.isStrictOrder, MvPolynomial.degreeOf_mul_le, MvPolynomial.degreeOf_sum_le, Ideal.finsuppTotal_apply_eq_of_fintype, groupHomology.isoCycles₁_inv_comp_iCycles_apply, Finsupp.erase_ne, KaehlerDifferential.quotKerTotalEquiv_symm_comp_D, strongRankCondition_iff_forall_not_injective, IntermediateField.LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, MvPolynomial.aeval_eq_eval, MvPolynomial.supDegree_esymmAlgHomMonomial, Finsupp.support_mul, AddSubmonoid.mem_closure_range_iff, MvPolynomial.schwartz_zippel_totalDegree, Rep.ε_def, PowerSeries.coeff_heval, MvPolynomial.aeval_ite_mem_eq_self, MvPolynomial.support_sdiff_support_subset_support_add, Finsupp.eq_single_iff, Algebra.SubmersivePresentation.map_jacobianOfHasCoeffs, MvPolynomial.le_weightedTotalDegree, AddSubmonoid.exists_finsupp_of_mem_closure_range, MvPolynomial.IsWeightedHomogeneous.mul, Ordinal.CNF.coeff_eq_zero_of_lt, MvPolynomial.eval₂Hom_C_id_eq_join₁, finsuppTensorFinsupp'_symm_single_eq_tmul_single_one, Rep.finsuppToCoinvariantsTensorFree_single, Module.Relations.Solution.IsPresentation.linearEquiv_symm_var, Submodule.mem_ideal_smul_span_iff_exists_sum', Finsupp.toMultiset_toFinsupp, MvPolynomial.eval_mem, PolynomialLaw.exists_lift', ax_grothendieck_of_definable, Algebra.Generators.algebraMap_surjective, Nat.Partition.toFinsuppAntidiag_mem_finsuppAntidiag, Module.Presentation.cokernel_relation, MvPolynomial.totalDegree_add_eq_right_of_totalDegree_lt, MvPolynomial.pow_idealOfVars, MvPolynomial.join₂_comp_map, MvPolynomial.idealOfVars_eq_restrictSupportIdeal, PolynomialLaw.toFun_eq_rTensor_φ_toFun', groupHomology.chains₁ToCoinvariantsKer_surjective, MvPolynomial.comap_id, Height.logHeight_eval_ge', LinearMap.leftInverse_splittingOfFinsuppSurjective, Representation.ofMulActionSubsingletonEquivTrivial_symm_apply, MvPolynomial.eval_rename_prod_mk, linearIndependent_iff_ker, Finsupp.coeFnAddHom_apply, SkewMonoidAlgebra.ofFinsupp_sum, AddMonoidAlgebra.ofCoeff_neg, MvPolynomial.optionEquivRight_C, Module.presentationFinsupp_G, Finsupp.mapRange.addEquiv_apply, Representation.finsuppTensorRight_apply_tmul, Pi.counit_comp_finsuppLcoeFun, MvPolynomial.monomial_zero, MvPolynomial.map_mvPolynomial_eq_eval₂, Finsupp.curryLinearEquiv_symm_apply_apply, Polynomial.Bivariate.Polynomial.Bivariate.pderiv_one_equivMvPolynomial, MonomialOrder.degree_reduce_lt, MvPolynomial.eval_eval₂, MvPolynomial.aevalTower_comp_C, Finsupp.llift_apply, MvPolynomial.totalDegree_eq, MvPolynomial.rename_msymm, MvPolynomial.comap_comp_apply, MvPolynomial.eval₂_id, AddMonoidAlgebra.single_apply, Finsupp.linearCombination_smul, Nat.factorization_factorial, MvPolynomial.eval₂Hom_C_eq_bind₁, Representation.leftRegularTensorTrivialIsoFree_symm_apply_single_single, groupHomology.cycles₁_eq_top_of_isTrivial, MonoidAlgebra.opRingEquiv_symm_apply, MvPolynomial.sum_antidiagonal_card_esymm_psum_eq_zero, Bundle.Trivialization.localFrame_coeff_eq_coeff, MvPolynomial.X_mul_cancel_right_iff, Algebra.PreSubmersivePresentation.ofHasCoeffs_relation, AddCommMonCat.free_map, Finsupp.erase_apply, MvPolynomial.degreeOf_coeff_finSuccEquiv, Finsupp.mapRange.addMonoidHom_apply, Multiset.toFinsupp_sum_eq, Finsupp.instSubsingleton', MvPolynomial.mem_pow_idealOfVars_iff, LinearMap.singularValues_antitone, Ideal.finsuppTotal_apply, Finsupp.ext_iff', MvPolynomial.X_prime, groupHomology.d₃₂_comp_d₂₁_assoc, MvPolynomial.rename_id_apply, MvPolynomial.constantCoeff_C, Finsupp.neLocus_eq_support_sub, Representation.LinearizeMonoidal.μ_apply_single_single, linearIndepOn_iff, Finsupp.some_zero, TensorProduct.equivFinsuppOfBasisLeft_apply_tmul_apply, Finsupp.lmapDomain_linearCombination, MvPowerSeries.trunc_C, Finsupp.notMem_support_iff, Finsupp.range_mapRange_linearMap, MvPolynomial.map_map, Finsupp.sumFinsuppAddEquivProdFinsupp_symm_apply, MvPolynomial.support_eq_empty, MonomialOrder.degree_mem_support_iff, Module.Basis.repr_algebraMap, Rep.μ_def, MvPolynomial.eval₂Hom_comp_bind₂, Finsupp.mapRange_neg', Multiset.support_sum_subset, Nat.ordCompl_div_of_dvd, MvPolynomial.degrees_def, MvPolynomial.coe_one, MvPolynomial.nonempty_support_finSuccEquiv, AddMonoidAlgebra.uniqueRingEquiv_apply, Finsupp.fun_support_eq, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, MvPolynomial.mvPolynomialEquivMvPolynomial_apply, Finsupp.univ_sum_single_apply', MvPolynomial.pderiv_rename, sigmaFinsuppAddEquivDFinsupp_symm_apply, Algebra.Presentation.comp_relation_inr, Finsupp.iInf_ker_lapply_le_bot, MonoidAlgebra.uniqueRingEquiv_apply, Finsupp.basis_repr, Matrix.toBilin_apply, IsLocalRing.basisQuotient_repr, Module.Relations.surjective_toQuotient, MvPolynomial.monomial_eq_monomial_iff, AddEquiv.finsuppUnique_symm, Module.End.ringHomEndFinsupp_apply_apply, MvPolynomial.mem_vars, MonomialOrder.toSyn_strictMono, MvPowerSeries.coeff_X, List.toFinsupp_apply_fin, Representation.ofMulAction_single, LinearMap.nilRankAux_basis_indep, MonomialOrder.leadingTerm_zero, AddMonoidAlgebra.opRingEquiv_symm_apply, groupHomology.single_one_snd_sub_single_one_fst_mem_boundaries₂, MvPolynomial.eval₂_mul_monomial, MvPolynomial.weightedHomogeneousComponent_zero, Finsupp.linearCombination_one_tmul, Polynomial.coeff_ofFinsupp, AddMonoidAlgebra.coeff_add, Finset.mem_finsuppAntidiag_insert, groupHomology.d₁₀ArrowIso_hom_left, MvPolynomial.support_killCompl, Finset.support_sum_subset, AlgebraicIndependent.aeval_comp_repr, MonomialOrder.div_single, MvPolynomial.esymmAlgHomMonomial_single, MvPolynomial.homogeneousComponent_C_mul, Module.Basis.map_repr, groupHomology.cycles₁IsoOfIsTrivial_hom_apply, MvPolynomial.IsHomogeneous.map, PowerSeries.support_expand_subset, Finsupp.liftAddHom_comp_single, MvPolynomial.map_expand, AddMonoidAlgebra.coeff_sub, MonomialOrder.image_leadingTerm_sdiff_singleton_zero, Representation.coinvariantsFinsuppLEquiv_apply, Finsupp.card_toMultiset, Finsupp.update_self, LinearMap.toMatrixAlgEquiv_apply, MvPolynomial.map_aeval, Finsupp.sum_sub_index, MvPolynomial.instFree, Algebra.TensorProduct.basis_repr_tmul, Sym.coe_equivNatSum_symm_apply, MvPolynomial.map_frobenius_expand, Finsupp.disjoint_iff, Finsupp.comapSMul_single, MvPolynomial.coeffs_one, Finsupp.lmapDomain_comp, groupHomology.d₂₁_single_inv_mul_ρ_add_single, MvPolynomial.renameEquiv_trans, MvPolynomial.weightedDecomposition.decompose'_apply, Height.logHeight_eval_le', NumberField.mixedEmbedding.stdBasis_apply_isComplex_snd, FirstOrder.Ring.lift_genericPolyMap, Finsupp.Lex.wellFounded', Nat.ordCompl_dvd_ordCompl_of_dvd, MvPolynomial.coeffs_one_of_nontrivial, Finsupp.supported_inter, MvPolynomial.expand_monomial, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord, Finsupp.sum_smul_index, Finsupp.LinearEquiv.finsuppUnique_symm_apply, MvPolynomial.expand_char, MvPolynomial.monomial_mul_mem_coeffsIn, Finsupp.span_le_supported_biUnion_support, MvPolynomial.eval₂Hom_congr, WeierstrassCurve.Jacobian.eval_polynomialX_of_Z_ne_zero, Finsupp.cons_succ, MvPolynomial.map_rename, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc, Finset.finsuppAntidiag_empty_of_ne_zero, groupHomology.d₁₀_comp_coinvariantsMk_apply, LinearMap.BilinForm.apply_eq_dotProduct_toMatrix_mulVec, KaehlerDifferential.kerTotal_eq, Finsupp.mapDomain_nonpos, Finsupp.span_image_eq_map_linearCombination, MvPowerSeries.hasSum_aeval, Algebra.PreSubmersivePresentation.ofHasCoeffs_σ', MvPolynomial.killCompl_C, Algebra.Presentation.quotientEquiv_symm, MvPolynomial.eval₂_const_pUnitAlgEquiv_symm, MvPowerSeries.coeff_truncFinset_of_mem, MvPowerSeries.weightedOrder_monomial_of_ne_zero, MvPolynomial.eval_comp_toMvPolynomial, Algebra.Generators.H1Cotangent.δAux_C, Algebra.Generators.map_toComp_ker, MvPolynomial.support_finSuccEquiv_nonempty, Algebra.Generators.Hom.toExtensionHom_toAlgHom_apply, AddMonoidAlgebra.divOf_apply, MvPolynomial.eval₂_sum, LinearIndependent.repr_eq_single, PowerSeries.support_expand, Finsupp.small, MvPolynomial.bind₁_X_left, HahnSeries.toMvPowerSeries_symm_apply_coeff, MvPolynomial.monomial_one_dvd_iff_modMonomial_eq_zero, IsAdjoinRootMonic.basis_repr, Representation.leftRegular_norm_eq_zero_iff, Finsupp.supported_eq_span_single, TensorProduct.finsuppLeft_smul', MvPolynomial.sumAlgEquiv_comp_rename_inr, Finsupp.support_add_single, groupHomology.chainsMap_f_3_comp_chainsIso₃, Finsupp.mapRange.addEquiv_toEquiv, Nat.factorization_mul, MvPolynomial.aevalTower_toAlgHom, groupHomology.mapCycles₁_id_comp_assoc, Algebra.Generators.ofComp_val, Finsupp.filter_sum, MvPolynomial.coe_eq_one_iff, Algebra.Presentation.map_relationOfHasCoeffs, AddMonoidAlgebra.ofCoeff_injective, Finsupp.finite_support, LinearMap.polyCharpoly_coeff_isHomogeneous, Algebra.TensorProduct.basisAux_map_smul, Pi.basis_repr_single, Module.Relations.Solution.fromQuotient_toQuotient, groupHomology.eq_d₂₁_comp_inv, Finsupp.eq_option_embedding_update_none_iff, Finset.count_coe_finsuppAntidiagEquiv_apply, MvPolynomial.eval₂_map, TensorProduct.equivFinsuppOfBasisRight_apply_tmul, MvPolynomial.X_mul_pderiv_monomial, MvPowerSeries.lexOrder_def_of_ne_zero, MonomialOrder.degree_add_le, Module.Basis.ofEquivFun_repr_apply, Finsupp.mapRange_sub', MvPolynomial.degree_optionEquivLeft, Finsupp.supported_univ, Finsupp.mapDomain_surjective, MvPolynomial.mapAlgHom_id, Algebra.Generators.naive_val, Module.Basis.sumQuot_repr_left, MonomialOrder.leadingCoeff_prod_of_regular, groupHomology.mapCycles₁_comp, MvPowerSeries.LinearTopology.mem_basis_iff, Representation.ofMulAction_self_smul_eq_mul, Module.Basis.reindexRange_repr', Finsupp.sum_ite_eq, Ordinal.CNF.coeff_zero_apply, MvPolynomial.totalDegree_list_prod, Finsupp.indicator_of_notMem, MvPolynomial.coeff_expand_smul, Finsupp.optionElim_some, Algebra.Generators.algebraMap_apply, Finsupp.sum_fintype, Module.Basis.reindexRange_repr, Finsupp.some_add, Finsupp.embDomain_refl, Finsupp.mapRange.equiv_refl, MvPolynomial.map_esymm, AddMonoidAlgebra.coeff_sum, Finsupp.mem_rangeSingleton_apply_iff, Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply, TensorProduct.equivFinsuppOfBasisLeft_apply_tmul, MvPolynomial.weightedHomogeneousComponent_eq_zero', PiTensorProduct.ofFinsuppEquiv'_tprod_single, Nat.factorization_eq_card_pow_dvd_of_lt, MvPolynomial.IsHomogeneous.add, MonoidAlgebra.single_mul_apply, MvPolynomial.coe_eq_zero_iff, MvPolynomial.expand_C, Finsupp.single_eq_zero, MvPowerSeries.trunc'_trunc'_pow, factorization_mul, TensorProduct.equivFinsuppOfBasisLeft_symm, MonomialOrder.eq_C_of_degree_eq_zero, Polynomial.finsuppSum_homogenize_eq, MonoidAlgebra.mapRingHom_apply, Module.Presentation.finsupp_R, instIsIntegralMvPolynomial, MvPolynomial.derivation_eq_zero_of_forall_mem_vars, DFinsupp.toFinsupp_sub, MvPolynomial.coeffs_C, Submodule.mulLeftMap_apply, AddMonoidAlgebra.neg_apply, TensorProduct.finsuppScalarRight_apply, Finsupp.zipWith_apply, Algebra.Generators.compLocalizationAwayAlgHom_X_inl, MvPolynomial.optionEquivRight_X_none, MvPolynomial.homogeneousComponent_isHomogeneous, MvPolynomial.rename_psum, Module.Relations.Solution.ofQuotient_var, BoundedContinuousFunction.mem_charPoly, groupHomology.mapCycles₁_comp_i, Finsupp.Lex.isStrictOrder, Algebra.Generators.map_ofComp_ker, Finsupp.toMultiset_apply, Finsupp.embDomain_injective, MvPowerSeries.lexOrder_mul, BoundedContinuousFunction.charAlgHom_apply, Finsupp.Colex.addRightMono, TensorProduct.finsuppScalarRight_apply_tmul, WeierstrassCurve.Jacobian.polynomialY_eq, MvPolynomial.sum_homogeneousComponent, MvPolynomial.expand_zero, MvPolynomial.support_add, MonomialOrder.sPolynomial_self, Finsupp.coe_pointwise_smul, MvPolynomial.degreesLE_nsmul, MvPolynomial.coe_monomial, Ordinal.CNF.coeff_of_not_mem_CNF, WeierstrassCurve.Jacobian.eval_polynomialX, Polynomial.derivativeFinsupp_apply_toFun, MvPolynomial.totalDegree_rename_le, MvPolynomial.C_apply, Finsupp.filter_curry, MonomialOrder.leadingCoeff_mul_of_right_mem_nonZeroDivisors, MvPolynomial.coe_mapEquivMonic_comp', Algebra.Presentation.naive_relation, LieAlgebra.LoopAlgebra.toFinsupp_symm_single, Finsupp.update_eq_single_add, Finsupp.DegLex.single_lt_iff, WeierstrassCurve.Projective.eval_polynomialX, Finsupp.add_eq_zero_iff, WeierstrassCurve.Projective.baseChange_polynomial, Module.Basis.repr_smul, Nat.ordProj_dvd_ordProj_iff_dvd, Matrix.toMvPolynomial_map, MvPolynomial.single_eq_monomial, Polynomial.toMvPolynomial_eq_rename_comp, MvPowerSeries.trunc_one, finsuppTensorFinsupp'_single_tmul_single, Finsupp.mapDomain.coe_linearEquiv, Finsupp.single_eq_of_ne, DividedPowerAlgebra.dp_mul, MonomialOrder.le_degree, AddMonoidAlgebra.grade_eq_lsingle_range, Polynomial.aeval_homogenize_X_one, MvPolynomial.adjoin_range_X, MvPolynomial.mul_X_mem_coeffsIn, NumberField.canonicalEmbedding.integralBasis_repr_apply, ChevalleyThm.chevalley_mvPolynomialC, Finsupp.Colex.wellFoundedLT, sigmaFinsuppEquivDFinsupp_add, MvPolynomial.coeff_C, WeierstrassCurve.Jacobian.eval_polynomialY_of_Z_ne_zero, Finsupp.Colex.addRightStrictMono, MonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure, AddMonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure, Finsupp.lcoeFun_comp_lsingle, MvPolynomial.bind₂_map, MvPolynomial.totalDegree_mul_of_isDomain, Finsupp.weight_single, Finset.sum_apply', Nat.exists_factorization_lt_of_lt, Finsupp.isOrderedCancelAddMonoid, Finsupp.embSigma_add, Finsupp.antidiagonal_single, MvPolynomial.X_dvd_X, MvPolynomial.transcendental_polynomial_aeval_X_iff, MvPolynomial.aeval_algebraMap_eq_zero_iff_of_injective, MvPolynomial.eval₂_neg, QuadraticMap.map_finsuppSum, Algebra.Generators.algebraMap_eq, constantCoeff_wittStructureInt, Finsupp.lcoeFun_apply, Finsupp.single_sub, Algebra.SubmersivePresentation.ofSubsingleton_relation, Finsupp.sub_add_single_one_cancel, basisOfLinearIndependentOfCardEqFinrank_repr_apply, StandardEtalePair.equivMvPolynomialQuotient_symm_apply, MonomialOrder.leadingTerm_monomial, Finsupp.mapRange.equiv_symm, MvPolynomial.X_mul_mem_coeffsIn, Nat.ordCompl_pow_mul_eq_self_iff, MvPolynomial.support_rename_of_injective, Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial, MvPolynomial.comap_comp, MvPowerSeries.monomial_def, MvPolynomial.eval_ofNat, MonomialOrder.degree_mul_leadingTerm, PiTensorProduct.ofFinsuppEquiv_tprod_single, Module.Presentation.finsupp_G, AddMonoidAlgebra.ofCoeff_sub, Finsupp.toFreeAbelianGroup_comp_singleAddHom, xInTermsOfW_eq, LinearMap.nilRank_eq_polyCharpoly_natTrailingDegree, Finsupp.mapDomain_injOn, Module.Relations.range_map, MvPolynomial.eval_eq_eval_mv_eval', Nat.factorization_eq_one_of_squarefree, Finsupp.unique_single, MvPolynomial.IsHomogeneous.degree_eq_sum_deg_support, MvPolynomial.degrees_map_of_injective, MvPolynomial.ACounit_C, Finsupp.le_def, LinearMap.polyCharpoly_baseChange, Representation.LinearizeMonoidal.μ_comp_assoc, MvPolynomial.eq_zero_of_eval_eq_zero, MvPolynomial.transcendental_supported_X_iff, Polynomial.homogenize_add, Nat.factorization_choose_prime_pow_add_factorization, MvPolynomial.vanishingIdeal_pointToPoint, Module.Basis.SmithNormalForm.repr_apply_embedding_eq_repr_smul, MvPolynomial.optionEquivLeft_X_none, DFinsupp.toFinsupp_smul, MvPowerSeries.coeff_trunc'_mul_trunc'_eq_coeff_mul, MvPolynomial.algebraicIndependent_polynomial_aeval_X, MvPowerSeries.le_lexOrder_iff, groupHomology.single_one_fst_sub_single_one_snd_mem_boundaries₂, Finsupp.floorDiv_apply, MvPolynomial.IsHomogeneous.HomogeneousSubmodule.gcommSemiring, Representation.coinvariantsTprodLeftRegularLEquiv_apply, MvPolynomial.degreeOf_rename_of_injective, Finsupp.sum_ite_eq', MvPolynomial.degreesLE_add, finsuppTensorFinsuppLid_symm_single_smul, MonoidAlgebra.ofCoeff_sub, MvPolynomial.exists_rename_eq_of_vars_subset_range, Finsupp.ker_mapRange, MonomialOrder.span_leadingTerm_eq_span_monomial, MvPolynomial.optionEquivRight_symm_apply, Nat.factorization_prod_apply, Finsupp.erase_add, MvPolynomial.instIsPrimeVanishingIdealSingletonForallSet, MvPolynomial.eval₂Hom_zero_apply, Multiset.toFinsupp_union, MonomialOrder.span_leadingTerm_eq_span_monomial₀, groupHomology.mapCycles₂_id_comp, MvPolynomial.scalarRTensor_apply_tmul, MvPolynomial.degrees_C, Finsupp.supported_comap_lmapDomain, MonomialOrder.degree_neg, Finsupp.update_apply, Finsupp.prod_zpow, Finsupp.rangeIcc_toFun, Nat.properDivisors_eq_image_Iio_factorization_prod_pow, WeierstrassCurve.Jacobian.polynomial_relation, KaehlerDifferential.kerTotal_mkQ_single_algebraMap_one, finsuppTensorFinsupp'_symm_single_mul, LinearMap.polyCharpolyAux_map_eval, ZSpan.repr_ceil_apply, Finsupp.domLCongr_trans, MvPolynomial.eval_prod, LinearMap.polyCharpoly_coeff_eq_zero_of_basis, SkewMonoidAlgebra.toFinsupp_sub, MvPolynomial.C_mul_X_eq_monomial, Algebra.Generators.Hom.aeval_val, Finsupp.add_apply, Finsupp.mapRange_smul, MonoidAlgebra.coeff_neg, Polynomial.MonicDegreeEq.freeMonic_coe, LinearMap.singularValues_nonneg, DividedPowerAlgebra.natFactorial_mul_dp_eq, lp.zeroBasis_repr_apply, MvPolynomial.degreeOf_mul_eq, Algebra.Presentation.comp_aeval_relation_inl, Multiset.mem_sup_map_support_iff, Finset.mem_finsupp_iff, MvPowerSeries.WithPiTopology.as_tsum, Finsupp.indicator_apply, MvPolynomial.degreeOf_le_iff, MvPolynomial.C_0, WittVector.mulN_coeff, groupHomology.d₂₁_single_inv_self_ρ_sub_self_inv, MvPolynomial.bind₂_monomial, Module.Basis.addSubgroupOfClosure_repr_apply, MvPolynomial.isUnit_iff_totalDegree_of_isReduced, MvPolynomial.totalDegree_finset_prod, AddMonoidAlgebra.smul_apply, Module.Basis.span_repr_eq_single, MvPolynomial.monomialOneHom_apply, Finsupp.sumFinsuppLEquivProdFinsupp_symm_apply, Finsupp.support_add_eq, Module.Basis.repr_range, Representation.ofMulActionSubsingletonEquivTrivial_apply, Finsupp.comapDomain_zero, basis_toMatrix_basisFun_mul, Finsupp.prod_add_index', MvPolynomial.leadingCoeff_esymmAlgHomMonomial, Nat.factorization_one_right, Finsupp.neLocus_zero_left, instFinitePresentationFinsupp, Algebra.SubmersivePresentation.jacobianRelations_spec, Finsupp.finite_range, Finsupp.lex_iff_of_unique, MvPolynomial.pderiv_sumToIter, MvPolynomial.coeff_homogeneousComponent, MvPolynomial.support_expand_subset, Module.Basis.isScalarTower_finsupp, Rep.coindFunctorIso_inv_app_hom_toFun_coe, Submodule.LinearDisjoint.linearIndependent_right_of_flat, TensorProduct.finsuppLeft_symm_apply_single, Finsupp.linearEquivFunOnFinite_symm_apply, Finsupp.toDFinsupp_coe, MonomialOrder.coeff_prod_sum_degree, MvPolynomial.totalDegree_C, LinearMap.toMvPolynomial_add, WeierstrassCurve.Projective.polynomialZ_eq, MonomialOrder.lex_lt_iff_of_unique, finsuppTensorFinsupp'_apply_apply, MvPolynomial.IsSymmetric.one, Finsupp.finset_sum_apply, SkewMonoidAlgebra.toFinsuppAddEquiv_apply, Matrix.charpoly.univ_monic, MvPolynomial.totalDegree_pow, MvPolynomial.coeff_rename_embDomain, MvPolynomial.isUnit_iff, FreeAbelianGroup.equivFinsupp_symm_apply, Rep.coinvariantsTensorFreeLEquiv_apply, Finsupp.uncurry_apply, PiTensorProduct.ofFinsuppEquiv_symm_single_tprod, MvPolynomial.monomial_left_inj, Finsupp.leftInverse_lcomapDomain_mapDomain, Module.Basis.reindexRange_repr_self, AddCommGroup.equiv_free_prod_directSum_zmod, MvPolynomial.X_dvd_monomial, MvPolynomial.coe_zero, MonomialOrder.degLex_le_iff, groupHomology.toCycles_comp_isoCycles₁_hom_apply, TensorProduct.toIntegralClosure_mvPolynomial_bijective, MvPolynomial.finSuccEquiv_coeff_coeff, Ordinal.CNF.coeff_of_mem_CNF, MvPolynomial.rename_comp_expand, Finsupp.single_eq_of_ne', Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, Algebra.PreSubmersivePresentation.jacobiMatrix_apply, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C', MvPowerSeries.monomial_zero_eq_C, Finsupp.multinomial_of_support_subset, MvPowerSeries.coeff_inv, MvPolynomial.coeff_C_mul, MvPolynomial.rename_esymm, Rep.δ_def, MvPolynomial.IsHomogeneous.sub, PolynomialModule.single_apply, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_algebraMap_apply, Finsupp.support_mul_subset_right, MvPolynomial.quotient_map_C_eq_zero, Finsupp.single_apply_left, Finsupp.linearCombination_linear_comp, groupHomology.mapCycles₂_comp_i, MvPolynomial.iterToSum_X, Module.Basis.repr_eq_iff, MvPolynomial.coeff_X_pow, MvPolynomial.C_mul_monomial, Finsupp.le_iff, Finsupp.mem_submodule_iff, Finsupp.comp_liftAddHom, Algebra.Generators.H1Cotangent.δAux_monomial, Module.Basis.sumQuot_repr_inl, MvPolynomial.vars_monomial, Finsupp.sigmaFinsuppEquivPiFinsupp_apply, MvPolynomial.pow_idealOfVars_eq_span, Finsupp.lt_of_forall_lt_of_lt, Nat.ordProj_mul_ordCompl_eq_self, AnalyticOnNhd.eval_linearMap, Finsupp.mem_range_embDomain_iff, MvPolynomial.IsHomogeneous.pow, Nat.pairwise_coprime_pow_primeFactors_factorization, LaurentPolynomial.C_apply, MvPolynomial.IsWeightedHomogeneous.sum, groupHomology.boundariesOfIsBoundary₁_coe, Algebra.Generators.toAlgHom_ofComp_surjective, Finsupp.coe_neLocus, KaehlerDifferential.kerTotal_mkQ_single_add, IsBaseChange.of_basis, MvPolynomial.bind₁_comp_bind₁, Finsupp.mapRange.addMonoidHom_toZeroHom, MvPolynomial.commAlgEquiv_C, MvPolynomial.coeff_zero_C, MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported, Algebra.Generators.Hom.algebraMap_toAlgHom', Algebra.FinitePresentation.ker_fg_of_mvPolynomial, Algebra.Generators.cotangentSpaceBasis_repr_tmul, MonomialOrder.monic_X_add_C, MvPolynomial.aevalTower_X, MvPolynomial.vars_sub_subset, finsuppEquivDFinsupp_apply, MvPolynomial.bind₂_monomial_one, MvPolynomial.irreducible_of_forall_totalDegree_le, MvPolynomial.mem_support_notMem_vars_zero, MvPolynomial.commAlgEquiv_X, AddMonoidAlgebra.modOf_apply_of_not_exists_add, Finsupp.comul_comp_lapply, MvPolynomial.mapEquiv_apply, MvPolynomial.eval₂Hom_congr', Algebra.TensorProduct.equivFinsuppOfBasis_apply, Matrix.charpoly.univ_coeff_eval₂Hom, Finsupp.instSubsingleton, Multiset.toFinsupp_inter, MvPolynomial.optionEquivRight_X_some, Finsupp.sumFinsuppLEquivProdFinsupp_symm_inl, MonomialOrder.degree_le_iff, MvPolynomial.aeval_expand, AlgebraicIndependent.lift_reprField, MvPolynomial.instCharZero, Module.Basis.repr_linearCombination, groupHomology.eq_d₃₂_comp_inv_apply, MvPolynomial.aeval_algebraMap_apply, StdSimplex.nonneg, LaurentPolynomial.T_apply, Finsupp.embSigma_eq_zero, Finsupp.ceilDiv_apply, MvPolynomial.C_1, MvPolynomial.eval₂Hom_X', IsNonarchimedean.eval_mvPolynomial_le, Algebra.TensorProduct.equivFinsuppOfBasis_symm_apply, List.coe_toFinsupp, MvPolynomial.eval₂_one, MvPolynomial.rTensor_apply_X_tmul, Algebra.SubmersivePresentation.map_invJacobianOfHasCoeffs, Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation, wittPolynomial_one, MvPolynomial.pderiv_X, Algebra.FiniteType.baseChangeAux_surj, MvPowerSeries.coeff_homogeneousComponent, MvPolynomial.eval₂_mul_eq_zero_of_right, MonoidAlgebra.mapRangeAlgHom_apply, MvPolynomial.eval_eq', PiLp.basisFun_repr, MvPolynomial.uniqueFactorizationMonoid, MvPolynomial.restrictSupport_univ, Finsupp.degree_apply, Finsupp.domCongr_apply, Finsupp.exists_le_degree_eq, Algebra.Generators.H1Cotangent.δAux_toAlgHom, Representation.LinearizeMonoidal.ε_one, Finsupp.linearCombination_single_index, Finsupp.prod_unique, FreeAbelianGroup.toFinsupp_comp_toFreeAbelianGroup, MvPolynomial.eval₂_C, groupHomology.single_one_fst_sub_single_one_fst_mem_boundaries₂, Finsupp.lift_apply, LinearIndependent.linearCombinationEquiv_apply_coe, Subalgebra.mvPolynomial_aeval_coe, Nat.factorization_choose_le_one, Module.Relations.Solution.range_π, IsLocalization.Away.mvPolynomialQuotientEquiv_apply, Representation.LinearizeMonoidal.μ_comp_rTensor, TensorProduct.equivFinsuppOfBasisRight_apply_tmul_apply, Algebra.Presentation.naive_relation_apply, Finsupp.subtypeDomain_finsupp_sum, MvPolynomial.C_add, PolynomialLaw.exists_lift, LinearMap.toMvPolynomial_zero, Finsupp.Colex.wellFoundedLT_of_finite, Multiset.toFinsupp_apply, groupHomology.mapCycles₁_id_comp_apply, MonoidAlgebra.single_mul_apply_aux, Finsupp.sum_add_index', Finsupp.toFreeAbelianGroup_single, MvPolynomial.vars_eq_support_biUnion_support, MvPolynomial.isHomogeneous_C_mul_X, WittVector.mul_polyOfInterest_aux4, Equiv.finsuppUnique_apply, LinearIndependent.linearCombination_comp_repr, MvPolynomial.rename_eval₂, MonomialOrder.support_leadingTerm', Finsupp.single_eq_update, MvPolynomial.coeff_sum_X_pow_of_fintype, Finsupp.optionElim_eq_elim', AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some, MvPowerSeries.coeff_subst, MvPolynomial.coeff_smul, Finsupp.apply_surjective, MvPowerSeries.expand_eq_expand, MvPolynomial.irreducible_of_disjoint_support, Algebra.Generators.localizationAway_σ, Finsupp.embDomain_eq_zero, MvPolynomial.isWeightedHomogeneous_one, Representation.LinearizeMonoidal.μ_δ, sigmaFinsuppEquivDFinsupp_symm_apply, Finsupp.comapDomain_single_of_not_mem_range, Polynomial.derivativeFinsupp_apply_apply, MvPolynomial.mapAlgEquiv_apply, Polynomial.Bivariate.equivMvPolynomial_symm_X_0, MvPolynomial.algebraTensorAlgEquiv_symm_comp_aeval, Nat.dvd_ordCompl_of_dvd_not_dvd, MvPolynomial.finitePresentation_universalFactorizationMap, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, MvPolynomial.mapAlgEquiv_refl, WittVector.frobeniusPoly_zmod, AddEquiv.finsuppUnique_apply, MvPolynomial.totalDegree_multiset_prod, Finsupp.finite_of_nat_weight_le, MvPolynomial.eval_neg, Module.Presentation.finsupp_var, Algebra.FiniteType.iff_quotient_mvPolynomial', MvPolynomial.map_restrict_dom_evalₗ, Algebra.Presentation.differentials.surjective_hom₁, Polynomial.sum_eq_natDegree_of_mem_support_homogenize, Nat.Prime.dvd_iff_one_le_factorization, MvPolynomial.tensorEquivSum_one_tmul_C, MvPolynomial.eq_modMonomial_single_iff, MvPolynomial.rTensor_apply_tmul, Finsupp.codisjoint_supported_supported, MvPolynomial.IsWeightedHomogeneous.weightedHomogeneousComponent_ne, LinearMap.singularValues_eq_zero_iff, Finsupp.supported_union, MvPolynomial.IsSymmetric.mul, Module.Basis.linearCombination_dualBasis, Finsupp.prod_of_support_subset, Finsupp.isLowerSet_range_embDomain, groupHomology.π_comp_H2Iso_hom, FiniteDimensional.basisSingleton_repr_apply, WeierstrassCurve.Jacobian.baseChange_polynomialY, MonomialOrder.Monic.pow, MonomialOrder.degree_mul_of_isRegular_right, MvPolynomial.map_ofNat, Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom, Finsupp.mapDomain_mono, MvPolynomial.coeff_monomial_mul, Finset.mapRange_finsuppAntidiag_eq, Polynomial.degree_freeMonic, Finset.finsuppAntidiagEquivSubtype_symm_apply_coe, Finsupp.sum_sum_index', MvPolynomial.IsWeightedHomogeneous.add, Finsupp.instFaithfulSMulOfNonempty, MvPolynomial.eval₂Hom_rename, MvPolynomial.degreeOf_pow_eq, LieModule.rank_eq_natTrailingDegree, MvPolynomial.bind₂_id, Finsupp.le_degree, Module.Basis.equivFunL_symm_apply_repr, MvPolynomial.degree_degLexDegree, PowerBasis.repr_gen_pow_isIntegral, MvPolynomial.X_mul_cancel_left_iff, Finsupp.card_Icc, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, Rep.coindToInd_apply, Finsupp.equivFunOnFinite_symm_apply_support, groupHomology.mapCycles₁_comp_i_apply, Finsupp.sum_unique, Polynomial.derivativeFinsupp_derivative, MvPolynomial.sumAlgEquiv_comp_rename_inl, Subalgebra.LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, Finsupp.lsum_single, KaehlerDifferential.ker_map, MvPolynomial.dvd_monomial_iff_exists, Finsupp.ceilDiv_def, groupHomology.mapCycles₂_comp, WeierstrassCurve.Projective.baseChange_polynomialY, AlgebraicIndependent.aeval_of_algebraicIndependent, LinearMap.CompatibleSMul.finsupp_dom, LinearMap.BilinForm.sum_repr_mul_repr_mul, Finsupp.linearEquivFunOnFinite_single, Finsupp.supported_iInter, Module.Basis.mulOpposite_repr_op, MvPolynomial.aeval_bind₁, Module.Basis.smulTower'_repr_mk, Finsupp.single_finset_sum, Finsupp.rangeIcc_apply, MonomialOrder.degree_sum_le, instTwoUniqueSumsFinsupp, MonomialOrder.degree_mul_of_mul_leadingCoeff_ne_zero, MvPolynomial.X_dvd_mul_iff, MonomialOrder.leadingCoeff_pow_of_pow_leadingCoeff_ne_zero, MvPolynomial.DirectSum.coeAddMonoidHom_eq_support_sum, instIsLocalizedModuleFinsuppLinearMap, Matrix.GeneralLinearGroup.toLin'_apply, Representation.linearizeTrivialIso_apply, MvPolynomial.algebraMap_apply, MvPolynomial.mkDerivationₗ_monomial, Finsupp.counit_comp_lsingle, Finsupp.le_weight, MvPolynomial.killCompl_monomial_eq_zero_of_not_subset, MvPolynomial.exists_fin_rename, TensorProduct.finsuppScalarRight_smul, LinearMap.toMvPolynomial_baseChange, AList.lookupFinsupp_eq_iff_of_ne_zero, Finset.mem_finsupp_iff_of_support_subset, MvPolynomial.optionEquivLeft_coeff_coeff, MonomialOrder.degree_subsingleton, MvPolynomial.IsWeightedHomogeneous.sum_weight_X_mul_pderiv, Matrix.charpoly.optionEquivLeft_symm_univ_isHomogeneous, Finsupp.filter_add, groupHomology.coe_mapCycles₂, finsuppTensorFinsupp_single, Nat.factorization_zero, Finsupp.instSMulPosReflectLT, Cardinal.mk_finsupp_nat, MvPolynomial.sum_weightedHomogeneousComponent, MvPolynomial.exists_degree_lt, MvPowerSeries.truncFinset_C, MonoidAlgebra.coeffLinearEquiv_symm_apply, MvPolynomial.C_surjective, Finsupp.card_uIcc, AList.empty_lookupFinsupp, LinearMap.injective_iff_forall_lt_finrank_singularValues_pos, MvPolynomial.pderiv_def, MvPolynomial.isEmptyRingEquiv_symm_apply, groupHomology.comp_d₁₀_eq, MvPolynomial.finsupp_support_eq_support, AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord, Finsupp.card_Ioo, MonomialOrder.degree_leadingTerm_mul, MvPolynomial.hom_eq_hom, groupHomology.H1π_comp_map_apply, Nat.ceilRoot_def, MvPolynomial.mem_pow_idealOfVars_iff', Module.Basis.repr_reindex, MvPolynomial.mem_supported, Matrix.toMvPolynomial_zero, Finsupp.comapDomain_surjective, MvPolynomial.renameEquiv_apply, MvPolynomial.degrees_pow_le, Finsupp.DegLex.single_antitone, Finsupp.Lex.single_lt_iff, Finsupp.support_sum, MvPolynomial.rename_esymmAlgHom, Module.subsingletonEquiv_symm_apply, Nat.dvd_iff_div_factorization_eq_tsub, MvPolynomial.ne_zero_iff, Finsupp.mk_mem_graph_iff, IsLocalizedModule.map_linearCombination, rank_finsupp_self', Module.Basis.algebraMapCoeffs_repr_apply_toFun, MvPolynomial.aeval_eq_zero, Finsupp.filter_sub, MvPolynomial.eval₂_cast_comp, Finsupp.mapDomain_lt_mapDomain_iff_lt, Algebra.PreSubmersivePresentation.naive_toPresentation, MonoidAlgebra.coeffEquiv_symm_apply, Polynomial.eval_homogenize, LinearMap.toMatrix_mulVec_repr, Finsupp.sum_filter_index, AddMonoidAlgebra.apply_add_of_supDegree_le, Finsupp.sum_neg_index, Finsupp.single_eq_set_indicator, SkewMonoidAlgebra.ofFinsupp_injective, Finsupp.filter_eq_sum, Finsupp.snd_sumFinsuppAddEquivProdFinsupp, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul, Matrix.toLin_apply_eq_zero_iff, MvPolynomial.modMonomial_add_divMonomial, Finsupp.erase_eq_sub_single, AddMonoidAlgebra.modOf_apply_of_exists_add, MonomialOrder.span_leadingTerm_eq_span_monomial', Finsupp.mem_toMultiset, MvPolynomial.bind₁_C_right, Finsupp.single_le_sum, MvPolynomial.coe_coeffs_map, Polynomial.toTupleMvPolynomial_one_eq, linearDepOn_iff, AddMonoidAlgebra.coe_add, MvPolynomial.decompose'_apply, DFinsupp.toFinsupp_coe, MvPolynomial.rename_zero, groupHomology.toCycles_comp_isoCycles₁_hom_assoc, Module.Basis.algebraMapCoeffs_repr_apply_apply, Matrix.toLinearMapₛₗ₂_apply, MvPolynomial.instIsLocalHomRingHomAlgebraMap, Finsupp.lcomapDomain_apply, WittVector.bind₁_wittMulN_wittPolynomial, Finsupp.lhom_ext'_iff, LinearMap.BilinForm.dualBasis_repr_apply, MvPowerSeries.coeff_one, PolynomialLaw.exists_range_φ_eq_of_fg, Algebra.FinitePresentation.mvPolynomial, MvPowerSeries.truncFinset_map, IsIsotypicOfType.linearEquiv_finsupp, MvPolynomial.coeff_single_X_pow, Finsupp.support_subset_singleton, Submodule.mem_span_set, Finsupp.filter_eq_zero_iff, MvPolynomial.dvd_X_mul_iff, PolynomialModule.zero_apply, MonomialOrder.degree_X_sub_C, Finsupp.curry_single, linearIndepOn_iff_disjoint, MvPolynomial.monomial_one_mul_cancel_left_iff, Finsupp.mapRange.linearMap_apply, MvPolynomial.eq_zero_iff, Module.Basis.sumQuot_repr_inl_of_mem, Finsupp.mapRange.linearEquiv_symm, MvPolynomial.aevalTower_C, Module.End.ringEquivEndFinsupp_apply_apply_apply, Submodule.set_smul_eq_map, MvPolynomial.expand_one_apply, MvPowerSeries.coeff_truncFinset_mul_truncFinset_eq_coeff_mul, MvPolynomial.coe_basisMonomials, Nat.exponent_eq_exponent_mul_factorization_of_prime_pow_eq_base_pow, Finsupp.lcongr_symm, MvPolynomial.map_expand_pow_char, xInTermsOfW_aux, Finsupp.sumFinsuppEquivProdFinsupp_symm_inr, TensorProduct.finsuppScalarRight_apply_tmul_apply, Algebra.Presentation.span_range_relation_eq_ker, MonomialOrder.degree_mul_lt_iff_left_lt_of_ne_zero, Finsupp.coe_curryAddEquiv, MvPolynomial.mapRange_eq_map, Finset.mem_sup_support_iff, MvPolynomial.monomial_mem_pow_idealOfVars_iff, Finsupp.infinite_of_left, AddMonoidAlgebra.mul_single_zero_apply, Module.Basis.repr_symm_single, Representation.finsuppToCoinvariants_single_mk, groupHomology.H2π_comp_map_assoc, apply_eq_dotProduct_toMatrix₂_mulVec, MonoidAlgebra.ofCoeff_finsuppSum, MonomialOrder.degree_smul_le, TensorProduct.finsuppLeft_apply, MvPolynomial.irreducible_sumSMulX, factorization_zero, AnalyticOnNhd.aeval_mvPolynomial, Subgroup.mem_closure_range_iff, Finsupp.support_ceilDiv_subset, MvPolynomial.totalDegree_eq_zero_iff_eq_C, finsuppTensorFinsuppRid_symm_single_smul, MvPowerSeries.coeff_expand_smul, finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply, MonoidAlgebra.ofCoeff_eq_zero, Representation.LinearizeMonoidal.η_toLinearMap, Algebra.Generators.Hom.toAlgHom_X, Finsupp.uncurry_single, MvPolynomial.weightedTotalDegree_eq_zero_iff, MvPolynomial.bind₁_rename, TensorProduct.exists_finsupp_left, MvPolynomial.degreeOf_sub_le, AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly_assoc, MvPolynomial.degreeOf_mul_X_eq_degreeOf_add_one_iff, wittStructureRat_prop, Finsupp.inf_apply, Nat.Partition.toFinsuppAntidiag_injective, Module.Basis.restrictScalars_repr_apply, WeierstrassCurve.Projective.eval_polynomialX_of_Z_ne_zero, Orthonormal.inner_finsupp_eq_sum_right, MvPolynomial.degrees_rename, AddMonoidAlgebra.mapAddEquiv_apply, MvPolynomial.vars_neg, Algebra.Presentation.comp_relation, MvPolynomial.eval₂Hom_zero', Representation.finsupp_single, Polynomial.Bivariate.equivMvPolynomial_symm_C, Algebra.Generators.instIsScalarTowerRing, MvPowerSeries.aeval_coe, Finsupp.span_eq_range_linearCombination, Module.Basis.equivFunL_apply, Nat.factorization_centralBinom_eq_zero_of_two_mul_lt, Finsupp.prod_eq_zero_iff, MvPowerSeries.truncFinset_monomial_eq_zero, MonomialOrder.toSyn_degree_mul_le, Finsupp.isCompl_range_lmapDomain_span, Polynomial.homogenize_X_pow, WittVector.IsPoly.poly, MvPolynomial.map_hsymm, Finsupp.mapRange.addEquiv_symm, Squarefree.natFactorization_le_one, MvPolynomial.monomial_le_degreeOf, MvPowerSeries.eval₂_eq_tsum, Finsupp.instSMulPosMono, Algebra.Generators.cotangentRestrict_bijective_of_isCompl, MvPolynomial.combinatorial_nullstellensatz_exists_linearCombination, MvPolynomial.finite_universalFactorizationMap, Module.Relations.map_single, Module.presentationFinsupp_R, MvPolynomial.rTensorAlgHom_toLinearMap, groupHomology.d₁₀ArrowIso_inv_right, wittStructureRat_rec, Finsupp.mapDomain_zero, WittVector.mul_polyOfInterest_vars, Finsupp.single_left_injective, Nat.divisors_eq_map_attach_Iic_factorization_prod_pow, MvPolynomial.isRegular_prod_X, MonoidAlgebra.mapRangeAddEquiv_apply, MvPolynomial.homogeneousSubmodule_zero, MvPolynomial.coeff_sumSMulX, Finsupp.single_mul, MvPolynomial.expand_eq_C, Finsupp.multinomial_eq_of_support_subset, Finsupp.coe_strictMono, MvPowerSeries.le_weightedOrder_subst, algebraicIndependent_iff, Finsupp.mapDomainEmbedding_apply, MvPowerSeries.trunc'_expand, MvPolynomial.universalFactorizationMapPresentation_map, Finsupp.linearCombinationOn_range, MvPolynomial.coeff_rename_mapDomain, Nat.factorization_choose_of_lt_three_mul, Algebra.TensorProduct.basisAux_tmul, Finsupp.multinomial_update, MvPowerSeries.monomial_zero_eq_C_apply, MonomialOrder.degree_mul_le, AddSubgroup.mem_closure_range_iff, Module.Basis.singleton_repr, MvPolynomial.restrictSupport_mono, KaehlerDifferential.derivationQuotKerTotal_apply, Finsupp.count_toMultiset, MonoidAlgebra.coe_add, MvPolynomial.algebraTensorAlgEquiv_symm_X, Finsupp.neLocus_add_right, MvPolynomial.expand_injective, Finsupp.linearIndependent_single_of_ne_zero, MvPolynomial.mem_restrictDegree, MvPolynomial.support_coeff_finSuccEquiv, LinearMap.hasEigenvalue_adjoint_comp_self_sq_singularValues, MonomialOrder.monic_monomial, Algebra.Presentation.aeval_val_relation, LinearMap.polyCharpolyAux_map_eq_charpoly, MvPolynomial.totalDegree_neg, MvPolynomial.expand_one, Finsupp.sum_add_index_of_disjoint, FreeAbelianGroup.toFinsupp_of, MvPolynomial.degrees_map_le, MvPolynomial.esymmAlgHom_fin_surjective, MvPolynomial.expand_inj, LinearMap.polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff, MvPolynomial.coeff_prod_X_pow, MvPolynomial.support_neg, CommRingCat.HomTopology.mvPolynomialHomeomorph_symm_apply_hom, MvPolynomial.supDegree_esymm, Nat.factorization_lt, LinearMap.toMatrix_transpose_apply, MvPolynomial.indicator_mem_restrictDegree, MvPolynomial.coeffsIn_mul, Pi.basis_repr, Nat.ordCompl_pow_mul_of_not_dvd, AlgebraicGeometry.AffineSpace.map_toSpecMvPoly, Finsupp.cons_tail, Finsupp.erase_neg, Finsupp.mapRange_injective, MvPolynomial.eval_eq, MvPowerSeries.rename_coe, MonoidAlgebra.mul_apply_mul_eq_mul_of_uniqueMul, groupHomology.d₁₀_comp_coinvariantsMk, MonomialOrder.sPolynomial_def, groupHomology.d₂₁_comp_d₁₀_apply, Nat.not_dvd_ordCompl, MvPolynomial.mk_eq_eval₂, MonomialOrder.sPolynomial_antisymm, Algebra.Generators.H1Cotangent.δAux_ofComp, MvPolynomial.restrictSupport_zero, groupHomology.mapCycles₂_comp_apply, Module.Relations.Quotient.linearMap_ext_iff, Module.Presentation.ofExact_relation, Nat.factorization_lcm, LinearIndependent.span_repr_eq, MvPolynomial.killCompl_monomial_mapDomain, MonomialOrder.mem_nonZeroDivisors_of_leadingCoeff_mem_nonZeroDivisors, sigmaFinsuppEquivDFinsupp_smul, MonomialOrder.le_add_right, MvPolynomial.as_sum, Finsupp.sumElim_zero_single, MonomialOrder.degree_mul_of_left_mem_nonZeroDivisors, Finsupp.cons_right_injective, MvPolynomial.isUnit_iff_eq_C_of_isReduced, MonomialOrder.leadingCoeff_monomial, Algebra.Presentation.differentials.comm₂₃', MvPolynomial.psum_zero, Finsupp.equivMapDomain_trans', InnerProductSpace.gramSchmidt_triangular, MvPolynomial.monomial_add_single, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none, QuadraticAlgebra.basis_repr_apply, Finsupp.embSigma_injective, MvPolynomial.le_coeffsIn_pow, Finsupp.instPosSMulStrictMono, MvPolynomial.supported_strictMono, PowerBasis.repr_mul_isIntegral, MvPolynomial.IsWeightedHomogeneous.pow, MonomialOrder.degree_pow_le, MvPolynomial.eval_add, WeierstrassCurve.Projective.map_polynomialX, MvPolynomial.pointToPoint_zeroLocus_le, Module.Basis.toDual_eq_repr, Algebra.SubmersivePresentation.map_jacobianRelationsOfHasCoeffs, Finsupp.prod_hom_add_index, Finsupp.smul_single', exists_integral_inj_algHom_of_quotient, MvPowerSeries.trunc_map, Finsupp.weight_single_index, Finsupp.single_le_single, Finsupp.domCongr_symm, MvPolynomial.isNilpotent_iff, Module.Basis.sum_repr_mul_repr, Finsupp.addCommute_of_disjoint, Finsupp.linearCombination_apply, Finsupp.prod_filter_index, Nat.factorization_ceilRoot, Subalgebra.LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent, Finsupp.update_eq_single_add_erase, MvPolynomial.instNoZeroDivisors, NumberField.integralBasis_repr_apply, exists_finite_inj_algHom_of_fg, MvPolynomial.eval₂_eq', groupHomology.H2π_eq_iff, MonomialOrder.monic_monomial_one, Submodule.mulRightMap_eq_mulMap_comp, MvPolynomial.zeroLocus_bot, Finsupp.wellFoundedLT', WeierstrassCurve.Jacobian.baseChange_polynomial, MvPolynomial.aeval_def, Finsupp.mapDomain_apply_eq_sum, Finsupp.fst_sumFinsuppEquivProdFinsupp, Module.Basis.linearMap_repr_apply, MvPolynomial.monomial_eq_zero, AddMonoidAlgebra.coeffLinearEquiv_apply, Finsupp.isPWO, groupHomology.H1AddEquivOfIsTrivial_single, MvPolynomial.eval_monomial, Finsupp.degree_preimage_add, Finsupp.split_embSigma_of_ne, Relation.cutExpand_le_invImage_lex, MultilinearMap.freeFinsuppEquiv_def, MonomialOrder.degree_C, Finsupp.single_mono, Finsupp.liftAddHom_apply, MvPolynomial.coeff_monomial_mul', groupHomology.range_d₁₀_eq_coinvariantsKer, Finsupp.smul_apply, MvPolynomial.monomial_mem_coeffsIn, MonomialOrder.toSyn_monotone, MvPolynomial.degrees_sub_le, ArithmeticFunction.sigma_eq_prod_primeFactors_sum_range_factorization_pow_mul, MvPolynomial.coe_eval₂Hom, MvPowerSeries.coeff_trunc', Finsupp.Colex.le_iff_of_unique, MvPolynomial.vars_C_mul, Finsupp.Lex.le_iff_of_unique, Finsupp.coe_update, MvPolynomial.coeff_zero_X, MonomialOrder.sPolynomial_left_zero, AbsoluteValue.eval_mvPolynomial_le, MvPowerSeries.coeff_zero_mul_X, groupHomology.isoCycles₂_hom_comp_i_apply, Algebra.Generators.toAlgHom_ofComp_rename, MonomialOrder.support_leadingTerm, Finsupp.linearCombination_embDomain, Algebra.FinitePresentation.iff, DividedPowerAlgebra.dp_zero, wittStructureRat_rec_aux, Polynomial.Bivariate.equivMvPolynomial_symm_X_1, MvPolynomial.eval₂_add, MonomialOrder.image_leadingTerm_insert_zero, WeierstrassCurve.Projective.eval_polynomialZ, LinearMap.splittingOfFinsuppSurjective_injective, MvPowerSeries.coeff_inv_aux, MvPolynomial.supported_mono, Algebra.Generators.ker_localizationAway, Finsupp.erase_zero, MonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_support_val, Finsupp.DegLex.lt_iff, MonomialOrder.sPolynomial_decomposition, MonomialOrder.degLex_single_le_iff, MvPolynomial.constantCoeff_smul, MvPolynomial.totalDegree_expand, MvPolynomial.algHom_C, MvPolynomial.leadingCoeff_toLex_C, MvPolynomial.support_mul_X, Submodule.range_lsum_smul, Finsupp.comapDomain_apply, Representation.LinearizeMonoidal.assoc_comp_δ, wittStructureInt_prop, SkewMonoidAlgebra.toFinsuppAddEquiv_symm_apply, MvPowerSeries.coeff_weightedHomogeneousComponent, Finsupp.support_eq_singleton, MvPolynomial.eval_pow, Finsupp.single_nonpos, MvPowerSeries.order_le, Finsupp.mul_apply, Representation.ofMulActionSelfAsModuleEquiv_apply, Finsupp.mapDomain_apply, MvPolynomial.eval₂Hom_zero'_apply, KaehlerDifferential.kerTotal_map, MvPowerSeries.lexOrder_zero, MvPolynomial.psumPart_zero, QuadraticMap.map_finsuppSum', groupHomology.eq_d₂₁_comp_inv_assoc, Finsupp.degLex_def, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, Ordinal.CNF.eval_add, Finsupp.univ_sum_single_apply, SkewMonoidAlgebra.toFinsupp_injective, PiTensorProduct.ofFinsuppEquiv_apply, Finsupp.equivFunOnFinite_symm_coe, MvPolynomial.le_zeroLocus_iff_le_vanishingIdeal, Finsupp.mapRange.addMonoidHom_comp, MvPolynomial.support_esymm', TensorProduct.finsuppScalarRight_symm_apply_single, List.toFinsupp_concat_eq_toFinsupp_add_single, Finsupp.lt_def, Equiv.finsuppUnique_symm_apply_apply, groupHomology.cyclesMap_comp_isoCycles₂_hom_assoc, Module.Basis.mem_span_image, Finsupp.mapRange_add', Representation.linearizeOfMulActionIso_apply, LinearMap.CompatibleSMul.finsupp_cod, Finsupp.sumFinsuppAddEquivProdFinsupp_apply, MonomialOrder.leadingCoeff_mul_of_left_mem_nonZeroDivisors, MvPolynomial.mkₐ_eq_aeval, Finset.mapRange_finsuppAntidiag_subset, MvPolynomial.derivation_C, NumberField.mixedEmbedding.stdBasis_apply_isComplex_fst, MvPolynomial.mem_support_coeff_optionEquivLeft, Algebra.Presentation.fg_ker, Height.mulHeight_eval_ge, Finsupp.lex_lt_iff_of_unique, Module.Basis.localizationLocalization_repr_algebraMap, instIsAlgebraicMvPolynomialOfNoZeroDivisors, Polynomial.eval_X_toTupleMvPolynomial_zero_eq, groupHomology.inhomogeneousChains.d_single, MonoidAlgebra.coeff_injective, MvPolynomial.dvd_smul_X_iff_exists, Module.Basis.dualBasis_apply, Algebra.Generators.σ_smul, MvPowerSeries.coeff_trunc, MvPolynomial.mem_supported_vars, apply_eq_star_dotProduct_toMatrix₂_mulVec, MvPolynomial.mkDerivation_monomial, MvPolynomial.degrees_sum_le, Complex.coe_basisOneI_repr, Finsupp.linearCombination_single, Module.Presentation.CokernelData.π_lift, Finsupp.embDomain_apply_self, Finsupp.equivMapDomain_zero, Algebra.Presentation.relation_mem_ker, Algebra.Generators.Hom.toExtensionHom_toRingHom, Finsupp.ofSupportFinite_fin_two_eq, MvPolynomial.schwartz_zippel_sup_sum, PolynomialModule.smul_apply, Module.Basis.reindexFinsetRange_repr_self, AddMonoidAlgebra.mul_apply_left, Algebra.Generators.comp_localizationAway_ker, MvPolynomial.mem_map_C_iff, MvPolynomial.rename_monomial, MvPolynomial.aeval_toMvPolynomial, Finsupp.orderEmbeddingToFun_apply, MvPolynomial.mul_esymm_eq_sum, MvPolynomial.prime_C_iff, Finsupp.single_tsub, MvPolynomial.eval_mul, SkewMonoidAlgebra.toFinsupp_neg, MvPolynomial.restrictScalars_restrictSupportIdeal, MvPolynomial.instFiniteSubtypeMemSubmoduleRestrictDegreeOfFinite, Orthonormal.inner_right_finsupp, LinearMap.toMatrix_transpose_apply', Finsupp.piecewise_apply, Finsupp.degree_comapDomain_le_of_canonicallyOrderedAdd, MvPolynomial.mem_restrictSupport_iff, Module.Basis.repr_symm_single_one, MvPolynomial.degreesLE_zero, groupHomology.isBoundary₂_iff, MvPolynomial.universalFactorizationMapPresentation_relation, HahnSeries.coeff_ofFinsupp, MonoidAlgebra.mapAlgHom_apply, MvPolynomial.aevalTower_comp_algebraMap, Finsupp.coe_onFinset, MvPolynomial.monic_esymm, MonoidAlgebra.ofCoeff_neg, Finsupp.embDomain_lt_embDomain_iff_lt, MvPolynomial.eval₂_zero_apply, Algebra.PreSubmersivePresentation.aevalDifferential_single, MvPolynomial.isWeightedHomogeneous_monomial, AlgebraicIndependent.algebraMap_aevalEquiv, MvPolynomial.isWeightedHomogeneous_zero, MonomialOrder.coeff_degree_eq_zero_iff, Ordinal.CNF.coeff_of_notMem_CNF, MvPolynomial.aeval_id_rename, Finsupp.sum_nsmul, Finsupp.toMultiset_add, Nat.primeFactorsList_count_eq, Multiset.toFinsupp_singleton, Representation.LinearizeMonoidal.rTensor_comp_δ, Finsupp.coe_basis, MvPolynomial.degreeOf_mul_X_self, MonomialOrder.monic_C_one, MvPolynomial.eq_C_of_isEmpty, Finsupp.mapRange.linearEquiv_toLinearMap, MvPolynomial.coeff_one, MonomialOrder.sPolynomial_right_zero, AddMonoidAlgebra.mapAlgHom_apply, Submodule.smul_top_eq_range_lsum, LinearMap.toMatrix_smulRight, Finsupp.single_apply_eq_zero, Module.Relations.solutionFinsupp_var, Finsupp.subtypeDomain_apply, WeierstrassCurve.Projective.polynomialX_eq, Algebra.adjoin_range_eq_range_aeval, Prime.dvd_finsuppProd_iff, Multiset.toFinsupp_symm_apply, MvPolynomial.monomial_zero', Nat.setOf_pow_dvd_eq_Icc_factorization, Polynomial.homogenize_finsetSum, FreeAbelianGroup.equivFinsupp_apply, MvPolynomial.eval₂_sub, Finsupp.sumFinsuppEquivProdFinsupp_symm_apply, Finsupp.counit_single, MvPolynomial.weightedHomogeneousComponent_directSum, SkewMonoidAlgebra.toFinsupp_zero, NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul, Algebra.Generators.aeval_val_σ, MvPolynomial.msymm_zero, Finsupp.lex_lt_of_lt, MvPolynomial.totalDegree_add, RootPairing.Base.toCoweightBasis_repr_coroot, Polynomial.homogenize_C_mul, Finsupp.single_swap, AdjoinRoot.powerBasisAux'_repr_symm_apply, MvPowerSeries.coeff_prod, groupHomology.mapCycles₂_id_comp_assoc, MvPowerSeries.exists_coeff_ne_zero_and_order, Finsupp.coe_finset_sum, groupHomology.π_comp_H1Iso_hom_apply, MvPolynomial.mem_zeroLocus_iff, Representation.freeLift_toLinearMap, Nat.factorization_choose', MvPowerSeries.truncFinset_monomial, Finsupp.restrictDom_comp_subtype, AddMonoidAlgebra.coeff_smul, Finsupp.lsum_apply, groupHomology.single_isCycle₂_iff, MvPolynomial.coe_add, Finsupp.filter_single_of_neg, Basis.multilinearMap_apply_apply, Finsupp.neLocus_zero_right, MvPolynomial.totalDegree_coeff_optionEquivLeft_add_le, Nat.factorization_choose_le_log, MvPolynomial.modMonomial_X, MvPolynomial.homogeneousComponent_apply, Nat.factorization_eq_zero_of_not_prime, Rep.standardComplex.d_of, MvPolynomial.vars_prod, MonomialOrder.leadingCoeff_add_of_lt, MvPolynomial.eval_indicator_apply_eq_zero, Module.Basis.coe_finTwoProd_repr, MvPolynomial.sumToIter_iterToSum, Representation.LinearizeMonoidal.μ_comp_lTensor, MvPolynomial.divMonomial_mul_monomial, MvPolynomial.map_surjective_iff, AlgebraicIndependent.eq_zero_of_aeval_eq_zero, constantCoeff_wittPolynomial, Finsupp.linearCombination_unique, WeierstrassCurve.Projective.polynomialY_eq, MvPolynomial.aeval_eq_constantCoeff_of_vars, groupHomology.toCycles_comp_isoCycles₂_hom, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul, SkewMonoidAlgebra.ofFinsupp_neg, Finsupp.coe_lsum, MvPolynomial.weightedHomogeneousComponent_finsupp, Finsupp.isCentralScalar, Finsupp.neLocus_sub_left, WeierstrassCurve.Projective.negDblY_eq, Finsupp.sum_uncurry_index', groupHomology.cyclesMap_comp_isoCycles₂_hom_apply, Finsupp.linearCombination_mapDomain, Span.finsupp_linearCombination_repr, SymmetricAlgebra.equivMvPolynomial_symm_X, MvPolynomial.coeff_linearCombination_X_pow, MvPolynomial.expand_bind₁, MvPolynomial.map_injective_iff, groupHomology.mapCycles₁_id_comp, MvPolynomial.linearIndependent_X, MvPolynomial.coeff_mul_X', PolynomialModule.smul_single_apply, Finset.finsuppAntidiag_mono, MvPolynomial.prod_X_pow_eq_monomial, List.support_sum_eq, Finsupp.lapply_comp_lsingle_same, MvPolynomial.map_injective, MonoidAlgebra.mapRingEquiv_apply, Finsupp.instIsCocomm, MvPolynomial.constantCoeff_monomial, MvPolynomial.coeff_mul_X, Representation.LinearizeMonoidal.rightUnitor_δ, MvPolynomial.smul_eval, Finsupp.multinomial_eq, MvPolynomial.eval₂Hom_zero, MvPowerSeries.substAlgHom_coe, LinearMap.singularValues_pos_iff_lt_finrank_range, Finsupp.mapRange_surjective, MvPolynomial.universalFactorizationMapPresentation_algebra_algebraMap, MvPolynomial.degrees_one, Finsupp.instIsCancelAdd, MvPolynomial.C_eq_zero, MonoidAlgebra.mapRangeRingEquiv_apply, MvPolynomial.supDegree_toLex_C, WeierstrassCurve.Projective.eval_polynomialY_of_Z_ne_zero, MvPolynomial.coeff_rTensorAlgHom_tmul, MvPolynomial.aeval_zero, Cardinal.mk_finsupp_of_fintype, Module.Presentation.finsupp_relation, MvPolynomial.killCompl_rename_app, IsAdjoinRootMonic.coeff_apply_lt, Nat.Icc_factorization_eq_pow_dvd, Nat.factorization_le_iff_dvd, Finsupp.neLocus_self_sub_left, List.mem_foldr_sup_support_iff, Finsupp.mem_rangeIcc_apply_iff, MvPolynomial.mem_weightedHomogeneousSubmodule, Representation.apply_eq_of_leftRegular_eq_of_generator, MvPolynomial.hom_congr_vars, Nat.ordCompl_pos, MvPolynomial.comp_aeval, DirectSum.IsInternal.collectedBasis_repr_of_mem_ne, MvPolynomial.support_map_of_injective, MvPolynomial.constantCoeff_X, MvPolynomial.divMonomial_monomial, MvPolynomial.frobenius_zmod, Module.Basis.toMatrix_apply, KaehlerDifferential.mvPolynomialBasis_repr_apply, WittVector.frobeniusPolyAux_eq, LinearMap.exists_finsupp_nat_of_prod_injective, MvPolynomial.optionEquivLeft_coeff_some_coeff_none, MvPowerSeries.coeff_zero_one, Finsupp.sigmaFinsuppLEquivPiFinsupp_apply, IntermediateField.mem_adjoin_range_iff, groupHomology.eq_d₁₀_comp_inv, Nat.ordCompl_mul, DividedPowerAlgebra.mkAlgHom_surjective, Finsupp.sum_curry_index, finsuppTensorFinsuppRid_single_tmul_single, WittVector.coeff_frobeniusFun, LinearIndependent.linearCombinationEquiv_symm_apply, Nat.ordProj_le, MvPolynomial.renameEquiv_refl, Module.DualBases.basis_repr_apply, MvPolynomial.totalDegree_renameEquiv, LieAlgebra.LoopAlgebra.toFinsupp_single_tmul, Algebra.toMatrix_lmul', Nat.dvd_iff_exists_le_factorization, LinearMap.singularValues_fin, AddMonoidAlgebra.ofCoeff_zero, LinearMap.sq_singularValues_of_lt, MvPolynomial.expand_mul, MvPolynomial.mem_coeffsIn, Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul, AddMonoidAlgebra.single_mul_apply, groupHomology.isoShortComplexH1_inv, Representation.LinearizeMonoidal.η_single, AlgebraicGeometry.AffineSpace.map_SpecMap, WeierstrassCurve.Projective.baseChange_polynomialX, Module.Relations.Solution.isPresentation_iff, Nat.factorization_le_factorization_choose_add, Module.DualBases.dual_lc, MvPolynomial.isLocalHom_expand, MvPolynomial.exists_mem_support_not_dvd_of_forall_totalDegree_le, Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, MvPolynomial.weightedHomogeneousComponent_of_isWeightedHomogeneous_ne, Polynomial.derivativeFinsupp_map, groupHomology.eq_d₁₀_comp_inv_assoc, MvPolynomial.C_mul', AlgebraicClosure.le_maxIdeal, Finsupp.disjoint_supported_supported, MvPolynomial.isEmptyAlgEquiv_apply, MvPolynomial.bind₂_X_right, Finsupp.llift_symm_apply, Finsupp.Colex.lt_iff, MvPolynomial.of_irreducible_expand, TensorProduct.finsuppScalarLeft_apply_tmul_apply, AddMonoidAlgebra.modOf_apply_self_add, Algebra.Generators.cMulXSubOneCotangent_eq, DividedPowerAlgebra.submodule_span_prod_dp_eq_top, MvPolynomial.map_C, Finsupp.apply_single', MvPolynomial.isHomogeneous_monomial, groupHomology.chainsMap_f_1_comp_chainsIso₁_assoc, Finsupp.equivMapDomain_symm_apply, SkewMonoidAlgebra.ofFinsupp_add, LinearMap.polyCharpolyAux_baseChange, MonoidAlgebra.smul_apply, Finsupp.prod_pow, Polynomial.Bivariate.equivMvPolynomial_X, Finsupp.sum_antidiagonal_swap, groupHomology.isoCycles₁_hom_comp_i_apply, AddMonoidAlgebra.supported_eq_map, MvPolynomial.C_dvd_iff_dvd_coeff, Finsupp.mk_mem_graph, Finsupp.coe_add, Finsupp.nsmul_apply, MvPolynomial.pderiv_C_mul, Polynomial.homogenize_finsetProd, Nat.card_divisors, Module.Basis.symmetricAlgebra_repr_apply, AddMonoidAlgebra.mapRingEquiv_apply, Finsupp.comapSMul_def, MonomialOrder.degree_smul_of_isRegular, Finsupp.supportedEquivFinsupp_symm_apply_coe_support_val, AlgebraicClosure.toSplittingField_coeff, ZLattice.exists_forall_abs_repr_le_norm, groupHomology.lsingle_comp_chainsMap_f, MvPolynomial.eval₂_mul, Matrix.toMvPolynomial_eval_eq_apply, groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply, Nat.Prime.factorization_self, MvPolynomial.coe_pow, MvPowerSeries.coeff_add_mul_monomial, AddMonoidAlgebra.single_mul_apply_of_not_exists_add, Finsupp.sumElim_single_single, MonomialOrder.degree_one, MvPolynomial.natDegree_optionEquivLeft, Matrix.charpoly.univ_coeff_isHomogeneous, MvPolynomial.isHomogeneous_one, Finsupp.card_pi, ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial, Matrix.toLin_apply, WittVector.constantCoeff_wittMul, Representation.finsuppTensorRight_symm_apply_single, not_linearIndependent_iff_finsupp, MvPolynomial.totalDegree_eq_zero_iff, Finsupp.mapDomain_finset_sum, MvPowerSeries.monomial_pow, AlgebraicGeometry.AffineSpace.SpecIso_inv_over_assoc, Algebra.Generators.self_algebra_smul, MultilinearMap.freeFinsuppEquiv_apply, AddMonoidAlgebra.apply_eq_zero_of_not_le_supDegree, Finsupp.filter_apply, Finsupp.linearCombination_range, Finsupp.mapRange_smul', Nat.ordProj_dvd_ordProj_of_dvd, MvPolynomial.decomposition.decompose'_apply, Finsupp.coe_smul, MvPolynomial.restrictSupport_nsmul, groupHomology.d₃₂_single_one_fst, Algebra.Generators.toKaehler_tmul_D, MvPolynomial.mem_support_finSuccEquiv, AddMonoidAlgebra.coeffAddEquiv_symm_apply, Finsupp.mem_support_multiset_sum, Submodule.mulRightMap_apply, MvPolynomial.psum_one, MvPolynomial.mem_degreesLE, MvPolynomial.weightedHomogeneousComponent_isWeightedHomogeneous, LinearMap.sq_singularValues_fin, Finsupp.comapSMul_apply, MvPolynomial.isNoetherianRing_fin, MvPolynomial.X_dvd_iff_modMonomial_eq_zero, Finsupp.coe_orderIsoMultiset_symm, MvPolynomial.funext_set_iff, finsuppLEquivDirectSum_single, MvPolynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing, Finsupp.some_single_none, groupHomology.d₂₁_comp_d₁₀, Orthonormal.inner_finsupp_eq_sum_left, Sylow.card_eq_multiplicity, MvPolynomial.X_mul_divMonomial, MvPolynomial.map_monomial, Finsupp.comul_single, MvPolynomial.monomial_mem_restrictSupport, algebraicIndependent_iff_injective_aeval, SkewMonoidAlgebra.toFinsupp_add, MvPolynomial.vars_map_of_injective, MvPolynomial.aeval_map_algebraMap, Algebra.Generators.Hom.toAlgHom_C, groupHomology.d₂₁_single_self_inv_ρ_sub_inv_self, Finsupp.subtypeDomain_eq_zero_iff', LinearIndependent.finsuppLinearCombination_injective, Representation.ker_leftRegular_norm_eq, Finsupp.lapply_apply, MvPowerSeries.coeff_zero_X_mul, MvPolynomial.rename_comp_toMvPolynomial, Height.mulHeightBound_eq, groupHomology.chainsMap_f_3_comp_chainsIso₃_assoc, groupHomology.single_ρ_self_add_single_inv_mem_boundaries₁, Finsupp.support_single_add_single_subset, groupHomology.H1ToTensorOfIsTrivial_H1π_single, MvPolynomial.comap_C_surjective, Finsupp.mapRange.linearMap_comp, MvPolynomial.finSuccEquiv_comp_C_eq_C, Finsupp.fst_sumFinsuppAddEquivProdFinsupp, MvPolynomial.esymmAlgHom_zero, MvPolynomial.homogeneousComponent_eq_zero, Nat.Iio_factorization_prod_pow_injective, Nat.factorization_centralBinom_of_two_mul_self_lt_three_mul, MvPolynomial.eval₂_eta, Finsupp.zero_apply, MvPolynomial.coeToMvPowerSeries.algHom_apply, Finsupp.DegLex.single_le_iff, MonoidAlgebra.coeffLinearEquiv_apply, MvPolynomial.degreeOf_eq_sup, AlgebraicIndependent.liftAlgHom_comp_reprField, Module.length_finsupp, AddMonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_support_val, DividedPowerAlgebra.algHom_ext_iff, Finsupp.support_floorDiv_subset, MvPolynomial.rename_rightInverse, char_dvd_card_solutions, Algebra.SubmersivePresentation.sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs, Finsupp.ofSupportFinite_coe, Finsupp.linearCombination_restrict, Algebra.Presentation.differentials.comm₁₂, WeierstrassCurve.Jacobian.polynomialZ_eq, Module.Basis.sumQuot_repr_inr_of_mem, Finsupp.wellQuasiOrderedLE, MonomialOrder.sPolynomial_monomial_mul, MvPolynomial.hsymmPart_zero, Module.IsLocalRing.linearCombination_bijective_of_flat, MvPolynomial.eval₂Hom_map_hom, Finsupp.coe_basisSingleOne, Finsupp.coe_lmapDomain, MvPolynomial.isRegular_X, MvPolynomial.mem_homogeneousSubmodule, Finsupp.mapRange_sub, MvPolynomial.finSuccEquiv_eq, Finsupp.indicator_eq_sum_attach_single, char_dvd_card_solutions_of_sum_lt, List.toFinsupp_apply_le, Finsupp.lapply_comp_lsingle_of_ne, SymmetricAlgebra.equivMvPolynomial_ι_apply, Nat.ordCompl_self_pow_mul, groupHomology.cyclesOfIsCycle₁_coe, Module.Basis.repr_injective, Finsupp.support_single_add, AddMonoidAlgebra.ofCoeff_add, RingHom.IsStandardSmooth.exists_etale_mvPolynomial, MonoidAlgebra.mul_single_apply_of_not_exists_mul, MvPolynomial.homogeneousComponent_zero, LinearIndependent.repr_range, LinearMap.polyCharpoly_eq_of_basis, MvPolynomial.ker_eval₂Hom_universalFactorizationMap, Finsupp.prod_neg_index, Module.Basis.repr_apply_eq, MvPolynomial.monomial_left_injective, Finsupp.addHom_ext'_iff, MvPolynomial.bind₁_comp_rename, MvPolynomial.coeff_map, MonomialOrder.degree_le_degree_of_support_subset, MvPolynomial.monomial_sum_index, groupHomology.inhomogeneousChains.ext_iff, Finsupp.linearCombination_comp, MonomialOrder.degree_eq_zero_iff_totalDegree_eq_zero, MvPolynomial.degrees_prod_le, exteriorPower.presentation_relation, LinearMap.polyCharpolyAux_map_aeval, Matrix.mvPolynomialX_mapMatrix_eval, MvPolynomial.monic_monomial_eq, Pi.counit_coe_finsupp, MvPolynomial.image_support_finSuccEquiv, MvPolynomial.support_nonempty, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply, MvPolynomial.pderiv_monomial_single, AddMonoidAlgebra.mul_single_apply_aux, MvPolynomial.degreeOf_prod_eq, groupHomology.d₂₁_apply_mem_cycles₁, MvPolynomial.eval₂_rename, AlgebraicIndependent.aeval_repr, MvPolynomial.support_expand, NumberField.inverse_basisMatrix_mulVec_eq_repr, Finsupp.range_linearCombination, Finsupp.toFreeAbelianGroup_toFinsupp, MonomialOrder.degree_eq_zero_iff, Finsupp.sum_update_add, MonomialOrder.degree_mem_support, MvPolynomial.add_divMonomial, Finsupp.Lex.addRightStrictMono, MvPolynomial.instFiniteSubtypeMemSubmoduleRestrictTotalDegreeOfFinite, Polynomial.Bivariate.equivMvPolynomial_C_X, Nat.factorization_one, Finsupp.supported_empty, MvPolynomial.IsSymmetric.rename, MvPolynomial.IsHomogeneous.aeval, Module.Relations.ker_toQuotient, MvPolynomial.isEmptyRingEquiv_symm_toRingHom, groupHomology.cyclesMap_comp_isoCycles₁_hom_apply, Finsupp.bilinearCombination_apply, groupHomology.toCycles_comp_isoCycles₂_hom_apply, MonomialOrder.leadingTerm_C, MvPolynomial.DirectSum.coeLinearMap_eq_finsum, Finsupp.coe_nsmul, Finsupp.embSigma_apply_of_ne, Finsupp.antidiagonal_zero, Finsupp.apply_linearCombination, WittVector.mul_polyOfInterest_aux1, Module.Relations.Solution.IsPresentation.surjective_π, Module.finite_finsupp_iff, Finsupp.erase_add_single, Finsupp.mapRange_eq_zero, MonoidAlgebra.mul_single_one_apply, MvPolynomial.support_monomial_subset, MvPolynomial.monomial_mul, MonomialOrder.toSyn_eq_zero_iff, Finsupp.toDFinsupp_smul, MvPolynomial.quotientEquivQuotientMvPolynomial_leftInverse, KaehlerDifferential.kerTotal_mkQ_single_mul, AddMonoidAlgebra.coeff_eq_zero, LaurentPolynomial.ext_iff, Finsupp.linearIndependent_single_iff, PointedCone.mem_span_set, MultilinearMap.freeFinsuppEquiv_single, TensorProduct.eq_repr_basis_left, MvPowerSeries.weightedOrder_eq_nat, Height.mulHeight_eval_le, MonoidAlgebra.coeff_finsuppSum, MvPowerSeries.totalDegree_trunc', groupHomology.eq_d₃₂_comp_inv_assoc, Module.Basis.end_repr_symm_apply, MvPowerSeries.expand_monomial, FirstOrder.Ring.MvPolynomialSupportLEEquiv_symm_apply_coeff, MvPolynomial.aeval_bind₂, MvPolynomial.rename_bind₁, InnerProductSpace.toMatrix_rankOne, MvPolynomial.support_X_pow, MvPolynomial.rTensor_symm_apply_single, finTwoArrowEquiv'_symm_apply, Finsupp.eq_zero_of_comapDomain_eq_zero, MvPolynomial.pderiv_X_of_ne, MvPolynomial.prod_X_add_C_coeff, MvPolynomial.renameSymmetricSubalgebra_symm_apply_coe, Finsupp.update_eq_sub_add_single, MvPolynomial.IsSymmetric.zero, Algebra.Generators.Hom.toAlgHom_comp_apply, MvPolynomial.degree_finSuccEquiv, Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, Finsupp.optionElim_zero, AddMonoidAlgebra.mul_apply_add_eq_mul_of_uniqueAdd, MvPolynomial.isNoetherianRing_fin_0, Representation.free_single_single, MvPolynomial.nonempty_support_optionEquivLeft, Finsupp.toDFinsupp_neg, MvPolynomial.pderiv_monomial, Finsupp.mapRange_zero, Finsupp.lcongr_symm_single, MvPolynomial.isRegular_X_pow, Module.Basis.apply_eq_iff, Finsupp.sum_uncurry_index, Module.Flat.iff_forall_exists_factorization, Finsupp.coe_sym2Mul, sigmaFinsuppLequivDFinsupp_symm_apply, sigmaFinsuppEquivDFinsupp_single, Nat.prod_pow_primeFactors_factorization, bind₁_rename_expand_wittPolynomial, Algebra.adjoin_eq_range, MvPolynomial.degrees_add_le, MvPolynomial.mapAlgEquiv_symm, Algebra.Generators.toComp_toAlgHom_monomial, Module.Relations.Solution.π_comp_map, MvPolynomial.counit_surjective, Finsupp.equivMapDomain_apply, MvPolynomial.rename_injective, Finsupp.domLCongr_symm, Multiset.toFinsupp_zero, MvPolynomial.isHomogeneous_zero, groupHomology.mem_cycles₁_of_mem_boundaries₁, MvPolynomial.degrees_mul_le, WeierstrassCurve.Projective.negDblY_eq', MvPolynomial.quotient_mk_comp_C_injective, MvPolynomial.monomial_mem_homogeneousSubmodule_pow_degree, MonomialOrder.leadingCoeff_neg, Algebra.SubmersivePresentation.aeval_jacobianOfHasCoeffs, Finsupp.single_add_erase, Multiset.toFinsupp_toMultiset, setBasisOfTopLeSpanOfCardEqFinrank_repr_apply, LinearMap.polyCharpolyAux_coeff_eval, MvPolynomial.esymmAlgHomMonomial_single_one, AlgebraicClosure.Monics.map_eq_prod, MvPolynomial.coe_smul, Cardinal.mk_finsupp_lift_of_fintype, MonomialOrder.degree_prod_le, MvPolynomial.totalDegree_add_eq_left_of_totalDegree_lt, MonoidAlgebra.supportedEquivFinsupp_apply_support_val, Finsupp.disjoint_lsingle_lsingle, Finsupp.coe_eq_zero, MvPolynomial.map_rightInverse, Finsupp.subset_support_tsub, MvPolynomial.finrank_eq_zero, MvPolynomial.dvd_monomial_mul_iff_exists, MvPolynomial.killCompl_map, MonomialOrder.span_leadingTerm_insert_zero, Algebra.FiniteType.iff_quotient_mvPolynomial, Finsupp.linearCombination_comp_addSingleEquiv, Finsupp.DegLex.isStrictOrder, Finsupp.rangeSingleton_apply, Matrix.toLinAlgEquiv_apply, Module.Basis.coe_ofRepr, Module.equiv_free_prod_directSum, AddMonoidAlgebra.opRingEquiv_apply, Finsupp.codisjoint_supported_supported_iff, Algebra.Generators.H1Cotangent.δAux_X, MonomialOrder.div_set, MvPolynomial.aeval_eq_bind₁, MvPolynomial.support_optionEquivLeft, MonoidAlgebra.ofCoeff_zero, Finsupp.single_add, TensorProduct.equivFinsuppOfBasisRight_apply, Submodule.mulLeftMap_eq_mulMap_comp, MvPolynomial.X_mul_modMonomial, Finset.sum_single_ite, MvPolynomial.degreeOf_pow_le, MvPolynomial.dvd_X_iff_exists, MvPowerSeries.WithPiTopology.hasSum_of_monomials_self, MvPolynomial.finSuccEquiv_X_succ, groupHomology.mapCycles₂_hom, MvPolynomial.aeval_ofNat, Finsupp.toDFinsupp_sub, MonomialOrder.degree_zero, groupHomology.isoCycles₂_inv_comp_iCycles_apply, Ordinal.CNF.coeff_zero_right, groupHomology.isoCycles₂_inv_comp_iCycles_assoc, Finsupp.support_smul, Algebra.Presentation.aeval_val_relationOfHasCoeffs, Finsupp.le_iff', KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination, Finsupp.instPosSMulMono, MvPolynomial.eval₂Hom_eq_zero, MvPolynomial.instCharP, Finsupp.embDomain_add, Nat.ordProj_self_pow, Finsupp.univ_sum_single, MvPolynomial.expand_comp_bind₁, MvPolynomial.mapAlgEquiv_trans, MonomialOrder.leadingCoeff_C, Finsupp.mapRange.linearMap_id, Algebra.SubmersivePresentation.aeval_invJacobianOfHasCoeffs, exists_ordCompl_eq_one_iff_isPrimePow, MvPolynomial.ker_mapAlgHom, Finsupp.degree_preimage_nsmul, Finsupp.eq_indicator_self_iff, Nat.factorization_le_factorization_mul_right, MvPolynomial.aeval_injective_iff_of_isEmpty, MvPolynomial.support_one, PowerSeries.coeff_prod, WittVector.constantCoeff_wittAdd, Finsupp.instIsScalarTowerForall, Finsupp.sum_eq_single, Algebra.Generators.ofComp_kerCompPreimage, MonoidAlgebra.coeffAddEquiv_symm_apply, MvPolynomial.X_mem_supported, Rep.indCoindIso_hom_hom_toLinearMap, MvPolynomial.coeff_zero, Finsupp.lcongr_single, Module.Flat.exists_factorization_of_apply_eq_zero_of_free, MvPowerSeries.exists_coeff_ne_zero_and_weightedOrder, Nat.prod_factorization_eq_prod_primeFactors, MvPolynomial.eval_sub, Nat.factorization_eq_zero_iff_remainder, MvPolynomial.mem_restrictDegree_iff_sup, Finsupp.Lex.addLeftStrictMono, MvPolynomial.esymmAlgHom_fin_injective, List.toFinsupp_apply_lt, Matrix.toLinearMap₂_apply, Finsupp.linearEquivFunOnFinite_apply, MvPolynomial.aeval_comp_bind₁, MvPolynomial.hsymm_one, LinearMap.singularValues_of_finrank_le, Nat.Prime.pow_dvd_iff_dvd_ordProj, MvPolynomial.weightedHomogeneousComponent_eq_zero_of_notMem, ZLattice.abs_repr_lt_of_norm_lt, Height.logHeight_eval_le, MonoidAlgebra.supportedEquivFinsupp_apply_apply, groupHomology.cyclesMk₂_eq, groupHomology.chainsMap_f_1_comp_chainsIso₁, Finsupp.optionElim_apply_some, Finsupp.embDomain_zero, Finsupp.prod_option_index, MvPolynomial.totalDegree_sub, LieAlgebra.LoopAlgebra.residuePairing_apply_apply, KaehlerDifferential.kerTotal_mkQ_single_smul, Polynomial.monic_freeMonic, MvPolynomial.rTensor_apply_monomial_tmul, MvPolynomial.IsWeightedHomogeneous.prod, Nat.ordCompl_div_pow_of_dvd, MvPolynomial.eval₂_const_pUnitAlgEquiv, Algebra.Generators.repr_CotangentSpaceMap, Module.Basis.dualBasis_repr, groupHomology.H1π_eq_zero_iff, DividedPowerAlgebra.dp_sum_smul, groupHomology.isoCycles₁_inv_comp_iCycles_assoc, Finsupp.sumFinsuppLEquivProdFinsupp_symm_inr, MonomialOrder.degLex_lt_iff, MvPolynomial.coeff_X', groupHomology.π_comp_H1Iso_hom_assoc, Pi.comul_coe_finsupp, Finsupp.sum_hom_add_index, MvPolynomial.pderiv_pow, groupHomology.chainsMap_f_2_comp_chainsIso₂, constantCoeff_wittStructureRat_zero, groupHomology.d₂₁_single_one_fst, WeierstrassCurve.Jacobian.map_polynomialZ, Finsupp.supported_mono, MonoidAlgebra.coeff_zero, MvPolynomial.aeval_esymm_eq_multiset_esymm, MvPolynomial.supported_le_supported_iff, MvPolynomial.totalDegree_zero, AddMonoidAlgebra.coeffLinearEquiv_symm_apply, MonomialOrder.coeff_pow_nsmul_degree, MvPolynomial.bind₂_C_right, groupHomology.H2π_comp_map, NumberField.mixedEmbedding.stdBasis_apply_isReal, Finsupp.coe_rangeIcc, Finsupp.add_closure_setOf_eq_single, Finsupp.mapRange.addEquiv_toAddMonoidHom, MvPowerSeries.algebraMap_apply', MvPolynomial.constantCoeff_eq, LinearMap.toMvPolynomial_constantCoeff, HahnSeries.coeff_toMvPowerSeries_symm, MonoidAlgebra.uniqueRingEquiv_symm_apply, WeierstrassCurve.Projective.map_polynomialZ, groupHomology.mem_cycles₂_of_mem_boundaries₂, MvPolynomial.eval_rename, Module.Basis.linearCombination_repr, MvPolynomial.mkDerivationₗ_C, union_support_maximal_linearIndependent_eq_range_basis, Representation.LinearizeMonoidal.leftUnitor_δ, MvPolynomial.vars_one, StandardEtalePresentation.toPresentation_σ', MvPolynomial.totalDegree_finsetSum_le, Module.FinitePresentation.out, Nat.factorization_eq_primeFactorsList_multiset, Representation.finsuppTensorLeft_symm_apply_single, Finsupp.mapRange.equiv_apply, PolynomialModule.lsingle_apply, MvPolynomial.isIntegral_iff_isIntegral_coeff, witt_structure_prop, Finsupp.lex_eq_invImage_dfinsupp_lex, MvPowerSeries.weightedOrder_le, Nat.factorization_floorRoot, Module.Basis.linearCombination_coord, MvPolynomial.map_surjective, Finsupp.sup_apply, Representation.FiniteCyclicGroup.coinvariantsKer_leftRegular_eq_ker, Finsupp.coe_floorDiv, Finsupp.cons_zero, MvPolynomial.degreeOf_one, MvPolynomial.coe_eval₂AlgHom, WittVector.constantCoeff_wittNSMul, MonoidAlgebra.mapAddEquiv_apply, LinearMap.toMvPolynomial_comp, Finsupp.addLeftReflectLE, MvPolynomial.eval₂Hom_eq_bind₂, Module.Basis.tensorAlgebra_repr_apply, Nat.floorRoot_def, MvPolynomial.IsHomogeneous.rename_isHomogeneous_iff, MvPolynomial.vars_bind₁, MonomialOrder.leadingCoeff_pow, WittVector.bind₁_verschiebungPoly_wittPolynomial, MvPolynomial.prod_C_add_X_eq_sum_esymm, Module.projective_def', Algebra.Presentation.instFinitePresentationModelOfHasCoeffsOfFinite, MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card, MvPolynomial.eval₂_map_comp_C, groupHomology.H1π_comp_map_assoc, MonomialOrder.degree_pow, MvPowerSeries.coeff_zero_C, MvPolynomial.support_smul_eq, TensorProduct.exists_finsupp_right, Representation.coinvariantsTprodLeftRegularLEquiv_symm_apply, MvPolynomial.optionEquivRight_apply, Module.Basis.equivFun_apply, MvPolynomial.finSuccEquiv_apply, Finsupp.add_sum_erase', Finsupp.sum_option_index_smul, Finset.finsuppAntidiag_empty_zero, TensorProduct.finsuppScalarLeft_apply_tmul, MvPowerSeries.coeff_monomial, groupHomology.instEpiModuleCatH1π, MvPolynomial.vanishingIdeal_empty, MvPowerSeries.coeff_C, MvPolynomial.C_eq_coe_nat, Finsupp.mapRange.zeroHom_comp, Module.Relations.directSum_relation, Module.Basis.mulOpposite_repr_eq, MvPolynomial.tensorEquivSum_X_tmul_X, Module.Basis.coe_repr_symm, Finsupp.coe_equivFunOnFinite_symm, Module.Basis.smulTower'_repr, Module.Relations.toQuotient_map_apply, LinearMap.snd_prodOfFinsuppNat, MvPolynomial.comp_aeval_apply, MvPolynomial.vars_mul, Algebra.Presentation.relation_comp_localizationAway_inl, MvPolynomial.bind₂_comp_bind₂, WittVector.coeff_select, AddMonoidAlgebra.uniqueRingEquiv_symm_apply, Finsupp.toFinset_toMultiset, Finsupp.apply_single, Finsupp.degree_single, MvPolynomial.aeval_unique, WeierstrassCurve.Jacobian.baseChange_polynomialX, MonoidAlgebra.mul_apply, Module.Presentation.tensor_relation, Finsupp.LinearEquiv.finsuppUnique_apply, linearIndependent_iff, Finsupp.applyAddHom_apply, Finsupp.single_eval_le_sum, DividedPowerAlgebra.dp_def, Finsupp.mapDomain_equiv_apply, MvPolynomial.coeff_rTensorAlgHom_monomial_tmul, Finsupp.linearCombination_fin_zero, MvPolynomial.bind₁_bind₁, MvPolynomial.support_sum_monomial_coeff, MvPolynomial.degreeOf_mul_C_le, MvPolynomial.mem_coeffsIn_iff_coeffs_subset, Module.Relations.Solution.π_relation, MvPolynomial.esymmAlgHomMonomial_add, Finsupp.wellFoundedLT, exteriorPower.basis_repr_apply, Finsupp.linearEquivFunOnFinite_symm_single, MvPolynomial.algebraTensorAlgEquiv_symm_map, LinearIndependent.repr_eq, Module.Basis.toMatrix_update, Finsupp.range_single_subset, PiLp.basis_toMatrix_basisFun_mul, MvPolynomial.coeff_sub, Finsupp.single_multiset_sum, MvPolynomial.rename_polynomial_aeval_X, groupHomology.single_one_snd_sub_single_one_snd_mem_boundaries₂, MvPolynomial.weightedDecomposition.decompose'_eq, MvPolynomial.degrees_mul_eq, MvPolynomial.coeff_expand_of_not_dvd, Finsupp.subtypeDomain_eq_iff_forall, Polynomial.toFinsupp_apply, Finsupp.linearCombination_equivMapDomain, Rep.linearization_map, MvPowerSeries.lexOrder_eq_top_iff_eq_zero, DividedPowerAlgebra.dp_sum, Algebra.Generators.Hom.equivAlgHom_symm_apply_val, Finsupp.comapDomain_smul, MvPolynomial.isHomogeneous_C_mul_X_pow, Finsupp.mapRange.equiv_trans, Finsupp.neg_apply, MvPolynomial.tensorEquivSum_C_tmul_one, Finsupp.le_weight_of_ne_zero, MvPolynomial.map_iterateFrobenius_expand, MvPolynomial.vars_pow, Finsupp.mapRange.linearEquiv_apply, Finset.finsuppAntidiag_empty, Finsupp.instSMulPosStrictMono, Multiset.support_sum_eq, groupHomology.instEpiModuleCatH2π, Finsupp.Lex.single_antitone, Polynomial.toMvPolynomial_X, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop, AddMonoidAlgebra.coeff_finsuppSum, Module.Basis.baseChange_repr_tmul, SkewMonoidAlgebra.coeff_ofFinsupp, MvPolynomial.hsymm_zero, List.support_sum_subset, AddTorsor.convexCombination_eq_affineCombination, MvPolynomial.sumAlgEquiv_apply, Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one, Finsupp.lex_le_iff_of_unique, ZSpan.repr_fract_apply, finsuppLEquivDirectSum_apply, Basis.mem_ideal_iff, Multiset.toFinsupp_eq_iff, Finsupp.mem_span_range_iff_exists_finsupp, Algebra.Generators.ker_comp_eq_sup, MvPolynomial.degreeOf_C_mul_le, Finsupp.instIsAddTorsionFree, Algebra.TensorProduct.basis_repr_symm_apply, Rep.indCoindIso_inv_hom_toLinearMap, algebraicIndependent_subtype, LinearMap.polyCharpoly_map_eq_charpoly, MonomialOrder.degree_add_eq_right_of_lt, MvPolynomial.coeffsIn_eq_span_monomial, MvPolynomial.sumToIter_Xr, LinearMap.polyCharpoly_monic, Orthonormal.inner_finsupp_eq_zero, Finsupp.filter_pos_add_filter_neg, Polynomial.natDegree_freeMonic, Algebra.Generators.ofComp_toAlgHom_monomial_sumElim, Submodule.mulLeftMap_apply_single, Finsupp.single_mem_span_single, KaehlerDifferential.quotKerTotalEquiv_symm_apply, Finsupp.mapDomain.addMonoidHom_apply, finsuppTensorFinsuppLid_apply_apply, MvPolynomial.exists_finset_rename₂, LaurentPolynomial.invert_apply, Representation.LinearizeMonoidal.η_ε, LinearIndependent.repr_ker, Matrix.charpoly.univ_natDegree, Representation.LinearizeMonoidal.lTensor_comp_δ, WeierstrassCurve.Projective.eval_polynomial_of_Z_ne_zero, MvPolynomial.algebraMap_eq, MvPolynomial.algebraicIndependent_X, Representation.leftRegularTensorTrivialIsoFree_apply_single_tmul_single, MvPolynomial.eval_toMvPolynomial, groupHomology.H1π_comp_map, groupHomology.chainsMap_f_hom, Algebra.Presentation.algebraTensorAlgEquiv_symm_relation, groupHomology.d₃₂_apply_mem_cycles₂, Algebra.Generators.aeval_val_eq_zero, MvPolynomial.coeffsIn_pow, MvPolynomial.sum_C, Finsupp.mapRange.linearMap_toAddMonoidHom, MvPolynomial.totalDegree_one, Finsupp.single_apply_mem, MvPolynomial.esymmAlgHom_apply, MvPolynomial.monomial_eq, QuaternionAlgebra.coe_basisOneIJK_repr, Representation.LinearizeMonoidal.δ_apply_single, MvPolynomial.homogeneousSubmodule_eq_finsupp_supported, MvPolynomial.aeval_eq_eval₂Hom, Nat.factorizationEquiv_symm_apply_coe, MonoidAlgebra.supported_eq_map, MvPolynomial.vars_C, MvPolynomial.rename_prod_mk_eval₂, Ideal.range_finsuppTotal, Nat.factorization_div, AlgebraicIndependent.aevalEquivField_apply_coe, MvPolynomial.IsSymmetric.smul, Finsupp.Lex.isOrderedCancelAddMonoid, MvPolynomial.aeval_C, MvPolynomial.support_map_subset, MonoidAlgebra.ofCoeff_sum, IsTranscendenceBasis.mvPolynomial, Nat.factorization_choose_eq_zero_of_lt, Finsupp.sum_smul_index_semilinearMap', groupHomology.boundariesOfIsBoundary₂_coe, centralBinom_factorization_small, MvPolynomial.toMvPowerSeries_pUnitAlgEquiv, MvPolynomial.transcendental_polynomial_aeval_X, Finsupp.Lex.wellFounded, MvPolynomial.pderiv_map, Finsupp.subtypeDomain_eq_zero_iff, groupHomology.cyclesMk₁_eq, finsuppLequivDFinsupp_apply_apply, Nat.prod_pow_factorization_choose, Finsupp.support_add, WeierstrassCurve.Jacobian.eval_polynomial, Finsupp.graph_zero, Finsupp.liftAddHom_singleAddHom, MvPowerSeries.coeff_invOfUnit, Finsupp.support_inf_union_support_sup, Representation.linearizeOfMulActionIso_symm_apply, Finsupp.hasFiniteSupport, MvPolynomial.aeval_comp_expand, Algebra.Generators.naive_σ, AlgebraicIndependent.aevalEquiv_apply_coe, MvPolynomial.esymm_eq_sum_monomial, Polynomial.homogenize_monomial_of_lt, AddEquiv.finsuppUnique_symm_apply_support_val, Finsupp.logHeight_eq_log_mulHeight, groupHomology.mapCycles₂_comp_i_assoc, WittVector.wittMul_zero, MvPolynomial.rename_C, Finsupp.toMultiset_sum, LinearMap.singularValues_finrank_range_self, MvPolynomial.HomogeneousSubmodule.gradedMonoid, Finsupp.uncurry_apply_pair, FirstOrder.realize_genericPolyMapSurjOnOfInjOn, MvPowerSeries.coeff_mul_eq_coeff_trunc'_mul_trunc', Nat.factorization_prime_le_iff_dvd, MvPolynomial.eval₂_mul_C, Finsupp.domLCongr_apply, MonomialOrder.degree_lt_of_left_ne_zero_of_degree_mul_lt, StandardEtalePresentation.aeval_val_equivMvPolynomial, Finsupp.coe_lt_coe, Nat.sum_divisors, Finsupp.prod_ite_eq, Finsupp.range_single_one, MvPolynomial.instFiniteOfIsEmpty, MvPolynomial.C_neg, MvPolynomial.weightedHomogeneousComponent_eq_zero, MvPolynomial.aevalTower_comp_toAlgHom, MvPolynomial.zeroLocus_vanishingIdeal_galoisConnection, Finsupp.extendDomain_toFun, MvPolynomial.coeToMvPowerSeries.ringHom_apply, MvPolynomial.restrictSupport_add, Rep.linearization_obj_V, Finset.card_finsuppAntidiag_nat_eq_multichoose, Finsupp.curryLinearEquiv_apply, MvPolynomial.eval₂_X_pow, MvPolynomial.zeroLocus_span, MvPolynomial.instIsCancelMulZeroOfIsCancelAdd, QuadraticMap.apply_linearCombination', Finset.support_sum_eq, MvPolynomial.coeffs_map, Finsupp.card_Iic, MvPolynomial.totalDegree_monomial_le, Nat.factorization_pow_self, MvPowerSeries.totalDegree_truncFinset, MvPolynomial.IsHomogeneous.rename_isHomogeneous, groupHomology.mapCycles₂_id_comp_apply, Representation.linearizeMap_single, WittVector.polyOfInterest_vars_eq, Finsupp.optionElim_apply_eq_elim, finsuppTensorFinsupp_symm_single, Finsupp.single_le_iff, WeierstrassCurve.Jacobian.map_polynomial, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom, Finsupp.linearCombination_linearCombination, MvPolynomial.mapEquiv_trans, MvPowerSeries.WithPiTopology.tendsto_trunc'_atTop, Module.Relations.Solution.IsPresentation.desc_comp_π, Finsupp.mapRange.zeroHom_apply, MvPolynomial.isNoetherianRing, MvPolynomial.constantCoeff_comp_C, Finsupp.Colex.addLeftMono, MvPolynomial.pderiv_inr_universalFactorizationMap_X, MvPolynomial.degrees_zero, MvPolynomial.IsHomogeneous.mul, MvPolynomial.sumAlgEquiv_symm_apply, AddMonoidAlgebra.coeffAddEquiv_apply, MvPolynomial.eval₂_comp, Finsupp.equivCongrLeft_symm, MvPolynomial.weightedHomogeneousComponent_C_mul, MonomialOrder.leadingCoeff_zero, MvPolynomial.eval₂_pUnitAlgEquiv_symm, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul, Nat.factorizationEquiv_apply, Finsupp.split_apply, Submonoid.mem_closure_range_iff, WeierstrassCurve.Jacobian.eval_polynomial_of_Z_ne_zero, MvPolynomial.dvd_C_iff_exists, Finsupp.lift_symm_apply, Algebra.Generators.ker_eq_ker_aeval_val, MvPolynomial.instIsPushout_1, MvPowerSeries.coeff_zero_X, AddMonoidAlgebra.coeff_injective, WittVector.wittNeg_zero, groupHomology.H2π_comp_map_apply, NumberField.mixedEmbedding.latticeBasis_repr_apply, Algebra.Generators.ker_ofAlgHom, Finsupp.card_Iio, MvPolynomial.mul_monomial_mem_coeffsIn, MvPolynomial.IsHomogeneous.sum, Finsupp.smul_eq, MvPolynomial.supported_empty, MvPolynomial.C_mem_pow_idealOfVars_iff, Module.Basis.ext_elem_iff, Finsupp.default_eq_zero, instIsAlgebraicMvPolynomialOfNoZeroDivisors_1, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, MvPolynomial.esymmPart_zero, Algebra.Generators.toExtension_algebra₁, Finsupp.distribMulActionHom_ext'_iff, KaehlerDifferential.mvPolynomialBasis_repr_D, Rep.η_def, MonomialOrder.sPolynomial_monomial_mul', HahnSeries.coeff_toMvPowerSeries, AddMonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_apply, Finsupp.restrictSupportEquiv_symm_single, Representation.LinearizeMonoidal.μ_toLinearMap, MonoidAlgebra.mapDomainRingEquiv_apply, MvPolynomial.pderiv_eq_zero_of_notMem_vars, WittVector.map_frobeniusPoly, Representation.LinearizeMonoidal.μ_leftUnitor, Finsupp.single_add_single_eq_single_add_single, Nat.factorization_eq_card_pow_dvd, Finsupp.prod_fintype, MvPolynomial.sum_eval_eq_zero, MvPolynomial.support_divMonomial, MvPolynomial.le_degrees_add_right, MvPolynomial.weightedTotalDegree'_zero, finsuppTensorFinsuppRid_apply_apply, Module.Basis.repr_sum_self, WittVector.constantCoeff_wittZSMul, WeierstrassCurve.Jacobian.polynomialX_eq, MvPolynomial.aeval_C_comp_left, MvPolynomial.transcendental_X, RootPairing.Base.toWeightBasis_repr_root, finsuppEquivDFinsupp_symm_apply, MvPolynomial.msymm_one, MvPolynomial.C_mul_X_pow_eq_monomial, MvPolynomial.totalDegree_mul, Finsupp.linearCombination_option, MonoidAlgebra.coeffAddEquiv_apply, Polynomial.derivativeFinsupp_one, Algebra.leftMulMatrix_mulVec_repr, MvPowerSeries.order_monomial, Ordinal.CNF.eval_zero_right, Rep.standardComplex.d_apply, factorization_eq_count, Finsupp.linearCombination_eq_fintype_linearCombination, Nat.factorization_factorial_mul_succ, MvPolynomial.weightedHomogeneousComponent_mem, Finsupp.mapRange_add, KaehlerDifferential.ker_map_of_surjective, Finsupp.basisSingleOne_repr, MvPolynomial.degrees_rename_of_injective, Finsupp.supportedEquivFinsupp_symm_apply_coe, PolynomialLaw.range_φ, MvPolynomial.coeff_add, Finsupp.mapDomain_apply_eq_zero_iff_of_subsingletonAddUnits, groupHomology.inhomogeneousChains.d_comp_d, MvPolynomial.psum_eq_mul_esymm_sub_sum, MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_weight, MvPolynomial.eval_C, MvPolynomial.IsWeightedHomogeneous.C_mul, Module.Basis.smulTower_repr_mk, Module.Basis.repr_support_subset_of_mem_span, MvPolynomial.mapAlgHom_apply, MvPolynomial.support_zero, Algebra.Generators.cotangentRestrict_mk, Nat.factorization_ordCompl, Finsupp.liftAddHom_apply_single, Finsupp.supportedEquivFinsupp_apply_support_val, MvPolynomial.optionEquivLeft_monomial, finsuppLequivDFinsupp_symm_apply, AddMonoidAlgebra.ofCoeff_sum, Finsupp.lsum_comp_lsingle, Finsupp.mapDomain.addMonoidHom_id, Finsupp.lex_lt_iff, Algebra.Generators.cotangentRestrict_bijective_of_basis_kaehlerDifferential, TensorProduct.finsuppRight_symm_apply_single, MvPolynomial.rename_eq_zero_iff_of_injective, Finsupp.degree_mapDomain_eq_of_subsingletonAddUnits, Polynomial.coeff_homogenize, Representation.diagonalOneEquivLeftRegular_symm_apply_single, Algebra.Generators.H1Cotangent.δ_eq_δAux, Finsupp.mul_prod_erase, Finsupp.DegLex.instIsOrderedCancelAddMonoidDegLexNat, Algebra.SubmersivePresentation.ofSubsingleton_algebra_smul, Module.Basis.linearMap_repr_symm_apply, MonomialOrder.leadingCoeff_mul_of_isRegular_left, Representation.finsuppTensorLeft_apply_tmul_apply, KaehlerDifferential.mvPolynomialBasis_repr_comp_D, LieAlgebra.rank_eq_natTrailingDegree, MonoidAlgebra.coeff_eq_zero, WittVector.bind₁_onePoly_wittPolynomial, map_wittPolynomial, MvPowerSeries.coeff_truncFinset_eq_zero, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, Derivation.mapCoeffs_apply, MvPolynomial.optionEquivLeft_symm_apply, MvPolynomial.exists_coeff_ne_zero, Finsupp.tsub_apply, Nat.factorizationEquiv_inv_apply, finsuppTensorFinsuppLid_single_tmul_single, Finsupp.embSigma_apply_self, Representation.LinearizeMonoidal.μ_rightUnitor, SkewMonoidAlgebra.ofFinsupp_sub, Finsupp.embDomain_notin_range, Finsupp.support_neg, MvPolynomial.isLocalization_C_mk', MvPolynomial.algebraTensorAlgEquiv_tmul, MvPolynomial.vars_map, groupHomology.isoCycles₁_hom_comp_i_assoc, MvPolynomial.mem_support_coeff_finSuccEquiv, Nat.factorization_eq_zero_iff', MvPolynomial.homogeneousSubmodule_one_eq_span_X, Algebra.Generators.aeval_val_σ', Finsupp.embDomain.addMonoidHom_apply, MvPolynomial.support_sub, WittVector.wittOne_zero_eq_one, MvPolynomial.eval₂Hom_id_X_eq_join₂, Algebra.Generators.Hom.toAlgHom_id, Algebra.Generators.Hom.comp_val, MvPolynomial.degreeOf_C_mul, AddMonoidAlgebra.ext_iff, isArtinian_finsupp, span_range_eq_top_iff_surjective_finsuppLinearCombination, MvPolynomial.instIsPushout, Finsupp.prod_sum_index, MvPolynomial.C_injective, Fintype.card_finsupp, Module.Relations.Solution.ofπ_var, MvPolynomial.C_mul, CommRingCat.HomTopology.mvPolynomialHomeomorph_apply_fst, sigmaFinsuppEquivDFinsupp_apply, Representation.LinearizeMonoidal.δ_μ, MvPolynomial.esymm_eq_multiset_esymm, MvPolynomial.comap_apply, LaurentPolynomial.support_C_mul_T_of_ne_zero, Finsupp.mapDomain_sum, Finsupp.single_apply, Finsupp.sumFinsuppEquivProdFinsupp_symm_inl, AlgebraicGeometry.AffineSpace.over_over, MvPolynomial.vars_rename, MvPolynomial.eval₂Hom_eq_constantCoeff_of_vars, Finsupp.lex_def, groupHomology.d₁₀_eq_zero_of_isTrivial, WittVector.bind₁_zero_wittPolynomial, Representation.leftRegular_norm_apply, Finsupp.weight_sub_single_add, IsTranscendenceBasis.mvPolynomial', Finsupp.supported_iUnion, MvPolynomial.totalDegree_finset_sum, Representation.coinvariantsToFinsupp_mk_single, Finsupp.single_add_apply, Module.Relations.Solution.fromQuotient_comp_toQuotient, MonomialOrder.lex_lt_iff, Module.Basis.SmithNormalForm.repr_comp_embedding_eq_smul, Nat.sub_one_mul_factorization_factorial, MvPowerSeries.aeval_eq_sum, Representation.ind_mk, Module.Basis.toDual_linearCombination_right, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp, MvPolynomial.support_esymm'', MvPolynomial.isLocalization, TensorProduct.finsuppLeft_apply_tmul, MvPolynomial.instExpChar, PiTensorProduct.ofFinsuppEquiv'_apply_apply, AddMonoidAlgebra.single_zero_mul_apply, MvPolynomial.divMonomial_monomial_mul, Finsupp.restrictSupportEquiv_apply, StandardEtalePresentation.toPresentation_val, Finsupp.smul_apply_addAction, groupHomology.d₂₁_single_one_snd, AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly, MonomialOrder.notMem_support_of_degree_lt, MvPolynomial.instIsCancelAddOfIsLeftCancelAdd, Nat.ordProj_dvd, LinearMap.toMatrix_toSpanSingleton, LinearMap.singularValues_pos_iff_ne_zero, MvPolynomial.divMonomial_zero, MonoidAlgebra.ext_iff, MvPolynomial.sum_monomial_eq, MvPolynomial.rename_comp_bind₁, Finsupp.curryEquiv_symm_apply, Finsupp.unique_ext_iff, linearDepOn_iffₛ, MvPolynomial.degrees_monomial_eq, MvPolynomial.zeroLocus_top, Finsupp.Lex.wellFounded_of_finite, MvPolynomial.aeval_id_eq_join₁, Finsupp.Icc_eq, Finsupp.addCommute_iff_inter, Ordinal.CNF.eval_single_add, MvPolynomial.rename_X, Representation.coinvariantsFinsuppLEquiv_symm_apply, Module.finrank_finsupp_self, Finsupp.support_smul_eq, MvPolynomial.IsSymmetric.C, MvPolynomial.pUnitAlgEquiv_monomial, Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero, Polynomial.support_derivativeFinsupp_subset_range, MvPolynomial.coeff_monomial, TensorProduct.equivFinsuppOfBasisRight_symm, Cardinal.mk_finsupp_of_infinite, MvPolynomial.coeff_mul_monomial, Polynomial.homogenize_sub, groupHomology.d₃₂_comp_d₂₁, groupHomology.d₃₂_single_one_snd, MvPolynomial.eval₂_eq, MvPolynomial.degreeOf_zero, exteriorPower.basis_repr, MvPolynomial.ringHom_ext'_iff, MvPolynomial.mem_ideal_span_monomial_image_iff_dvd, MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero, Algebra.mvPolynomial, Finsupp.support_eq_empty, IsRegular.monomial, groupHomology.π_comp_H2Iso_hom_apply, Matrix.charpoly.univ_map_eval₂Hom, MonomialOrder.leadingCoeff_prod_of_mem_nonZeroDivisors, groupHomology.isBoundary₀_iff, finsuppAddEquivDFinsupp_apply, Finsupp.indicator_eq_sum_single, Finsupp.graph_eq_empty, Module.Relations.Solution.span_relation_le_ker_π, MvPolynomial.comap_id_apply, MvPolynomial.aeval_one_tmul, Algebra.SubmersivePresentation.ofSubsingleton_σ', Nat.factorization_def, MvPolynomial.monomial_pow, Finsupp.prod_antidiagonal_swap, AddMonoidAlgebra.domCongr_apply, MvPolynomial.divMonomial_add_modMonomial_single, MvPolynomial.eval_sum, MonomialOrder.degree_prod, IsBaseChange.basis_repr_comp, MvPowerSeries.monomial_zero_one, Finsupp.mapRange.linearEquiv_trans, MvPolynomial.degreeOf_sub_lt, ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial, OrthonormalBasis.coe_toBasis_repr_apply, Finsupp.mapDomain.toLinearMap_linearEquiv, MvPolynomial.smul_eq_C_mul, MvPolynomial.eval₂_monomial, Nat.coprime_ordCompl, MvPolynomial.counitNat_C, Rep.coinvariantsTensorIndHom_mk_tmul_indVMk, ZLattice.normBound_spec, QuadraticMap.apply_linearCombination, Finsupp.support_mul_subset_left, groupHomology.mapCycles₁_hom, MvPolynomial.finSuccEquiv_rename_finSuccEquiv, Nat.Prime.pow_dvd_iff_le_factorization, Algebra.Presentation.HasCoeffs.relation_mem_range_map, MvPolynomial.rename_expand, Rep.indToCoind_coindToInd, MvPolynomial.homogeneousSubmodule_one_pow, MvPolynomial.coeff_mapRange, Algebra.Generators.fg_ker_of_finitePresentation, Finsupp.Colex.single_le_iff, finsuppAddEquivDFinsupp_symm_apply, groupHomology.isoCycles₁_inv_comp_iCycles, MvPolynomial.prod_X_pow, MonoidAlgebra.ofCoeff_smul, MvPolynomial.universalFactorizationMapPresentation_algebra_smul, MonomialOrder.degree_smul, Algebra.FiniteType.instMvPolynomialOfFinite, Finsupp.embSigma_apply, MvPolynomial.IsHomogeneous.sum_X_mul_pderiv, MvPolynomial.derivation_C_mul, AdjoinRoot.powerBasisAux'_repr_apply_to_fun, IsAdjoinRootMonic.coeff_apply_coe, Module.Basis.mapCoeffs_repr, MvPolynomial.aeval_sumElim_pderiv_inl, MvPolynomial.monomial_one_dvd_monomial_one, Module.Basis.traceDual_repr_apply, AnalyticAt.aeval_mvPolynomial, MvPolynomial.mul_monomial_modMonomial, groupHomology.cyclesMap_comp_isoCycles₁_hom_assoc, MvPolynomial.eval₂_natCast, MvPolynomial.tensorEquivSum_one_tmul_X, Finsupp.linearIndependent_single, Nat.factorization_factorial_le_div_pred, LinearMap.polyCharpoly_coeff_eq_zero_iff_of_basis, MvPolynomial.iterToSum_C_C, MvPolynomial.mapEquiv_refl, MvPolynomial.totalDegree_sub_C_le, MvPolynomial.coeffAddMonoidHom_apply, groupHomology.single_mem_cycles₁_of_mem_invariants, groupHomology.isoShortComplexH2_inv, Finsupp.liftAddHom_symm_apply_apply, groupHomology.coe_mapCycles₁, MvPolynomial.coeff_X_mul, AddMonoidAlgebra.single_mul_apply_aux, groupHomology.toCycles_comp_isoCycles₁_hom, MvPolynomial.supported_univ, Module.Relations.toQuotient_relation, MvPolynomial.isSymmetric_rename, Module.Flat.exists_factorization_of_comp_eq_zero_of_free, MvPolynomial.one_coeffsIn, MvPolynomial.mkDerivationₗ_X, MvPolynomial.eval₂_C_mk_eq_zero, MvPolynomial.mem_degrees, AddMonoidAlgebra.mem_supported', Finsupp.moduleIsTorsionFree, Module.Basis.ofZLatticeComap_repr_apply, MvPolynomial.universalFactorizationMap_freeMonic, Finsupp.embDomain_tsub, Finsupp.toDFinsupp_zero, Algebra.Generators.Hom.toAlgHom_monomial, Polynomial.homogenize_zero, MvPolynomial.le_degrees_add_left, Finsupp.DegLex.wellFoundedLT, MonomialOrder.sPolynomial_mem_ideal, MvPolynomial.mem_ideal_of_coeff_mem_ideal, MvPolynomial.irreducible_of_totalDegree_eq_one, MvPolynomial.universalFactorizationMapPresentation_val, Module.projective_def, Finsupp.coe_univ_sum_single, MvPolynomial.rename_comp_rename, groupHomology.chainsMap_f_2_comp_chainsIso₂_assoc, Finset.finsuppAntidiag_insert, Finsupp.mem_ideal_span_range_iff_exists_finsupp, MonomialOrder.leadingCoeff_sub_of_lt, HahnSeries.toMvPowerSeries_apply, MvPolynomial.coe_expand, Rep.indResHomEquiv_symm_apply, Module.End.ringEquivEndFinsupp_apply_apply_support, MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero, Finsupp.coe_tsub, groupHomology.mapCycles₂_comp_i_apply, MvPolynomial.aeval_sumElim, Module.annihilator_finsupp, Finsupp.neLocus_sub_right, MvPolynomial.universalFactorizationMapPresentation_σ', PolynomialModule.monomial_smul_apply, Representation.linearizeMap_toLinearMap, Finsupp.orderedSub, MvPolynomial.aeval_comp_rename, LinearMap.toMvPolynomial_eval_eq_apply, KaehlerDifferential.mvPolynomialBasis_repr_symm_single, groupHomology.boundariesToCycles₂_apply, Module.Basis.toMatrix_transpose_apply, MvPolynomial.mem_symmetricSubalgebra, Module.finite_finsupp_self_iff, HahnSeries.SummableFamily.coeff_apply, Finsupp.indicator_of_mem, MonomialOrder.degree_mul_of_isRegular_left, groupHomology.cyclesOfIsCycle₂_coe, rank_finsupp', MvPolynomial.support_rename_killCompl_subset, Nat.dvd_ordProj_of_dvd, Nat.factorization_pow, groupHomology.isoCycles₂_hom_comp_i, finTwoArrowEquiv'_sum_eq, MvPolynomial.eval₂_rename_prod_mk, Nat.properDivisors_eq_map_attach_Iio_factorization_prod_pow, Finsupp.sumFinsuppAddEquivProdFinsupp_symm_inr, AddMonoidAlgebra.ofCoeff_finsuppSum, Finsupp.embDomain_mono, AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe, Finsupp.DegLex.le_iff, Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial, groupHomology.π_comp_H1Iso_hom, Nat.ordProj_pos, MvPolynomial.coeff_linearCombination_X_pow_of_fintype, MvPolynomial.mapAlgHom_coe_ringHom, MvPolynomial.monomial_sum_one, Finsupp.curryAddEquiv_symm_apply, MvPowerSeries.truncFinset_truncFinset, bind₁_wittPolynomial_xInTermsOfW, Finsupp.liftAddHom_symm_apply, MonoidAlgebra.mul_apply_right, Nat.ordCompl_eq_self_iff_zero_or_not_dvd, groupHomology.isoCycles₂_inv_comp_iCycles, Module.Basis.ofZLatticeBasis_repr_apply, groupHomology.d₁₀_single_inv, groupHomology.mkH1OfIsTrivial_apply, MvPolynomial.schwartz_zippel_sum_degreeOf, MvPolynomial.isHomogeneous_C, Finsupp.Lex.wellFoundedLT, Finsupp.span_single_image, Algebra.FinitePresentation.out, Nat.ordProj_mul, Nat.factorization_eq_zero_of_remainder, MvPolynomial.rename_leftInverse, MvPolynomial.totalDegree_smul_le, MvPowerSeries.support_truncFinset_subset, IsIsotypic.linearEquiv_finsupp, MonomialOrder.Monic.mul, ax_grothendieck_of_locally_finite, MvPowerSeries.coeff_truncFinset, Finsupp.optionEquiv_symm_apply, SkewMonoidAlgebra.toFinsupp_eq_zero, Finsupp.equivFunOnFinite_symm_single, Algebra.FiniteType.iff_quotient_mvPolynomial'', Finsupp.pointwise_smul_support_finite, Finsupp.sum_add_index, Finsupp.degree_eq_zero_iff, Algebra.Presentation.quotientEquiv_mk, Finsupp.toMultiset_single, MvPolynomial.esymmAlgHom_fin_bijective, lp.zeroBasis_repr_symm_apply_coe, Finsupp.mem_graph_iff, MvPolynomial.esymmAlgEquiv_apply, Polynomial.homogenize_C, Finsupp.single_neg, MvPolynomial.eval₂AlgHom_X, Finsupp.tail_apply, LinearMap.toMatrixAlgEquiv_apply', MvPolynomial.mem_vanishingIdeal_iff, MonomialOrder.degree_add_of_lt, MvPolynomial.mem_vanishingIdeal_singleton_iff, MvPowerSeries.coeff_subst_finite, MonomialOrder.div, Finsupp.equivFunOnFinite_symm_sum, MvPolynomial.weightedTotalDegree'_eq_bot_iff, AlgebraicGeometry.AffineSpace.SpecIso_inv_over, Finsupp.linearCombination_surjective, WittVector.mul_polyOfInterest_aux5, IntermediateField.LinearDisjoint.basisOfBasisLeft_repr_apply, MvPolynomial.scalarRTensor_symm_apply_single, Finsupp.support_sup, MvPolynomial.expand_zmod, MonomialOrder.lex_le_iff, Finsupp.lsingle_range_le_ker_lapply, groupHomology.d₁₀ArrowIso_hom_right, MvPolynomial.aeval_zero', TensorProduct.equivFinsuppOfBasisLeft_apply, Module.Basis.prod_repr_inr, MvPolynomial.weightedTotalDegree_rename_of_injective, Finsupp.support_subset_iff, Finsupp.range_lmapDomain, Finsupp.neLocus_self_add_right, Finsupp.extendDomain_apply, MvPolynomial.range_mapAlgHom, AddEquiv.finsuppUnique_symm_apply_apply, Finsupp.add_sum_erase, MvPolynomial.counit_C, Finsupp.sum_smul_index_addMonoidHom, groupHomology.single_one_mem_boundaries₁, Finsupp.subtypeDomain_sub, Finsupp.single_sum, MvPolynomial.weightedHomogeneousComponent_of_mem, LinearMap.singularValues_of_lt, Finsupp.linearCombination_comp_lmapDomain, WeierstrassCurve.Projective.baseChange_polynomialZ, Finsupp.support_monotone, Finsupp.mem_span_image_iff_linearCombination, Finsupp.comapDomain.addMonoidHom_apply, MvPolynomial.IsHomogeneous.prod, MvPowerSeries.order_eq_nat, Nat.factorization_choose_prime_pow, MvPolynomial.irreducible_sumSMulXSMulY, Finsupp.equivMapDomain_refl', MvPolynomial.counitNat_X, MonomialOrder.degree_sPolynomial_le, MonomialOrder.degree_X_add_C, MvPolynomial.eval₂Hom_bind₂, MvPolynomial.mem_ideal_span_monomial_image, ArithmeticFunction.carmichael_factorization, Finsupp.sum_apply, MvPolynomial.rename_toMvPolynomial, MvPolynomial.aeval_rename, MonomialOrder.Monic.add_of_lt, WittVector.bind₁_frobeniusPolyRat_wittPolynomial, MvPolynomial.optionEquivLeft_symm_C_X, MvPolynomial.mul_X_modMonomial, BilinForm.apply_eq_dotProduct_toMatrix_mulVec, Nat.factorization_choose, MvPolynomial.bind₂_bind₂, Module.Relations.toQuotient_map, Representation.leftRegularMapEquiv_symm_single, MvPolynomial.IsSymmetric.antitone_supDegree, WittVector.aeval_verschiebungPoly, LaurentPolynomial.support_C_mul_T, groupHomology.d₂₁_single, Finsupp.mapDomain.linearEquiv_symm, MvPolynomial.eval₂Hom_bind₁, MvPowerSeries.coeff_rename, Polynomial.homogenize_X, Submodule.mem_span_set_iff_exists_finsupp_le_finrank, Module.Basis.constr_def, MvPolynomial.finSuccEquiv_X_zero, Finsupp.domCongr_trans, MvPolynomial.isJacobsonRing_MvPolynomial_fin, MvPolynomial.degreeOf_prod_le, MonomialOrder.monic_one, MvPolynomial.degreeOf_eq_natDegree, MvPowerSeries.support_expand_subset, MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_degree, Finsupp.mapRange.zeroHom_id, Finsupp.mapRange.addEquiv_trans, groupHomology.inhomogeneousChains.d_eq, Finsupp.comul_comp_lsingle, MvPolynomial.coeff_weightedHomogeneousComponent, WeierstrassCurve.Projective.dblX_eq, groupHomology.cycles₁IsoOfIsTrivial_inv_apply, Finsupp.coe_sum, Finsupp.Lex.addRightMono, MonomialOrder.coeff_mul_of_degree_add, groupHomology.eq_d₂₁_comp_inv_apply, Algebra.Presentation.baseChange_relation, Finsupp.faithfulSMul, MonomialOrder.degree_sub_leadingTerm_lt_degree, Module.Basis.toDual_apply_left, MonomialOrder.coeff_sPolynomial_sup_eq_zero, Finsupp.support_sup_union_support_inf, MonomialOrder.sPolynomial_mem_sup_ideal, Finsupp.optionEquiv_apply, QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar, MvPolynomial.esymm_zero, MvPolynomial.rTensor_apply, ax_grothendieck_univ, groupHomology.d₁₀_comp_coinvariantsMk_assoc, MvPolynomial.C_mem_coeffsIn, Finsupp.degree_mono, MvPolynomial.bind₁_X_right, MvPolynomial.coeff_rename_eq_zero, MvPolynomial.disjoint_support_monomial, TensorProduct.sum_tmul_basis_left_eq_zero, MvPowerSeries.monomial_mul_monomial, Module.DualBases.lc_def, MonomialOrder.coeff_mul_of_add_of_degree_le, Finsupp.Lex.acc, Finsupp.card_support_le_one, MonoidAlgebra.coeffEquiv_apply, Finsupp.single_eq_pi_single, MonoidAlgebra.mapDomainAddEquiv_apply, MvPolynomial.join₂_map, MvPolynomial.eval₂Hom_C_left, MvPolynomial.transcendental_supported_polynomial_aeval_X_iff, MvPolynomial.aeval_monomial, groupHomology.isoCycles₁_hom_comp_i, Finsupp.coe_mul, Polynomial.homogenize_eq_zero_iff, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over, Module.Relations.Solution.IsPresentation.exact, StandardEtalePresentation.toPresentation_relation, DividedPowerAlgebra.dp_smul, MvPolynomial.leadingCoeff_toLex, Finsupp.sum_ite_self_eq', Finsupp.sum_zero_index, Polynomial.toMvPolynomial_injective, Algebra.PreSubmersivePresentation.localizationAway_jacobiMatrix, AddMonoidAlgebra.ofCoeff_smul, Nat.factorization_eq_zero_iff, MvPolynomial.coeff_eval_eq_eval_coeff, AddMonoidAlgebra.coeff_zero, NumberField.canonicalEmbedding_eq_basisMatrix_mulVec, MvPolynomial.C_pow, Finsupp.coe_mk, Module.Relations.solutionFinsupp_isPresentation, groupHomology.chainsMap_f_0_comp_chainsIso₀_apply, MonoidAlgebra.mul_single_apply, LinearMap.polyCharpoly_natDegree, Finset.finsuppAntidiag_zero, MvPolynomial.coeffs_C_subset, Algebra.PreSubmersivePresentation.ofHasCoeffs_val, AList.lookupFinsupp_apply, Finsupp.eraseAddHom_apply, Module.Basis.reindexFinsetRange_repr, Finsupp.mem_frange, MvPolynomial.IsSymmetric.add, Submodule.mem_set_smul, Module.Basis.continuous_coe_repr, MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing, MonomialOrder.degree_mul, Finsupp.sym2Mul_apply_mk, Finsupp.mapDomain_apply', TensorProduct.finsuppScalarLeft_apply, MonomialOrder.degree_monomial_le, MvPolynomial.C_sub, Algebra.Generators.self_algebra_algebraMap, DFinsupp.toFinsupp_neg, MvPolynomial.esymm_eq_sum_subtype, Module.Basis.smulTower_repr, Module.Basis.toDual_apply_right, groupHomology.single_inv_ρ_self_add_single_mem_boundaries₁, Finsupp.toMultiset_sup, MvPolynomial.coeff_mul_monomial', Finsupp.nontrivial_iff, MonomialOrder.Monic.prod, MvPolynomial.ringKrullDim_of_isNoetherianRing, MvPowerSeries.lexOrder_le_of_coeff_ne_zero, Finsupp.linearCombination_comapDomain, Module.DualBases.coeffs_apply, MvPolynomial.pderiv_X_self, MvPolynomial.quotientEquivQuotientMvPolynomial_rightInverse, WittVector.mul_polyOfInterest_aux3, Nat.Prime.exists_addOrderOf_eq_pow_padic_val_nat_add_exponent, WittVector.verschiebungPoly_zero, MvPolynomial.pderiv_C, Nat.factorization_eq_zero_of_non_prime, MonomialOrder.degLex_single_lt_iff, MvPowerSeries.trunc'_one, MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix, MvPolynomial.modMonomial_add_divMonomial_single, List.toFinsupp_apply, constantCoeff_xInTermsOfW, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_smul, Finsupp.toLex_monotone, MvPolynomial.C_dvd_iff_zmod, ZSpan.repr_floor_apply, MvRatFunc.rank_eq_max_lift, MvPolynomial.aeval_prod, Finsupp.equivFunOnFinite_single, MvPolynomial.homogeneousSubmodule_mul, Finsupp.comapDomain_add_of_injective, MonomialOrder.leadingCoeff_one, Module.Basis.repr_symm_apply, Finsupp.coe_sub, Finsupp.apply_linearCombination_id, Matrix.toMvPolynomial_mul, Polynomial.Bivariate.pderiv_one_equivMvPolynomial, MonoidAlgebra.single_apply, Finsupp.support_inf, WittVector.wittOne_pos_eq_zero, Height.mulHeight_eval_le', MvPolynomial.IsHomogeneous.neg, MvPowerSeries.trunc_C_mul, MvPolynomial.exists_restrict_to_vars, MvPolynomial.lcoeff_apply, wittStructureInt_rename, WittVector.constantCoeff_wittNeg, algebraicIndependent_comp_subtype, map_wittStructureInt, Module.Basis.tensorProduct_repr_tmul_apply, MvPolynomial.algebraTensorAlgEquiv_symm_monomial, Finsupp.smul_single_one, Finsupp.Colex.single_lt_iff, Representation.freeLiftLEquiv_symm_apply, MvPolynomial.restrictSupport_eq_span, Nat.prod_pow_factorization_centralBinom, MonomialOrder.degree_sub_LTerm_lt, not_linearIndependent_iff_linearCombination, MvPolynomial.constantCoeff_comp_map, Finsupp.sub_single_one_add, Representation.free_asModule_free, Finset.mem_finsuppAntidiag', groupHomology.lsingle_comp_chainsMap_f_assoc, FirstOrder.Ring.mvPolynomial_zeroLocus_definable, MvPolynomial.rank_eq, MvPolynomial.vars_add_subset, Basis.piTensorProduct_repr_tprod_apply, MonomialOrder.sPolynomial_lt_of_degree_ne_zero_of_degree_eq, Finsupp.cons_zero_zero, Finsupp.mul_prod_erase', Finsupp.single_zero, MvPolynomial.aevalTower_algebraMap, Module.Relations.Solution.π_comp_map_apply, MvPolynomial.optionEquivLeft_elim_eval, MvPolynomial.esymm_one, MvPolynomial.optionEquivLeft_symm_X, SymmetricAlgebra.IsSymmetricAlgebra.mvPolynomial, groupHomology.single_mem_cycles₂_iff, TensorProduct.finsuppScalarLeft_symm_apply_single, MvPolynomial.renameEquiv_symm, MvPolynomial.eval₂Hom_C, Module.Basis.repr_smul', Representation.LinearizeMonoidal.μ_apply_apply, Finsupp.Lex.lt_iff, MvPolynomial.counitNat_surjective, lmap_finsuppLEquivDirectSum_eq, Finsupp.subtypeDomain_sum, Finsupp.DegLex.monotone_degree, Finset.finsuppAntidiagEquiv_symm_apply_apply, Finsupp.ker_lsingle, Module.Projective.out, PointedCone.mem_hull_set, groupHomology.boundaries₁_le_cycles₁, Module.Basis.repr_unitsSMul, MvPolynomial.support_symmDiff_support_subset_support_add, Representation.ind_apply, MvPolynomial.isEmptyRingEquiv_eq_coeff_zero, Finsupp.equivFunOnFinite_symm_eq_sum, MvPolynomial.sumToIter_C, MvPolynomial.mem_coeffs_iff, MvPolynomial.X_divMonomial, PowerSeries.coeff_pow, Height.mulHeight_eval_ge', WeierstrassCurve.Projective.dblX_eq', MvPolynomial.eval_expand, Finsupp.coe_mono, RingHom.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial, MonoidAlgebra.coeff_sum, Finsupp.wellFoundedLT_of_finite, MvPolynomial.aeval_comp_toMvPolynomial, Nat.ordCompl_dvd, Module.Basis.constr_apply, MvPolynomial.divMonomial_add, MvPolynomial.finrank_eq_one, Module.Finite.finsupp, MvPolynomial.supportedEquivMvPolynomial_symm_C, MonoidAlgebra.mul_apply_antidiagonal, Finsupp.single_nonneg, Matrix.toMvPolynomial_constantCoeff, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, MvPowerSeries.trunc'_map, MvPolynomial.derivation_eqOn_supported, Finsupp.ext_iff, MvPolynomial.killCompl_monomial_eq_monomial_comapDomain_of_subset, Finsupp.linearCombination_eq_fintype_linearCombination_apply, AddMonoidAlgebra.mapRingHom_apply, MvPolynomial.eval₂AlgHom_apply, MvPolynomial.tensorEquivSum_X_tmul_one, MvPolynomial.instIsMaximalVanishingIdealSingletonForallSet, Nat.factorization_eq_zero_of_lt, AList.lookupFinsupp_surjective, Representation.leftRegularMapEquiv_apply, MvPolynomial.C_inj, Finsupp.mapDomain_sub, MvPolynomial.expand_mul_eq_comp, WeierstrassCurve.Jacobian.map_polynomialY, Finsupp.Lex.single_le_iff, MvPolynomial.IsHomogeneous.eval₂, Subalgebra.LinearDisjoint.basisOfBasisLeft_repr_apply, TensorProduct.sum_tmul_basis_right_eq_zero, MvPolynomial.eval₂_pUnitAlgEquiv, MvPolynomial.eval_X, Finsupp.support_tsub, Finsupp.mapDomain.addMonoidHom_comp_mapRange, MvPowerSeries.hasSum_eval₂, Ideal.mem_span_pow_iff_exists_isHomogeneous, MvPolynomial.killCompl_monomial, Finsupp.disjoint_supported_supported_iff, Finsupp.erase_single, Polynomial.map_map_freeMonic, MonomialOrder.degree_prod_of_regular, List.toFinsupp_append, Nat.Partition.coeff_genFun, mem_finsuppAffineCoords_iff_linearCombination, MvPolynomial.supported_eq_range_rename, Nat.factorization_gcd, LinearMap.splittingOfFinsuppSurjective_splits, MvPolynomial.trdeg_of_isDomain, Finsupp.optionElim_apply_none, Submodule.LinearDisjoint.linearIndependent_left_of_flat, Module.Basis.repr_eq_iff', linearDepOn_iff', Finsupp.mapDomain_add, Finsupp.snd_sumFinsuppEquivProdFinsupp, List.toFinsupp_nil, Finsupp.prod_finset_sum_index, Finsupp.smul_single, Module.End.ringEquivEndFinsupp_symm_apply_apply, Finsupp.sum_single, Finsupp.supportedEquivFinsupp_symm_apply_coe_apply, Finsupp.subtypeDomain_zero, WeierstrassCurve.Projective.dblY_of_Y_eq', Finsupp.sumElim_inl, MvPolynomial.support_esymm, MvPolynomial.IsHomogeneous.C_mul, MvPolynomial.rename_hsymm, Module.Presentation.tautologicalRelations_relation, MonomialOrder.sPolynomial_decomposition', iSupIndep_range_lsingle, Rep.coinvariantsTensorIndInv_mk_tmul_indMk, MvPolynomial.constantCoeff_map, Finsupp.sum_finset_sum_index, MvPolynomial.transcendental_supported_X, MvPolynomial.degrees_add_of_disjoint, DividedPowerAlgebra.dp_add, Cardinal.mk_finsupp_lift_of_infinite', Finsupp.mapRange_finset_sum, MvPolynomial.aeval_natDegree_le, AnalyticOnNhd.eval_continuousLinearMap', MonoidAlgebra.single_mul_apply_of_not_exists_mul, Module.Basis.norm_repr_le_norm, MvPolynomial.degreeOf_neg, AddMonoidAlgebra.coeff_neg, Representation.freeLiftLEquiv_apply, MvPolynomial.scalarRTensor_apply_tmul_apply, MvPolynomial.optionEquivLeft_symm_C_C, MvPowerSeries.le_lexOrder_mul, Module.Basis.mem_span_repr_support, Pi.basisFun_repr, C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum, Algebra.leftMulMatrix_eq_repr_mul, Algebra.Generators.Hom.algebraMap_toAlgHom, Finsupp.apply_eq_of_mem_graph, Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, MonoidAlgebra.coeff_add, Finsupp.infinite_of_right, Finsupp.finsuppProdLEquiv_symm_apply_apply, MvPolynomial.IsSymmetric.sub, MvPolynomial.coeffsIn_le, Module.Basis.sum_repr, HahnSeries.SummableFamily.coeff_def, MonomialOrder.C_mul_leadingCoeff_monomial_degree, Finsupp.lmapDomain_disjoint_ker, Finsupp.supportedEquivFinsupp_apply_apply, WittVector.coeff_frobenius, ZSpan.mem_fundamentalDomain, MvPolynomial.degreeOf_mul_X_of_ne, Finsupp.nsmul_single_one_image, Finsupp.neLocus_self_sub_right, Rep.standardComplex.d_single, Finsupp.DegLex.lt_def, Submodule.image_smul_top_eq_range_lsum, groupHomology.d₁₀ArrowIso_inv_left, groupHomology.H1AddEquivOfIsTrivial_symm_tmul, Module.Basis.toMatrix_mulVec_repr, Algebra.Generators.comp_σ, groupHomology.single_mem_cycles₁_iff, AnalyticOnNhd.eval_mvPolynomial, groupHomology.d₂₁_single_ρ_add_single_inv_mul, MvPolynomial.support_smul, MvPowerSeries.monomial_smul_eq, MvPowerSeries.truncFinset_apply, Finsupp.single_mem_supported, DividedPowerAlgebra.dp_null_of_ne_zero, WeierstrassCurve.Projective.map_polynomialY, MvPolynomial.tensorEquivSum_C_tmul_C, MvPolynomial.IsHomogeneous.finSuccEquiv_coeff_isHomogeneous, MvPolynomial.finsum_weightedHomogeneousComponent, TensorProduct.sum_tmul_basis_left_injective, MvPowerSeries.order_monomial_of_ne_zero, Finsupp.graph_injective, Finsupp.indicator_injective, finsetBasisOfLinearIndependentOfCardEqFinrank_repr_apply, Module.End.ringHomEndFinsupp_surjective, Finsupp.mapDomain_tsub, Finsupp.isScalarTower, Algebra.Presentation.instFinitePresentationQuotientOfFinite, WeierstrassCurve.Projective.map_polynomial, WittVector.wittSub_zero, Finsupp.sumElim_zero_zero, Finsupp.sumElim_single_zero, DividedPowerAlgebra.mkRingHom_C, TensorProduct.equivFinsuppOfBasisRight_symm_apply, MvPolynomial.eval₂_assoc, MvPolynomial.instIsDomainOfIsCancelAdd, Finsupp.card_support_eq_zero, MvPowerSeries.subst_coe, MvPolynomial.coeff_zero_one, MvPolynomial.mapEquivMonic_symm_map_algebraMap, Module.Basis.algebraMapCoeffs_repr, MvPolynomial.support_X, Rep.finsupp_V, MonoidAlgebra.opRingEquiv_apply, WittVector.wittZero_eq_zero, MvPolynomial.coe_aeval_eq_eval, Nat.factorization_inj, Finsupp.lex_lt_of_lt_of_preorder, Finsupp.toMultiset_sum_single, Bundle.Trivialization.localFrame_coeff_apply_of_mem_baseSet, WeierstrassCurve.Projective.eval_polynomialY, AddMonoidAlgebra.coeffEquiv_apply, Nat.factorization_prod, Module.Basis.coord_apply, Multiset.toFinsupp_support, groupHomology.eq_d₁₀_comp_inv_apply, Finsupp.support_sum_eq_biUnion, DividedPowerAlgebra.prod_dp, exists_integral_inj_algHom_of_fg, MvPolynomial.coeff_rename_ne_zero, Module.Basis.mem_span_iff_repr_mem, Module.Basis.SmithNormalForm.repr_eq_zero_of_notMem_range, Module.Relations.Solution.IsPresentation.ker_π, KaehlerDifferential.quotKerTotalEquiv_apply, AddMonoidAlgebra.mul_apply_right, Finsupp.notMem_neLocus, MvPowerSeries.coeff_mul_of_add_lexOrder, KaehlerDifferential.kerTotal_map', Finsupp.instIsLeftCancelAdd, MvPolynomial.instIsLocalHomRingHomC, Finsupp.sumFinsuppEquivProdFinsupp_apply, MvPolynomial.eval₂_eq_eval_map, Finsupp.Colex.lt_iff_of_unique, MvPolynomial.coeff_add_pow, Finsupp.weight_eq_zero_iff_eq_zero, Finsupp.embDomain_some_none, Finsupp.toMultiset_map, MvPolynomial.weightedTotalDegree_zero, Finsupp.support_curry, Matrix.charpoly.univ_coeff_card, Polynomial.Bivariate.equivMvPolynomial_C_C, MonomialOrder.degree_sub_of_lt, Rep.barComplex.d_single, DividedPowerAlgebra.mkAlgHom_C, Module.Presentation.tautological_relation, Finsupp.mapDomain_smul, MvPolynomial.isWeightedHomogeneous_C, MvPolynomial.linearMap_ext_iff, Finsupp.indicator_indicator, MvPolynomial.map_X, Finsupp.prod_ite_eq', Finsupp.some_apply, Finsupp.domLCongr_refl, MvPolynomial.eval_assoc, groupHomology.d₂₁_comp_d₁₀_assoc, MvPolynomial.monomial_single_add, ax_grothendieck_zeroLocus, LinearMap.toMatrixAlgEquiv_transpose_apply, wittPolynomial_eq_sum_C_mul_X_pow, Finsupp.embDomain_le_embDomain_iff_le, Finsupp.mapRange_multiset_sum, Module.Basis.repr_self, Polynomial.homogenize_one, MvPolynomial.support_X_mul, MvPolynomial.coeffs_zero, exteriorPower.presentation.relations_relation, Finsupp.restrictSupportEquiv_symm_apply_coe, MvPolynomial.monomial_one_mul_cancel_right_iff, MonoidAlgebra.domCongr_apply, MonomialOrder.degree_mul', Finsupp.mapRange.addMonoidHom_id, constantCoeff_wittStructureInt_zero, TensorProduct.finsuppRight_apply_tmul_apply, Polynomial.homogenizeLM_apply, Finsupp.sum_ite_self_eq, Algebra.Generators.ker_naive, MvPolynomial.degreeOf_monomial_eq, Finsupp.linearCombination_zero, MvPolynomial.vanishingIdeal_zeroLocus_eq_radical, Nat.factorization_mul_of_coprime, Multiset.toFinsupp_strictMono, Finsupp.lcomapDomain_eq_linearProjOfIsCompl, Polynomial.homogenize_mul, Finsupp.Lex.wellFoundedLT_of_finite, MonomialOrder.degree_sPolynomial_lt_sup_degree, MonomialOrder.leadingTerm_eq_zero_iff, groupHomology.chainsMap_f_1_comp_chainsIso₁_apply, instFreeMvPolynomialKaehlerDifferential, isPrimePow_iff_minFac_pow_factorization_eq, MvPolynomial.hom_bind₁, WeierstrassCurve.Jacobian.map_polynomialX, MvPolynomial.coeff_expand_zero, MvPolynomial.C_dvd_iff_map_hom_eq_zero, MvPolynomial.IsSymmetric.neg, TensorProduct.finsuppRight_apply_tmul, Finsupp.toMultiset_inf, Module.subsingletonEquiv_apply, groupHomology.isBoundary₁_iff, rank_mvPolynomial_mvPolynomial, AnalyticOnNhd.eval_continuousLinearMap, MvPowerSeries.LinearTopology.hasBasis_nhds_zero, WeierstrassCurve.Jacobian.eval_polynomialZ, Finsupp.mapDomain_injective, Polynomial.degreeLT.basis_repr, MvPolynomial.vars_sum_subset, MvPolynomial.isMaximal_iff_eq_vanishingIdeal_singleton, Finsupp.coe_zero, Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial, Nat.ordCompl_self_pow, MvPolynomial.degreeOf_add_le, AddMonoidAlgebra.mul_single_apply_of_not_exists_add, Matrix.mvPolynomialX_mapMatrix_aeval, Module.Basis.repr_reindex_apply, MvPolynomial.algebraMap_def, MonomialOrder.leadingCoeff_mul_of_mul_leadingCoeff_ne_zero, Finsupp.weight_apply, groupHomology.mapCycles₁_quotientGroupMk'_epi, MvPolynomial.support_C, MvPolynomial.supported_eq_vars_subset, Finsupp.degree_def, groupHomology.mapCycles₁_comp_i_assoc, MvPolynomial.coeffs_X_mul, DividedPowerAlgebra.embed_def, LinearMap.toMatrix_apply, linearDepOn_iff'ₛ, MonomialOrder.degree_sub_leadingTerm_lt_iff, MvPolynomial.IsHomogeneous.coeff_isHomogeneous_of_optionEquivLeft_symm, MvPolynomial.eval₂_comp_right, Representation.linearize_apply, Nat.factorization_zero_right, NumberField.house.basis_repr_norm_le_const_mul_house, MonoidAlgebra.neg_apply, MvPolynomial.weightedHomogeneousComponent_apply, Finsupp.Set.indicator_singleton_eq, Polynomial.aeval_homogenize_of_eq_one, Nat.pow_factorization_choose_le, Finsupp.coe_orderIsoMultiset, MonomialOrder.degree_mul_of_right_mem_nonZeroDivisors, Nat.factorization_le_of_le_pow, Rep.coinvariantsTensorFreeToFinsupp_mk_tmul_single, MvPolynomial.map_eval, DFinsupp.toFinsupp_zero, MonomialOrder.degree_sub_leadingTerm_le, Representation.diagonalOneEquivLeftRegular_apply_single, Polynomial.homogenize_dvd, MvPolynomial.rename_eq, Cardinal.mk_finsupp_of_infinite', MvPolynomial.rank_eq_lift, Finsupp.linearIndependent_single_one, LinearMap.map_finsupp_linearCombination, Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det, MvPolynomial.totalDegree_coeff_optionEquivLeft_le, Finsupp.lt_wf, MvPolynomial.derivation_ext_iff, MvPolynomial.coeff_mul, MonoidAlgebra.mem_supported', Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination, Finsupp.Lex.lt_iff_of_unique, Finsupp.range_restrictDom, LinearMap.toMatrixAlgEquiv_transpose_apply', Module.Relations.Solution.π_single, Subgroup.exists_finsupp_of_mem_closure_range, Finsupp.lmapDomain_apply, linearIndepOn_iff_linearCombinationOnₛ, MvPolynomial.eval₂Hom_smul, WittVector.wittAdd_zero, Finsupp.DegLex.single_strictAnti, Finset.card_finsupp, Finsupp.instCanLift, MvPolynomial.mapEquivMonic_symm_map, ringKrullDim_mvPolynomial_of_isEmpty, MvPolynomial.IsHomogeneous.pderiv, MvPolynomial.mem_ideal_span_X_image, char_dvd_card_solutions_of_fintype_sum_lt, MvPolynomial.mem_restrictTotalDegree, Module.presentationFinsupp_var, MvPolynomial.vars_0, Polynomial.homogenize_neg, MvPolynomial.isHomogeneous_X_pow, finiteDimensional_finsupp, SkewMonoidAlgebra.toFinsupp_sum', Finsupp.domLCongr_single, MvPolynomial.vars_add_of_disjoint, groupHomology.mem_cycles₁_iff, Finsupp.sum_sum_index, MvPolynomial.restrictTotalDegree_le_restrictDegree, Nat.factorization_eq_of_coprime_left, factorization_one, instIsSemisimpleModuleFinsupp, Algebra.SubmersivePresentation.basisDeriv_apply, MvPolynomial.bind₁_monomial, TensorProduct.coe_finsuppScalarRight', LinearMap.polyCharpoly_coeff_eval, MvPolynomial.induction_on_monomial, lsum_comp_mapRange_toSpanSingleton, MvPolynomial.degreeOf_lt_iff, HahnSeries.SummableFamily.coe_ofFinsupp, Representation.finsuppTensorRight_apply_tmul_apply, Finsupp.sum_of_support_subset, MonomialOrder.degree_smul_of_mem_nonZeroDivisors, Module.Basis.repr_unop_eq_mulOpposite_repr, MvPolynomial.coe_coeffsIn, MvPolynomial.coe_mul, groupHomology.boundariesToCycles₁_apply, groupHomology.single_mem_cycles₂_iff_inv, groupHomology.d₁₀_single, Module.Relations.tensor_relation, MvPolynomial.mem_image_comap_C_basicOpen, MvPolynomial.continuous_eval, Algebra.Presentation.mem_ker_naive, MvPolynomial.C_eq_smul_one, linearIndepOn_iff_linearCombinationOn, Representation.linearizeTrivial_def, MvPowerSeries.coeff_mul, Finsupp.lsingle_apply, MvPolynomial.coeff_killCompl, MvPolynomial.vars_monomial_single, MvPolynomial.evalₗ_apply, MonoidAlgebra.coeff_sub, Finsupp.Colex.single_strictMono, Representation.IndV.hom_ext_iff, Module.Relations.Solution.IsPresentation.π_desc_apply, MvPolynomial.esymmAlgHom_surjective, Nat.Iic_factorization_prod_pow_injective, Pi.comul_comp_finsuppLcoeFun, Finsupp.mem_pi, Finsupp.toFreeAbelianGroup_comp_toFinsupp, MvPolynomial.aevalTower_ofNat, exteriorPower.basis_repr_self, TensorProduct.finsuppLeft'_apply, MvPolynomial.killCompl_monomial_eq_zero_of_notMem_range, Finsupp.erase_sub, Polynomial.derivativeFinsupp_C, TensorProduct.finsuppRight_tmul_single, MvPolynomial.monomial_modMonomial, Submodule.mulRightMap_apply_single, Module.finrank_finsupp, MvPolynomial.WeightedHomogeneousSubmodule.gradedMonoid, groupHomology.isoCycles₂_hom_comp_i_assoc, Finsupp.filter_zero, MvPolynomial.esymmAlgEquiv_symm_apply, Finsupp.card_support_eq_one, groupHomology.comp_d₃₂_eq, MvPowerSeries.lexOrder_mul_ge, Polynomial.derivativeFinsupp_X, finsuppLEquivDirectSum_symm_lof, Module.Flat.exists_factorization_of_isFinitelyPresented, Pi.lex_eq_finsupp_lex, instIsPushoutFractionRingMvPolynomial_1, groupHomology.H2π_eq_zero_iff, MvPolynomial.rename_surjective, Finsupp.toMultiset_eq_iff, Finsupp.curryLinearEquiv_symm_apply, KaehlerDifferential.linearCombination_surjective, Finsupp.lsubtypeDomain_apply, HahnSeries.coeff_ofFinsuppLinearMap, Module.Basis.sumQuot_repr_inr, MvPolynomial.map_id, instUniqueSumsFinsupp, Finsupp.prod_zero_index, Finsupp.linearCombination_onFinset, Finsupp.lsum_symm_apply, MvPowerSeries.coeff_add_monomial_mul, MvPolynomial.eval₂Hom_comp_expand, Finsupp.support_sub, AddMonoidAlgebra.mul_apply_antidiagonal, Module.Basis.coord_repr_symm, Module.Relations.Solution.linearCombination_var_relation, Polynomial.toMvPolynomial_C, Finsupp.lcongr_apply_apply, MonomialOrder.degree_sub_LTerm_le, Nat.factorization_le_factorization_of_dvd_right, Nat.ordCompl_of_not_prime, MonomialOrder.lex_le_iff_of_unique, MonomialOrder.sPolynomial_mul_monomial, MonomialOrder.degree_prod_of_mem_nonZeroDivisors, Algebra.Generators.toExtension_commRing, Nat.factorization_factorial_mul, Finsupp.sumElim_eq_add, Finsupp.instNontrivial, MvPowerSeries.trunc'_C, MvPowerSeries.prod_monomial, MonoidAlgebra.mul_single_apply_aux, ZLattice.abs_repr_le, LinearMap.singularValues_eq_zero_iff_le_finrank_range, MonomialOrder.degree_pow_of_pow_leadingCoeff_ne_zero, DirectSum.IsInternal.collectedBasis_repr_of_mem, Module.Basis.coe_sumCoords, Finsupp.equivFunOnFinite_symm_apply_apply, Algebra.Generators.Hom.equivAlgHom_apply_coe, MvPolynomial.decomposition.decompose'_eq, Finsupp.iSup_lsingle_range, Algebra.Generators.C_mul_X_sub_one_mem_ker, MvPolynomial.universalFactorizationMapPresentation_jacobian, MonoidAlgebra.ofCoeff_add, Representation.LinearizeMonoidal.ε_toLinearMap, LinearMap.sum_repr_mul_repr_mul, DividedPowerAlgebra.dp_eq_mkRingHom, MonomialOrder.sPolynomial_leadingTerm_mul, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap, Nat.squarefree_iff_factorization_le_one, Finsupp.mem_supported', MonoidAlgebra.mapRangeRingHom_apply, Finsupp.lmapDomain_supported, MvPolynomial.esymmAlgHom_injective, Representation.linearizeTrivialIso_symm_apply, MvPolynomial.coeff_sum, MvPowerSeries.trunc'_C_mul, MvPolynomial.commAlgEquiv_C_X, MvPolynomial.expand_zero_apply, Polynomial.homogenize_monomial, Finset.card_finsuppAntidiag_nat_eq_choose, groupHomology.δ₁_apply, Finsupp.DegLex.wellFounded, Module.Basis.ofIsLocalizedModule_repr_apply, MvPowerSeries.truncFinset_truncFinset_pow, Representation.leftRegularMapEquiv_symm_apply_toFun, WeierstrassCurve.Projective.negDblY_of_Y_eq', Polynomial.coeff_freeMonic, MonomialOrder.degree_sPolynomial, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap', AddMonoidAlgebra.apply_supDegree_add_supDegree, Module.Relations.Solution.ofQuotient_π, Finsupp.single_of_single_apply, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, groupHomology.H1π_eq_iff, LinearMap.fst_prodOfFinsuppNat, MvPolynomial.renameSymmetricSubalgebra_apply_coe, groupHomology.d₃₂_comp_d₂₁_apply, Algebra.FinitePresentation.iff_quotient_mvPolynomial', Finsupp.update_eq_erase_add_single, MvPolynomial.monomial_dvd_monomial, TensorProduct.finsuppLeft_apply_tmul_apply, groupHomology.chainsMap_f, MonomialOrder.degree_X_le_single, MvPolynomial.coe_mapEquivMonic_comp, MvPolynomial.eq_zero_of_eval_zero_at_prod_finset, MvPolynomial.transcendental_supported_polynomial_aeval_X, instIsPushoutFractionRingMvPolynomial, Height.max_mulHeightBound_zero_one_eq_one, groupHomology.chainsMap_f_2_comp_chainsIso₂_apply, MvPolynomial.monomial_mul_modMonomial, MvPolynomial.eval_polynomial_eval_finSuccEquiv, MvPolynomial.constantCoeff_comp_algebraMap, MvPolynomial.sumToIter_Xl, LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly, Finsupp.image_pow_eq_finsuppProd_image, Representation.ofMulAction_def, DividedPowerAlgebra.dp_null, groupHomology.cyclesMap_comp_isoCycles₁_hom, MvPolynomial.pderiv_inl_universalFactorizationMap_X, Finsupp.sym2_support_eq_preimage_support_mul, WittVector.constantCoeff_wittSub, Nat.divisors_eq_image_Iic_factorization_prod_pow, Finsupp.mapDomain_notin_range, MvPolynomial.counit_X, MvPolynomial.instFaithfulSMul, Finsupp.sum_option_index, MvPolynomial.rename_id, sigmaFinsuppLequivDFinsupp_apply, TensorProduct.eq_repr_basis_right, Finsupp.curry_apply, MvPolynomial.eval₂Hom_comp_C, Nat.factorization_factorial_eq_zero_of_lt, Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val, KaehlerDifferential.kerTotal_mkQ_single_algebraMap, MonoidAlgebra.mul_apply_left, MvPolynomial.idealOfVars_fg, MvPolynomial.rTensorAlgHom_apply_eq

---

← Back to Index