| Name | Category | Theorems |
|---|
addEquivFunOnFinite ๐ | CompOp | โ |
applyAddHom ๐ | CompOp | 1 mathmath: applyAddHom_apply
|
coeFnAddHom ๐ | CompOp | 1 mathmath: coeFnAddHom_apply
|
eraseAddHom ๐ | CompOp | 1 mathmath: eraseAddHom_apply
|
instAdd ๐ | CompOp | 556 mathmath: MvPolynomial.evalโ_mul_eq_zero_of_left, MonomialOrder.le_degree_of_mem_support, instCanonicallyOrderedAddOfAddLeftMono, toDFinsupp_add, MonomialOrder.sPolynomial_leadingTerm_mul', MvPolynomial.support_mul, MonomialOrder.span_leadingTerm_sdiff_singleton_zero, comapDomain_add, MvPolynomial.mul_X_divMonomial, Colex.addLeftStrictMono, MvPolynomial.coeffs_add, List.toFinsupp_eq_sum_mapIdx_single, MvPolynomial.zero_divMonomial, MvPolynomial.coeff_divMonomial, MonomialOrder.degree_add_of_ne, Algebra.Generators.H1Cotangent.ฮดAux_mul, Multiset.toFinsupp_add, MvPolynomial.mapEquiv_symm, MvPolynomial.homogeneousComponent_eq_zero', MvPolynomial.coeff_X_mul', sumFinsuppLEquivProdFinsupp_apply, groupHomology.dโโ_single, MvPolynomial.instIsReduced, MvPolynomial.isEmptyRingEquiv_apply, Algebra.Generators.toAlgHom_ofComp_localizationAway, MvPolynomial.leibniz_iff_X, domCongr_refl, neLocus_add_left, sumFinsuppAddEquivProdFinsupp_symm_inl, MvPolynomial.divMonomial_add_modMonomial, MonomialOrder.leadingCoeff_eq_zero_iff, MvPolynomial.homogeneousComponent_of_mem, prod_add_index_of_disjoint, MvPolynomial.expand_eq_zero, 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.coeffs_mul_X, MvPolynomial.mul_def, mapRange.addEquiv_refl, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C, groupHomology.mem_cyclesโ_iff, groupHomology.single_isCycleโ_iff_inv, Matrix.toMvPolynomial_add, Ordinal.CNF.coeff_opow_mul_add, DFinsupp.toFinsupp_add, MvPolynomial.mvPolynomialEquivMvPolynomial_symm_apply, subtypeDomain_add, MonomialOrder.leadingCoeff_mul_of_isRegular_right, support_single_add_single, sum_single_add_single, update_eq_add_single, MvPolynomial.irreducible_mul_X_add, MonomialOrder.leadingCoeff_mul, MonomialOrder.degree_sub_le, sigmaFinsuppAddEquivPiFinsupp_apply, neLocus_self_add_left, WittVector.mul_polyOfInterest_aux2, add_sub_single_one, Lex.addLeftMono, prod_add_index, MvPolynomial.pderiv_one, MvPolynomial.pderiv_mul, MonomialOrder.degree_lt_iff, MvPolynomial.evalโ_zero, MvPolynomial.degreeOf_mul_le, MvPolynomial.aeval_ite_mem_eq_self, MvPolynomial.support_sdiff_support_subset_support_add, MvPolynomial.IsWeightedHomogeneous.mul, toMultiset_toFinsupp, MvPolynomial.totalDegree_add_eq_right_of_totalDegree_lt, mapRange.addEquiv_apply, MvPolynomial.monomial_zero, MonomialOrder.degree_reduce_lt, MvPolynomial.sum_antidiagonal_card_esymm_psum_eq_zero, MvPolynomial.X_mul_cancel_right_iff, Multiset.toFinsupp_sum_eq, sumFinsuppAddEquivProdFinsupp_symm_apply, MvPolynomial.support_eq_empty, MvPolynomial.mvPolynomialEquivMvPolynomial_apply, sigmaFinsuppAddEquivDFinsupp_symm_apply, AddEquiv.finsuppUnique_symm, MonomialOrder.toSyn_strictMono, MonomialOrder.leadingTerm_zero, MvPolynomial.evalโ_mul_monomial, AddMonoidAlgebra.coeff_add, MonomialOrder.div_single, MvPolynomial.esymmAlgHomMonomial_single, MvPolynomial.homogeneousComponent_C_mul, MonomialOrder.image_leadingTerm_sdiff_singleton_zero, groupHomology.dโโ_single_inv_mul_ฯ_add_single, MvPolynomial.monomial_mul_mem_coeffsIn, MvPolynomial.monomial_one_dvd_iff_modMonomial_eq_zero, support_add_single, mapRange.addEquiv_toEquiv, Nat.factorization_mul, MvPolynomial.X_mul_pderiv_monomial, MonomialOrder.degree_add_le, MvPolynomial.totalDegree_list_prod, some_add, MvPolynomial.weightedHomogeneousComponent_eq_zero', MvPolynomial.IsHomogeneous.add, MvPolynomial.coe_eq_zero_iff, factorization_mul, MvPowerSeries.lexOrder_mul, Colex.addRightMono, WeierstrassCurve.Jacobian.polynomialY_eq, MvPolynomial.support_add, MonomialOrder.sPolynomial_self, MonomialOrder.leadingCoeff_mul_of_right_mem_nonZeroDivisors, update_eq_single_add, add_eq_zero_iff, MonomialOrder.le_degree, MvPolynomial.mul_X_mem_coeffsIn, sigmaFinsuppEquivDFinsupp_add, Colex.addRightStrictMono, MvPolynomial.totalDegree_mul_of_isDomain, embSigma_add, sub_add_single_one_cancel, MvPolynomial.X_mul_mem_coeffsIn, MonomialOrder.degree_mul_leadingTerm, xInTermsOfW_eq, MvPolynomial.eq_zero_of_eval_eq_zero, Polynomial.homogenize_add, MvPowerSeries.coeff_trunc'_mul_trunc'_eq_coeff_mul, erase_add, Multiset.toFinsupp_union, MonomialOrder.span_leadingTerm_eq_span_monomialโ, LinearMap.polyCharpoly_coeff_eq_zero_of_basis, MvPolynomial.C_mul_X_eq_monomial, add_apply, MvPolynomial.degreeOf_mul_eq, MvPolynomial.C_0, MvPolynomial.bindโ_monomial, sumFinsuppLEquivProdFinsupp_symm_apply, support_add_eq, prod_add_index', Algebra.SubmersivePresentation.jacobianRelations_spec, LinearMap.toMvPolynomial_add, WeierstrassCurve.Projective.polynomialZ_eq, MonomialOrder.lex_lt_iff_of_unique, SkewMonoidAlgebra.toFinsuppAddEquiv_apply, FreeAbelianGroup.equivFinsupp_symm_apply, AddCommGroup.equiv_free_prod_directSum_zmod, MvPolynomial.coe_zero, MonomialOrder.degLex_le_iff, MvPolynomial.coeff_C_mul, MvPolynomial.C_mul_monomial, MonomialOrder.monic_X_add_C, MvPolynomial.mapEquiv_apply, Multiset.toFinsupp_inter, MonomialOrder.degree_le_iff, wittPolynomial_one, MvPolynomial.pderiv_X, MvPolynomial.evalโ_mul_eq_zero_of_right, domCongr_apply, IsLocalization.Away.mvPolynomialQuotientEquiv_apply, MvPolynomial.C_add, LinearMap.toMvPolynomial_zero, Multiset.toFinsupp_apply, sum_add_index', MvPolynomial.isHomogeneous_C_mul_X, WittVector.mul_polyOfInterest_aux4, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some, Algebra.Generators.localizationAway_ฯ, AddEquiv.finsuppUnique_apply, MvPolynomial.IsWeightedHomogeneous.weightedHomogeneousComponent_ne, MvPolynomial.IsSymmetric.mul, MonomialOrder.degree_mul_of_isRegular_right, MvPolynomial.coeff_monomial_mul, Finset.mapRange_finsuppAntidiag_eq, MvPolynomial.IsWeightedHomogeneous.add, MvPolynomial.X_mul_cancel_left_iff, MonomialOrder.degree_sum_le, instTwoUniqueSumsFinsupp, MonomialOrder.degree_mul_of_mul_leadingCoeff_ne_zero, MvPolynomial.X_dvd_mul_iff, MvPolynomial.killCompl_monomial_eq_zero_of_not_subset, MvPolynomial.IsWeightedHomogeneous.sum_weight_X_mul_pderiv, filter_add, MvPolynomial.pderiv_def, MvPolynomial.isEmptyRingEquiv_symm_apply, MonomialOrder.degree_leadingTerm_mul, Matrix.toMvPolynomial_zero, snd_sumFinsuppAddEquivProdFinsupp, MvPolynomial.modMonomial_add_divMonomial, MonomialOrder.span_leadingTerm_eq_span_monomial', MvPolynomial.rename_zero, WittVector.bindโ_wittMulN_wittPolynomial, MvPolynomial.dvd_X_mul_iff, MvPolynomial.monomial_one_mul_cancel_left_iff, MvPolynomial.eq_zero_iff, MvPowerSeries.coeff_truncFinset_mul_truncFinset_eq_coeff_mul, xInTermsOfW_aux, MonomialOrder.degree_mul_lt_iff_left_lt_of_ne_zero, coe_curryAddEquiv, MonomialOrder.degree_smul_le, MvPolynomial.degreeOf_mul_X_eq_degreeOf_add_one_iff, MvPowerSeries.truncFinset_monomial_eq_zero, MonomialOrder.toSyn_degree_mul_le, Polynomial.homogenize_X_pow, mapRange.addEquiv_symm, MvPolynomial.combinatorial_nullstellensatz_exists_linearCombination, wittStructureRat_rec, WittVector.mul_polyOfInterest_vars, MvPolynomial.isRegular_prod_X, algebraicIndependent_iff, MonomialOrder.degree_mul_le, neLocus_add_right, sum_add_index_of_disjoint, MonomialOrder.sPolynomial_def, MonomialOrder.le_add_right, MonomialOrder.degree_mul_of_left_mem_nonZeroDivisors, MvPolynomial.monomial_add_single, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_none, MonomialOrder.degree_pow_le, MvPolynomial.eval_add, prod_hom_add_index, domCongr_symm, MvPolynomial.isNilpotent_iff, addCommute_of_disjoint, update_eq_single_add_erase, MvPolynomial.instNoZeroDivisors, MvPolynomial.monomial_eq_zero, degree_preimage_add, Relation.cutExpand_le_invImage_lex, MvPolynomial.coeff_monomial_mul', MonomialOrder.toSyn_monotone, MvPolynomial.vars_C_mul, MonomialOrder.sPolynomial_left_zero, MonomialOrder.support_leadingTerm, wittStructureRat_rec_aux, MvPolynomial.evalโ_add, MonomialOrder.image_leadingTerm_insert_zero, Algebra.Generators.ker_localizationAway, MonomialOrder.degLex_single_le_iff, MvPolynomial.support_mul_X, SkewMonoidAlgebra.toFinsuppAddEquiv_symm_apply, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, Ordinal.CNF.eval_add, List.toFinsupp_concat_eq_toFinsupp_add_single, mapRange_add', sumFinsuppAddEquivProdFinsupp_apply, MonomialOrder.leadingCoeff_mul_of_left_mem_nonZeroDivisors, Finset.mapRange_finsuppAntidiag_subset, groupHomology.inhomogeneousChains.d_single, Algebra.Generators.comp_localizationAway_ker, MvPolynomial.mul_esymm_eq_sum, MvPolynomial.eval_mul, groupHomology.isBoundaryโ_iff, MvPolynomial.isWeightedHomogeneous_zero, MonomialOrder.coeff_degree_eq_zero_iff, toMultiset_add, Multiset.toFinsupp_singleton, MvPolynomial.degreeOf_mul_X_self, MonomialOrder.sPolynomial_right_zero, WeierstrassCurve.Projective.polynomialX_eq, Multiset.toFinsupp_symm_apply, FreeAbelianGroup.equivFinsupp_apply, MvPolynomial.totalDegree_add, Polynomial.homogenize_C_mul, groupHomology.single_isCycleโ_iff, MvPolynomial.coe_add, MvPolynomial.modMonomial_X, MonomialOrder.leadingCoeff_add_of_lt, MvPolynomial.divMonomial_mul_monomial, AlgebraicIndependent.eq_zero_of_aeval_eq_zero, WeierstrassCurve.Projective.polynomialY_eq, MvPolynomial.weightedHomogeneousComponent_finsupp, MvPolynomial.coeff_mul_X', List.support_sum_eq, MvPolynomial.coeff_mul_X, instIsCancelAdd, MvPolynomial.C_eq_zero, WittVector.frobeniusPolyAux_eq, MvPolynomial.weightedHomogeneousComponent_of_isWeightedHomogeneous_ne, MvPolynomial.C_mul', Algebra.Generators.cMulXSubOneCotangent_eq, SkewMonoidAlgebra.ofFinsupp_add, coe_add, MvPolynomial.pderiv_C_mul, MvPolynomial.evalโ_mul, MvPowerSeries.coeff_add_mul_monomial, sumElim_single_single, MvPolynomial.restrictSupport_nsmul, AddMonoidAlgebra.coeffAddEquiv_symm_apply, MvPolynomial.X_dvd_iff_modMonomial_eq_zero, coe_orderIsoMultiset_symm, MvPolynomial.X_mul_divMonomial, SkewMonoidAlgebra.toFinsupp_add, groupHomology.single_ฯ_self_add_single_inv_mem_boundariesโ, support_single_add_single_subset, fst_sumFinsuppAddEquivProdFinsupp, MvPolynomial.homogeneousComponent_eq_zero, Algebra.SubmersivePresentation.sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs, WeierstrassCurve.Jacobian.polynomialZ_eq, MonomialOrder.sPolynomial_monomial_mul, MvPolynomial.isRegular_X, support_single_add, AddMonoidAlgebra.ofCoeff_add, MonomialOrder.degree_le_degree_of_support_subset, MvPolynomial.monomial_sum_index, exteriorPower.presentation_relation, MvPolynomial.add_divMonomial, Lex.addRightStrictMono, MvPolynomial.isEmptyRingEquiv_symm_toRingHom, WittVector.mul_polyOfInterest_aux1, erase_add_single, MvPolynomial.monomial_mul, MonomialOrder.toSyn_eq_zero_iff, MvPolynomial.pderiv_X_of_ne, update_eq_sub_add_single, MvPolynomial.IsSymmetric.zero, MvPolynomial.isRegular_X_pow, sigmaFinsuppLequivDFinsupp_symm_apply, MvPolynomial.degrees_add_le, Multiset.toFinsupp_zero, MvPolynomial.isHomogeneous_zero, MvPolynomial.degrees_mul_le, single_add_erase, Multiset.toFinsupp_toMultiset, MonomialOrder.degree_prod_le, MvPolynomial.totalDegree_add_eq_left_of_totalDegree_lt, MvPolynomial.dvd_monomial_mul_iff_exists, MonomialOrder.span_leadingTerm_insert_zero, MonomialOrder.div_set, single_add, MvPolynomial.X_mul_modMonomial, MonomialOrder.degree_zero, embDomain_add, degree_preimage_nsmul, MonoidAlgebra.coeffAddEquiv_symm_apply, MvPolynomial.coeff_zero, Lex.addLeftStrictMono, MvPolynomial.weightedHomogeneousComponent_eq_zero_of_notMem, MonomialOrder.degLex_lt_iff, sum_hom_add_index, MvPolynomial.pderiv_pow, MvPolynomial.totalDegree_zero, mapRange.addEquiv_toAddMonoidHom, Nat.factorization_eq_primeFactorsList_multiset, addLeftReflectLE, WittVector.bindโ_verschiebungPoly_wittPolynomial, MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero_of_le_card, MvPolynomial.tensorEquivSum_X_tmul_X, MvPolynomial.vars_mul, Algebra.Presentation.relation_comp_localizationAway_inl, MvPolynomial.degreeOf_mul_C_le, MvPolynomial.esymmAlgHomMonomial_add, MvPolynomial.degrees_mul_eq, MvPolynomial.isHomogeneous_C_mul_X_pow, List.support_sum_subset, Algebra.SubmersivePresentation.exists_sum_eq_ฯ_jacobian_mul_ฯ_jacobian_inv_sub_one, Multiset.toFinsupp_eq_iff, MvPolynomial.degreeOf_C_mul_le, algebraicIndependent_subtype, MonomialOrder.degree_add_eq_right_of_lt, filter_pos_add_filter_neg, MvPolynomial.monomial_eq, support_add, Polynomial.homogenize_monomial_of_lt, AddEquiv.finsuppUnique_symm_apply_support_val, WittVector.wittMul_zero, MvPowerSeries.coeff_mul_eq_coeff_trunc'_mul_trunc', MvPolynomial.evalโ_mul_C, domLCongr_apply, MonomialOrder.degree_lt_of_left_ne_zero_of_degree_mul_lt, MvPolynomial.weightedHomogeneousComponent_eq_zero, MvPolynomial.restrictSupport_add, MvPolynomial.instIsCancelMulZeroOfIsCancelAdd, WittVector.polyOfInterest_vars_eq, MvPolynomial.mapEquiv_trans, Colex.addLeftMono, MvPolynomial.pderiv_inr_universalFactorizationMap_X, MvPolynomial.degrees_zero, MvPolynomial.IsHomogeneous.mul, AddMonoidAlgebra.coeffAddEquiv_apply, MvPolynomial.weightedHomogeneousComponent_C_mul, MonomialOrder.leadingCoeff_zero, MvPolynomial.mul_monomial_mem_coeffsIn, KaehlerDifferential.mvPolynomialBasis_repr_D, MonomialOrder.sPolynomial_monomial_mul', MvPolynomial.pderiv_eq_zero_of_notMem_vars, single_add_single_eq_single_add_single, MvPolynomial.support_divMonomial, MvPolynomial.le_degrees_add_right, MvPolynomial.weightedTotalDegree'_zero, WeierstrassCurve.Jacobian.polynomialX_eq, MvPolynomial.C_mul_X_pow_eq_monomial, MvPolynomial.totalDegree_mul, MonoidAlgebra.coeffAddEquiv_apply, mapRange_add, MvPolynomial.coeff_add, MvPolynomial.psum_eq_mul_esymm_sub_sum, MvPolynomial.IsWeightedHomogeneous.C_mul, MvPolynomial.support_zero, MvPolynomial.rename_eq_zero_iff_of_injective, MonomialOrder.leadingCoeff_mul_of_isRegular_left, KaehlerDifferential.mvPolynomialBasis_repr_comp_D, MvPolynomial.degreeOf_C_mul, MvPolynomial.C_mul, WittVector.bindโ_zero_wittPolynomial, MonomialOrder.lex_lt_iff, MvPolynomial.divMonomial_monomial_mul, MvPolynomial.instIsCancelAddOfIsLeftCancelAdd, addCommute_iff_inter, Ordinal.CNF.eval_single_add, Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero, MvPolynomial.coeff_mul_monomial, MvPolynomial.degreeOf_zero, MvPolynomial.IsHomogeneous.eq_zero_of_forall_eval_eq_zero, IsRegular.monomial, finsuppAddEquivDFinsupp_apply, MvPolynomial.divMonomial_add_modMonomial_single, MvPolynomial.smul_eq_C_mul, finsuppAddEquivDFinsupp_symm_apply, MvPolynomial.IsHomogeneous.sum_X_mul_pderiv, MvPolynomial.mul_monomial_modMonomial, LinearMap.polyCharpoly_coeff_eq_zero_iff_of_basis, MvPolynomial.mapEquiv_refl, MvPolynomial.coeff_X_mul, MvPolynomial.evalโ_C_mk_eq_zero, Polynomial.homogenize_zero, MvPolynomial.le_degrees_add_left, orderedSub, MonomialOrder.degree_mul_of_isRegular_left, sumFinsuppAddEquivProdFinsupp_symm_inr, curryAddEquiv_symm_apply, MonomialOrder.Monic.mul, sum_add_index, Polynomial.homogenize_C, MonomialOrder.degree_add_of_lt, MonomialOrder.div, MvPolynomial.weightedTotalDegree'_eq_bot_iff, WittVector.mul_polyOfInterest_aux5, MonomialOrder.lex_le_iff, neLocus_self_add_right, AddEquiv.finsuppUnique_symm_apply_apply, MvPolynomial.weightedHomogeneousComponent_of_mem, MonomialOrder.degree_sPolynomial_le, MonomialOrder.degree_X_add_C, MonomialOrder.Monic.add_of_lt, MvPolynomial.mul_X_modMonomial, groupHomology.dโโ_single, Polynomial.homogenize_X, domCongr_trans, mapRange.addEquiv_trans, Lex.addRightMono, MonomialOrder.coeff_mul_of_degree_add, MonomialOrder.degree_sub_leadingTerm_lt_degree, MvPowerSeries.monomial_mul_monomial, MonomialOrder.coeff_mul_of_add_of_degree_le, Polynomial.homogenize_eq_zero_iff, StandardEtalePresentation.toPresentation_relation, Algebra.PreSubmersivePresentation.localizationAway_jacobiMatrix, MvPolynomial.IsSymmetric.add, MonomialOrder.degree_mul, MonomialOrder.degree_monomial_le, groupHomology.single_inv_ฯ_self_add_single_mem_boundariesโ, MvPolynomial.coeff_mul_monomial', WittVector.mul_polyOfInterest_aux3, WittVector.verschiebungPoly_zero, MvPolynomial.pderiv_C, MonomialOrder.degLex_single_lt_iff, MvPolynomial.modMonomial_add_divMonomial_single, MvPolynomial.C_dvd_iff_zmod, comapDomain_add_of_injective, WittVector.wittOne_pos_eq_zero, MvPowerSeries.trunc_C_mul, algebraicIndependent_comp_subtype, MonomialOrder.degree_sub_LTerm_lt, sub_single_one_add, MvPolynomial.vars_add_subset, MonomialOrder.sPolynomial_lt_of_degree_ne_zero_of_degree_eq, groupHomology.single_mem_cyclesโ_iff, MvPolynomial.support_symmDiff_support_subset_support_add, MvPolynomial.isEmptyRingEquiv_eq_coeff_zero, MvPolynomial.divMonomial_add, MvPolynomial.killCompl_monomial, List.toFinsupp_append, Nat.Partition.coeff_genFun, mapDomain_add, MvPolynomial.IsHomogeneous.C_mul, Module.Presentation.tautologicalRelations_relation, MvPolynomial.degrees_add_of_disjoint, MvPowerSeries.le_lexOrder_mul, C_p_pow_dvd_bindโ_rename_wittPolynomial_sub_sum, MonoidAlgebra.coeff_add, MonomialOrder.C_mul_leadingCoeff_monomial_degree, MvPolynomial.degreeOf_mul_X_of_ne, nsmul_single_one_image, Algebra.Generators.comp_ฯ, groupHomology.dโโ_single_ฯ_add_single_inv_mul, WittVector.wittZero_eq_zero, Multiset.toFinsupp_support, MvPowerSeries.coeff_mul_of_add_lexOrder, instIsLeftCancelAdd, MvPolynomial.coeff_add_pow, MvPolynomial.weightedTotalDegree_zero, Rep.barComplex.d_single, Module.Presentation.tautological_relation, MvPolynomial.monomial_single_add, wittPolynomial_eq_sum_C_mul_X_pow, MvPolynomial.support_X_mul, MvPolynomial.coeffs_zero, exteriorPower.presentation.relations_relation, MvPolynomial.monomial_one_mul_cancel_right_iff, MonomialOrder.degree_mul', Nat.factorization_mul_of_coprime, Multiset.toFinsupp_strictMono, Polynomial.homogenize_mul, MonomialOrder.degree_sPolynomial_lt_sup_degree, MonomialOrder.leadingTerm_eq_zero_iff, MvPolynomial.C_dvd_iff_map_hom_eq_zero, groupHomology.isBoundaryโ_iff, MvPolynomial.degreeOf_add_le, MonomialOrder.leadingCoeff_mul_of_mul_leadingCoeff_ne_zero, MvPolynomial.coeffs_X_mul, MonomialOrder.degree_sub_leadingTerm_lt_iff, MonomialOrder.degree_mul_of_right_mem_nonZeroDivisors, MonomialOrder.degree_sub_leadingTerm_le, MvPolynomial.coeff_mul, WittVector.wittAdd_zero, MvPolynomial.vars_0, MvPolynomial.vars_add_of_disjoint, MvPolynomial.bindโ_monomial, MvPolynomial.coe_mul, groupHomology.single_mem_cyclesโ_iff_inv, MvPolynomial.killCompl_monomial_eq_zero_of_notMem_range, MvPolynomial.monomial_modMonomial, MvPowerSeries.lexOrder_mul_ge, Polynomial.derivativeFinsupp_X, toMultiset_eq_iff, instUniqueSumsFinsupp, MvPowerSeries.coeff_add_monomial_mul, MonomialOrder.degree_sub_LTerm_le, MonomialOrder.lex_le_iff_of_unique, MonomialOrder.sPolynomial_mul_monomial, sumElim_eq_add, Algebra.Generators.C_mul_X_sub_one_mem_ker, MvPolynomial.universalFactorizationMapPresentation_jacobian, MonoidAlgebra.ofCoeff_add, MonomialOrder.sPolynomial_leadingTerm_mul, MvPowerSeries.trunc'_C_mul, Polynomial.coeff_freeMonic, MonomialOrder.degree_sPolynomial, update_eq_erase_add_single, MonomialOrder.degree_X_le_single, MvPolynomial.eq_zero_of_eval_zero_at_prod_finset, Height.max_mulHeightBound_zero_one_eq_one, MvPolynomial.monomial_mul_modMonomial, MvPolynomial.pderiv_inl_universalFactorizationMap_X, sigmaFinsuppLequivDFinsupp_apply
|
instAddCommGroup ๐ | CompOp | 190 mathmath: groupHomology.ฯ_comp_H2Iso_hom_assoc, groupHomology.mapCyclesโ_comp_assoc, groupHomology.dโโ_single_one, groupHomology.chainsMap_f_3_comp_chainsIsoโ_apply, groupHomology.dโโ_single, Rep.coindToInd_of_support_subset_orbit, groupHomology.mapCyclesโ_comp_apply, groupHomology.cyclesIsoโ_inv_comp_iCycles_apply, groupHomology.eq_dโโ_comp_inv, Rep.coindToInd_indToCoind, Module.FaithfullyFlat.finsupp, groupHomology.cyclesMap_comp_isoCyclesโ_hom, groupHomology.comp_dโโ_eq, groupHomology.mapCyclesโ_comp_assoc, groupHomology.toCycles_comp_isoCyclesโ_hom_assoc, groupHomology.ฮดโ_apply, groupHomology.dโโ_single_one_thd, groupHomology.isoCyclesโ_inv_comp_iCycles_apply, KaehlerDifferential.quotKerTotalEquiv_symm_comp_D, Rep.ฮต_def, groupHomology.chainsโToCoinvariantsKer_surjective, Module.presentationFinsupp_G, groupHomology.dโโ_comp_dโโ_assoc, Rep.ฮผ_def, groupHomology.dโโArrowIso_hom_left, groupHomology.cyclesโIsoOfIsTrivial_hom_apply, Representation.coinvariantsFinsuppLEquiv_apply, groupHomology.dโโ_single_inv_mul_ฯ_add_single, groupHomology.dโโ_comp_coinvariantsMk_apply, groupHomology.chainsMap_f_3_comp_chainsIsoโ, groupHomology.mapCyclesโ_id_comp_assoc, groupHomology.eq_dโโ_comp_inv, groupHomology.mapCyclesโ_comp, Module.Presentation.finsupp_R, groupHomology.mapCyclesโ_comp_i, Module.Presentation.finsupp_G, groupHomology.mapCyclesโ_id_comp, KaehlerDifferential.kerTotal_mkQ_single_algebraMap_one, groupHomology.dโโ_single_inv_self_ฯ_sub_self_inv, groupHomology.toCycles_comp_isoCyclesโ_hom_apply, Rep.ฮด_def, groupHomology.mapCyclesโ_comp_i, KaehlerDifferential.kerTotal_mkQ_single_add, groupHomology.eq_dโโ_comp_inv_apply, groupHomology.mapCyclesโ_id_comp_apply, Module.Presentation.finsupp_var, groupHomology.ฯ_comp_H2Iso_hom, groupHomology.pOpcycles_comp_opcyclesIso_hom_apply, Rep.coindToInd_apply, groupHomology.mapCyclesโ_comp_i_apply, groupHomology.mapCyclesโ_comp, groupHomology.coe_mapCyclesโ, groupHomology.comp_dโโ_eq, groupHomology.H1ฯ_comp_map_apply, groupHomology.toCycles_comp_isoCyclesโ_hom_assoc, Representation.finsuppToCoinvariants_single_mk, groupHomology.H2ฯ_comp_map_assoc, Module.presentationFinsupp_R, groupHomology.dโโArrowIso_inv_right, KaehlerDifferential.derivationQuotKerTotal_apply, groupHomology.dโโ_comp_coinvariantsMk, groupHomology.dโโ_comp_dโโ_apply, groupHomology.mapCyclesโ_comp_apply, groupHomology.H2ฯ_eq_iff, groupHomology.H1AddEquivOfIsTrivial_single, groupHomology.range_dโโ_eq_coinvariantsKer, groupHomology.isoCyclesโ_hom_comp_i_apply, groupHomology.eq_dโโ_comp_inv_assoc, groupHomology.cyclesMap_comp_isoCyclesโ_hom_assoc, groupHomology.inhomogeneousChains.d_single, Module.Relations.solutionFinsupp_var, groupHomology.mapCyclesโ_id_comp_assoc, groupHomology.ฯ_comp_H1Iso_hom_apply, groupHomology.toCycles_comp_isoCyclesโ_hom, groupHomology.cyclesMap_comp_isoCyclesโ_hom_apply, groupHomology.mapCyclesโ_id_comp, Module.Presentation.finsupp_relation, groupHomology.eq_dโโ_comp_inv, groupHomology.isoShortComplexH1_inv, groupHomology.eq_dโโ_comp_inv_assoc, groupHomology.chainsMap_f_1_comp_chainsIsoโ_assoc, groupHomology.isoCyclesโ_hom_comp_i_apply, groupHomology.lsingle_comp_chainsMap_f, groupHomology.coinvariantsMk_comp_opcyclesIsoโ_inv_apply, groupHomology.dโโ_single_one_fst, groupHomology.dโโ_comp_dโโ, groupHomology.dโโ_single_self_inv_ฯ_sub_inv_self, groupHomology.chainsMap_f_3_comp_chainsIsoโ_assoc, groupHomology.H1ToTensorOfIsTrivial_H1ฯ_single, Module.length_finsupp, groupHomology.inhomogeneousChains.ext_iff, groupHomology.dโโ_apply_mem_cyclesโ, groupHomology.cyclesMap_comp_isoCyclesโ_hom_apply, groupHomology.toCycles_comp_isoCyclesโ_hom_apply, KaehlerDifferential.kerTotal_mkQ_single_mul, groupHomology.eq_dโโ_comp_inv_assoc, groupHomology.mapCyclesโ_hom, groupHomology.isoCyclesโ_inv_comp_iCycles_apply, groupHomology.isoCyclesโ_inv_comp_iCycles_assoc, KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination, Rep.indCoindIso_hom_hom_toLinearMap, groupHomology.cyclesMkโ_eq, groupHomology.chainsMap_f_1_comp_chainsIsoโ, KaehlerDifferential.kerTotal_mkQ_single_smul, groupHomology.H1ฯ_eq_zero_iff, groupHomology.isoCyclesโ_inv_comp_iCycles_assoc, groupHomology.ฯ_comp_H1Iso_hom_assoc, groupHomology.chainsMap_f_2_comp_chainsIsoโ, groupHomology.dโโ_single_one_fst, groupHomology.H2ฯ_comp_map, Representation.FiniteCyclicGroup.coinvariantsKer_leftRegular_eq_ker, groupHomology.H1ฯ_comp_map_assoc, groupHomology.instEpiModuleCatH1ฯ, Rep.linearization_map, groupHomology.instEpiModuleCatH2ฯ, Rep.indCoindIso_inv_hom_toLinearMap, KaehlerDifferential.quotKerTotalEquiv_symm_apply, groupHomology.H1ฯ_comp_map, groupHomology.chainsMap_f_hom, groupHomology.dโโ_apply_mem_cyclesโ, groupHomology.cyclesMkโ_eq, groupHomology.mapCyclesโ_comp_i_assoc, groupHomology.mapCyclesโ_id_comp_apply, groupHomology.H2ฯ_comp_map_apply, Rep.ฮท_def, groupHomology.inhomogeneousChains.d_comp_d, groupHomology.isoCyclesโ_hom_comp_i_assoc, groupHomology.dโโ_eq_zero_of_isTrivial, Representation.coinvariantsToFinsupp_mk_single, Representation.ind_mk, groupHomology.dโโ_single_one_snd, Representation.coinvariantsFinsuppLEquiv_symm_apply, groupHomology.dโโ_comp_dโโ, groupHomology.dโโ_single_one_snd, groupHomology.ฯ_comp_H2Iso_hom_apply, Rep.coinvariantsTensorIndHom_mk_tmul_indVMk, groupHomology.mapCyclesโ_hom, Rep.indToCoind_coindToInd, groupHomology.isoCyclesโ_inv_comp_iCycles, groupHomology.cyclesMap_comp_isoCyclesโ_hom_assoc, groupHomology.isoShortComplexH2_inv, groupHomology.coe_mapCyclesโ, groupHomology.toCycles_comp_isoCyclesโ_hom, groupHomology.chainsMap_f_2_comp_chainsIsoโ_assoc, Rep.indResHomEquiv_symm_apply, groupHomology.mapCyclesโ_comp_i_apply, groupHomology.isoCyclesโ_hom_comp_i, groupHomology.ฯ_comp_H1Iso_hom, groupHomology.isoCyclesโ_inv_comp_iCycles, groupHomology.dโโ_single_inv, groupHomology.mkH1OfIsTrivial_apply, groupHomology.dโโArrowIso_hom_right, groupHomology.dโโ_single, groupHomology.inhomogeneousChains.d_eq, groupHomology.cyclesโIsoOfIsTrivial_inv_apply, groupHomology.eq_dโโ_comp_inv_apply, groupHomology.dโโ_comp_coinvariantsMk_assoc, groupHomology.isoCyclesโ_hom_comp_i, Module.Relations.solutionFinsupp_isPresentation, groupHomology.chainsMap_f_0_comp_chainsIsoโ_apply, groupHomology.lsingle_comp_chainsMap_f_assoc, Representation.ind_apply, mem_finsuppAffineCoords_iff_linearCombination, Rep.coinvariantsTensorIndInv_mk_tmul_indMk, groupHomology.dโโArrowIso_inv_left, groupHomology.H1AddEquivOfIsTrivial_symm_tmul, groupHomology.dโโ_single_ฯ_add_single_inv_mul, groupHomology.eq_dโโ_comp_inv_apply, KaehlerDifferential.quotKerTotalEquiv_apply, groupHomology.dโโ_comp_dโโ_assoc, lcomapDomain_eq_linearProjOfIsCompl, groupHomology.chainsMap_f_1_comp_chainsIsoโ_apply, groupHomology.mapCyclesโ_quotientGroupMk'_epi, groupHomology.mapCyclesโ_comp_i_assoc, Module.presentationFinsupp_var, finiteDimensional_finsupp, instIsSemisimpleModuleFinsupp, groupHomology.dโโ_single, Representation.IndV.hom_ext_iff, groupHomology.isoCyclesโ_hom_comp_i_assoc, groupHomology.comp_dโโ_eq, groupHomology.H2ฯ_eq_zero_iff, groupHomology.ฮดโ_apply, Module.Relations.Solution.ofQuotient_ฯ, groupHomology.H1ฯ_eq_iff, groupHomology.dโโ_comp_dโโ_apply, groupHomology.chainsMap_f, groupHomology.chainsMap_f_2_comp_chainsIsoโ_apply, groupHomology.cyclesMap_comp_isoCyclesโ_hom, KaehlerDifferential.kerTotal_mkQ_single_algebraMap
|
instAddCommMonoid ๐ | CompOp | 1247 mathmath: TensorProduct.finsuppRight_apply, AlgebraicGeometry.AffineSpace.map_Spec_map, snd_sumFinsuppLEquivProdFinsupp, LinearMap.exists_finsupp_nat_of_fin_fun_injective, fst_sumFinsuppLEquivProdFinsupp, groupHomology.ฯ_comp_H2Iso_hom_assoc, KaehlerDifferential.mvPolynomialBasis_apply, AddMonoidAlgebra.supportedEquivFinsupp_apply_apply, support_finset_sum, linearCombination_apply_of_mem_supported, Algebra.PreSubmersivePresentation.jacobiMatrix_naive, MvPolynomial.isJacobsonRing, Module.Free.finsupp, HahnSeries.instNoZeroDivisorsFinsuppNat, groupHomology.mapCyclesโ_comp_assoc, Orthonormal.inner_left_finsupp, AlgebraicGeometry.AffineSpace.map_toSpecMvPoly_assoc, mapRange.linearEquiv_refl, CommRingCat.HomTopology.mvPolynomialHomeomorph_apply_snd, MvPolynomial.radical_le_vanishingIdeal_zeroLocus, Module.Relations.Solution.ofฯ'_var, Module.Basis.end_repr_apply, Algebra.Presentation.differentials.commโโ_single, MvPolynomial.aeval_X_left, mem_supported_support, AlgebraicIndependent.of_aeval, Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, MvPolynomial.rTensor_apply_tmul_apply, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv, floorDiv_def, Algebra.Generators.H1Cotangent.ฮดAux_mul, Algebra.Presentation.naive_toGenerators, restrictDom_apply, groupHomology.boundariesโ_le_cyclesโ, instIsOrderedCancelAddMonoidLexFinsupp, QuadraticMap.sum_polar_sub_repr_sq, MvPolynomial.scalarRTensor_apply_monomial_tmul, Module.basisUnique_repr_eq_zero_iff, MvPolynomial.isOpenMap_comap_C, finsuppTensorFinsupp_apply, MvPolynomial.universalFactorizationMap_comp_map, Representation.ofMulActionSelfAsModuleEquiv_symm_apply, PolynomialModule.smul_def, IsBaseChange.finsuppPow, lmapDomain_id, NumberField.Units.fun_eq_repr, Algebra.PreSubmersivePresentation.ofHasCoeffs_map, TensorProduct.equivFinsuppOfBasisLeft_symm_apply, IsBaseChange.basis_repr_comp_apply, Module.DualBases.basis_repr_symm_apply, Module.Basis.toDual_linearCombination_left, LinearMap.prodOfFinsuppNat_injective, sumFinsuppLEquivProdFinsupp_apply, MvPolynomial.derivation_eq_of_forall_mem_vars, Algebra.Generators.cotangentSpaceBasis_apply, IsAdjoinRootMonic.coeff_apply, Module.Relations.Solution.surjective_ฯ_iff_span_eq_top, supportedEquivFinsupp_symm_single, MvPolynomial.IsWeightedHomogeneous.pderiv, Rep.coindToInd_of_support_subset_orbit, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply, Representation.finsupp_apply, LinearMap.toMatrix_apply', mapRange.linearEquiv_toAddEquiv, groupHomology.mapCyclesโ_comp_apply, AlgebraicGeometry.AffineSpace.SpecIso_hom_appTop, MonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_apply, Matrix.repr_toLin, MvPowerSeries.coeff_pow, KaehlerDifferential.mvPolynomialBasis_repr_D_X, multiset_sum_sum_index, PowerBasis.repr_pow_isIntegral, linearCombination_id_surjective, TensorProduct.sum_tmul_basis_right_injective, MvPolynomial.iterToSum_sumToIter, isOrderedAddMonoid, Representation.freeLift_single_single, Representation.finsuppTensorLeft_apply_tmul, Representation.LinearizeMonoidal.ฮต_ฮท, rank_finsupp, LinearIndependent.linearCombination_repr, exteriorPower.basis_repr_ne, MvPolynomial.aeval_X_left_apply, Algebra.Presentation.differentials.commโโ, rank_finsupp_self, Representation.ofCoinvariantsTprodLeftRegular_mk_tmul_single, Module.Basis.mk_repr, span_single_eq_top, Module.Flat.finsupp, MvPolynomial.monomial_finsupp_sum_index, Module.Relations.Solution.injective_fromQuotient_iff_ker_ฯ_eq_span, linearEquivFunOnFinite_symm_coe, Module.Basis.repr_isUnitSMul, StandardEtalePresentation.toPresentation_algebra_smul, Representation.linearize_single, Span.repr_def, MvPolynomial.image_comap_C_basicOpen, groupHomology.mem_cyclesโ_iff, coe_ceilDiv_def, Rep.coindToInd_indToCoind, groupHomology.cyclesMap_comp_isoCyclesโ_hom, chevalley_mvPolynomial_mvPolynomial, linearIndependent_iff_injective_finsuppLinearCombination, MvPolynomial.scalarRTensor_apply_X_tmul_apply, groupHomology.mapCyclesโ_comp_assoc, Algebra.FormallyUnramified.finite_of_free_aux, Module.Basis.prod_repr_inl, groupHomology.toCycles_comp_isoCyclesโ_hom_assoc, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, MvPolynomial.optionEquivLeft_apply, MvPolynomial.instIsScalarTower, Module.Relations.Solution.surjective_fromQuotient_iff_surjective_ฯ, MvPolynomial.prime_rename_iff, AddMonoidAlgebra.supportedEquivFinsupp_apply_support_val, linearCombination_zero_apply, mem_supported, MvPolynomial.evalโ_prod, Module.Basis.repr_self_apply, groupHomology.mem_cyclesโ_of_comp_eq_dโโ, mem_span_iff_linearCombination, MvPolynomial.iterToSum_C_X, MvPolynomial.map_evalโ, IsLocalFrameOn.coeff_apply_of_mem, Algebra.SubmersivePresentation.ofSubsingleton_algebra_algebraMap, setBasisOfLinearIndependentOfCardEqFinrank_repr_apply, Algebra.Presentation.differentials.homโ_single, LinearMap.sum_repr_mul_repr_mulโโ, groupHomology.ฮดโ_apply, MvPolynomial.pderiv_one, MvPolynomial.mkDerivation_X, MvPolynomial.pderiv_mul, Representation.ofMulAction_apply, Colex.isOrderedCancelAddMonoid, Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp, Ideal.finsuppTotal_apply_eq_of_fintype, groupHomology.isoCyclesโ_inv_comp_iCycles_apply, KaehlerDifferential.quotKerTotalEquiv_symm_comp_D, strongRankCondition_iff_forall_not_injective, IntermediateField.LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, MvPolynomial.aeval_ite_mem_eq_self, Algebra.SubmersivePresentation.map_jacobianOfHasCoeffs, MvPolynomial.evalโHom_C_id_eq_joinโ, finsuppTensorFinsupp'_symm_single_eq_tmul_single_one, Rep.finsuppToCoinvariantsTensorFree_single, Module.Relations.Solution.IsPresentation.linearEquiv_symm_var, Algebra.Generators.algebraMap_surjective, MvPolynomial.pow_idealOfVars, MvPolynomial.joinโ_comp_map, PolynomialLaw.toFun_eq_rTensor_ฯ_toFun', LinearMap.leftInverse_splittingOfFinsuppSurjective, Representation.ofMulActionSubsingletonEquivTrivial_symm_apply, linearIndependent_iff_ker, SkewMonoidAlgebra.ofFinsupp_sum, Representation.finsuppTensorRight_apply_tmul, Pi.counit_comp_finsuppLcoeFun, curryLinearEquiv_symm_apply_apply, Polynomial.Bivariate.Polynomial.Bivariate.pderiv_one_equivMvPolynomial, MvPolynomial.eval_evalโ, llift_apply, linearCombination_smul, MvPolynomial.evalโHom_C_eq_bindโ, Representation.leftRegularTensorTrivialIsoFree_symm_apply_single_single, groupHomology.cyclesโ_eq_top_of_isTrivial, Bundle.Trivialization.localFrame_coeff_eq_coeff, Algebra.PreSubmersivePresentation.ofHasCoeffs_relation, AddCommMonCat.free_map, MvPolynomial.mem_pow_idealOfVars_iff, Ideal.finsuppTotal_apply, MvPolynomial.X_prime, Representation.LinearizeMonoidal.ฮผ_apply_single_single, TensorProduct.equivFinsuppOfBasisLeft_apply_tmul_apply, lmapDomain_linearCombination, range_mapRange_linearMap, Module.Basis.repr_algebraMap, Multiset.support_sum_subset, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, MvPolynomial.pderiv_rename, iInf_ker_lapply_le_bot, basis_repr, Matrix.toBilin_apply, IsLocalRing.basisQuotient_repr, Module.Relations.surjective_toQuotient, Module.End.ringHomEndFinsupp_apply_apply, Representation.ofMulAction_single, groupHomology.single_one_snd_sub_single_one_fst_mem_boundariesโ, linearCombination_one_tmul, Finset.support_sum_subset, Module.Basis.map_repr, groupHomology.cyclesโIsoOfIsTrivial_hom_apply, Representation.coinvariantsFinsuppLEquiv_apply, LinearMap.toMatrixAlgEquiv_apply, Algebra.TensorProduct.basis_repr_tmul, lmapDomain_comp, NumberField.mixedEmbedding.stdBasis_apply_isComplex_snd, supported_inter, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_appTop_coord, LinearEquiv.finsuppUnique_symm_apply, span_le_supported_biUnion_support, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over_assoc, LinearMap.BilinForm.apply_eq_dotProduct_toMatrix_mulVec, KaehlerDifferential.kerTotal_eq, span_image_eq_map_linearCombination, Algebra.PreSubmersivePresentation.ofHasCoeffs_ฯ', Algebra.Presentation.quotientEquiv_symm, LinearIndependent.repr_eq_single, HahnSeries.toMvPowerSeries_symm_apply_coeff, IsAdjoinRootMonic.basis_repr, Representation.leftRegular_norm_eq_zero_iff, supported_eq_span_single, TensorProduct.finsuppLeft_smul', MvPolynomial.sumAlgEquiv_comp_rename_inr, groupHomology.mapCyclesโ_id_comp_assoc, filter_sum, Algebra.TensorProduct.basisAux_map_smul, Pi.basis_repr_single, Module.Relations.Solution.fromQuotient_toQuotient, TensorProduct.equivFinsuppOfBasisRight_apply_tmul, MvPolynomial.X_mul_pderiv_monomial, Module.Basis.ofEquivFun_repr_apply, supported_univ, Algebra.Generators.naive_val, Module.Basis.sumQuot_repr_left, MonomialOrder.leadingCoeff_prod_of_regular, groupHomology.mapCyclesโ_comp, Representation.ofMulAction_self_smul_eq_mul, Module.Basis.reindexRange_repr', Algebra.Generators.algebraMap_apply, Module.Basis.reindexRange_repr, AddMonoidAlgebra.coeff_sum, sigmaFinsuppLEquivPiFinsupp_symm_apply, TensorProduct.equivFinsuppOfBasisLeft_apply_tmul, PiTensorProduct.ofFinsuppEquiv'_tprod_single, TensorProduct.equivFinsuppOfBasisLeft_symm, instIsIntegralMvPolynomial, MvPolynomial.derivation_eq_zero_of_forall_mem_vars, Submodule.mulLeftMap_apply, TensorProduct.finsuppScalarRight_apply, Algebra.Generators.compLocalizationAwayAlgHom_X_inl, Module.Relations.Solution.ofQuotient_var, groupHomology.mapCyclesโ_comp_i, TensorProduct.finsuppScalarRight_apply_tmul, Polynomial.derivativeFinsupp_apply_toFun, Algebra.Presentation.naive_relation, LieAlgebra.LoopAlgebra.toFinsupp_symm_single, Module.Basis.repr_smul, finsuppTensorFinsupp'_single_tmul_single, mapDomain.coe_linearEquiv, AddMonoidAlgebra.grade_eq_lsingle_range, NumberField.canonicalEmbedding.integralBasis_repr_apply, ChevalleyThm.chevalley_mvPolynomialC, lcoeFun_comp_lsingle, Finset.sum_apply', isOrderedCancelAddMonoid, Algebra.Generators.algebraMap_eq, lcoeFun_apply, Algebra.SubmersivePresentation.ofSubsingleton_relation, basisOfLinearIndependentOfCardEqFinrank_repr_apply, StandardEtalePair.equivMvPolynomialQuotient_symm_apply, Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial, PiTensorProduct.ofFinsuppEquiv_tprod_single, Module.Relations.range_map, Representation.LinearizeMonoidal.ฮผ_comp_assoc, MvPolynomial.transcendental_supported_X_iff, MvPolynomial.vanishingIdeal_pointToPoint, Module.Basis.SmithNormalForm.repr_apply_embedding_eq_repr_smul, MvPolynomial.algebraicIndependent_polynomial_aeval_X, groupHomology.single_one_fst_sub_single_one_snd_mem_boundariesโ, floorDiv_apply, Representation.coinvariantsTprodLeftRegularLEquiv_apply, finsuppTensorFinsuppLid_symm_single_smul, ker_mapRange, MvPolynomial.optionEquivRight_symm_apply, groupHomology.mapCyclesโ_id_comp, MvPolynomial.scalarRTensor_apply_tmul, supported_comap_lmapDomain, finsuppTensorFinsupp'_symm_single_mul, LinearMap.polyCharpolyAux_map_eval, ZSpan.repr_ceil_apply, domLCongr_trans, MvPolynomial.eval_prod, lp.zeroBasis_repr_apply, Algebra.Presentation.comp_aeval_relation_inl, Module.Basis.addSubgroupOfClosure_repr_apply, MvPolynomial.totalDegree_finset_prod, Module.Basis.span_repr_eq_single, sumFinsuppLEquivProdFinsupp_symm_apply, Module.Basis.repr_range, Representation.ofMulActionSubsingletonEquivTrivial_apply, basis_toMatrix_basisFun_mul, instFinitePresentationFinsupp, Algebra.SubmersivePresentation.jacobianRelations_spec, MvPolynomial.pderiv_sumToIter, Submodule.LinearDisjoint.linearIndependent_right_of_flat, TensorProduct.finsuppLeft_symm_apply_single, linearEquivFunOnFinite_symm_apply, MonomialOrder.coeff_prod_sum_degree, finsuppTensorFinsupp'_apply_apply, finset_sum_apply, Rep.coinvariantsTensorFreeLEquiv_apply, PiTensorProduct.ofFinsuppEquiv_symm_single_tprod, leftInverse_lcomapDomain_mapDomain, Module.Basis.reindexRange_repr_self, groupHomology.toCycles_comp_isoCyclesโ_hom_apply, TensorProduct.toIntegralClosure_mvPolynomial_bijective, Algebra.PreSubmersivePresentation.jacobiMatrix_apply, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_algebraMap_apply, MvPolynomial.quotient_map_C_eq_zero, linearCombination_linear_comp, groupHomology.mapCyclesโ_comp_i, MvPolynomial.iterToSum_X, Module.Basis.repr_eq_iff, mem_submodule_iff, Module.Basis.sumQuot_repr_inl, MvPolynomial.pow_idealOfVars_eq_span, groupHomology.boundariesOfIsBoundaryโ_coe, IsBaseChange.of_basis, MvPolynomial.commAlgEquiv_C, Algebra.Generators.cotangentSpaceBasis_repr_tmul, MvPolynomial.commAlgEquiv_X, comul_comp_lapply, Algebra.TensorProduct.equivFinsuppOfBasis_apply, sumFinsuppLEquivProdFinsupp_symm_inl, AlgebraicIndependent.lift_reprField, Module.Basis.repr_linearCombination, ceilDiv_apply, Algebra.TensorProduct.equivFinsuppOfBasis_symm_apply, MvPolynomial.rTensor_apply_X_tmul, Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation, MvPolynomial.pderiv_X, PiLp.basisFun_repr, MvPolynomial.uniqueFactorizationMonoid, Algebra.Generators.H1Cotangent.ฮดAux_toAlgHom, Representation.LinearizeMonoidal.ฮต_one, linearCombination_single_index, groupHomology.single_one_fst_sub_single_one_fst_mem_boundariesโ, lift_apply, LinearIndependent.linearCombinationEquiv_apply_coe, Module.Relations.Solution.range_ฯ, IsLocalization.Away.mvPolynomialQuotientEquiv_apply, Representation.LinearizeMonoidal.ฮผ_comp_rTensor, TensorProduct.equivFinsuppOfBasisRight_apply_tmul_apply, Algebra.Presentation.naive_relation_apply, subtypeDomain_finsupp_sum, groupHomology.mapCyclesโ_id_comp_apply, LinearIndependent.linearCombination_comp_repr, MvPolynomial.rename_evalโ, Representation.LinearizeMonoidal.ฮผ_ฮด, Polynomial.derivativeFinsupp_apply_apply, MvPolynomial.finitePresentation_universalFactorizationMap, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, MvPolynomial.totalDegree_multiset_prod, Algebra.Presentation.differentials.surjective_homโ, MvPolynomial.rTensor_apply_tmul, codisjoint_supported_supported, supported_union, Module.Basis.linearCombination_dualBasis, groupHomology.ฯ_comp_H2Iso_hom, FiniteDimensional.basisSingleton_repr_apply, Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom, sum_sum_index', MvPolynomial.bindโ_id, Module.Basis.equivFunL_symm_apply_repr, PowerBasis.repr_gen_pow_isIntegral, Rep.coindToInd_apply, groupHomology.mapCyclesโ_comp_i_apply, Polynomial.derivativeFinsupp_derivative, MvPolynomial.sumAlgEquiv_comp_rename_inl, Subalgebra.LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply, lsum_single, KaehlerDifferential.ker_map, ceilDiv_def, groupHomology.mapCyclesโ_comp, LinearMap.CompatibleSMul.finsupp_dom, LinearMap.BilinForm.sum_repr_mul_repr_mul, linearEquivFunOnFinite_single, supported_iInter, Module.Basis.mulOpposite_repr_op, Module.Basis.smulTower'_repr_mk, single_finset_sum, instIsLocalizedModuleFinsuppLinearMap, Matrix.GeneralLinearGroup.toLin'_apply, Representation.linearizeTrivialIso_apply, counit_comp_lsingle, TensorProduct.finsuppScalarRight_smul, MvPolynomial.IsWeightedHomogeneous.sum_weight_X_mul_pderiv, groupHomology.coe_mapCyclesโ, finsuppTensorFinsupp_single, MonoidAlgebra.coeffLinearEquiv_symm_apply, MvPolynomial.pderiv_def, AlgebraicGeometry.AffineSpace.SpecIso_inv_appTop_coord, groupHomology.H1ฯ_comp_map_apply, Nat.ceilRoot_def, MvPolynomial.mem_pow_idealOfVars_iff', Module.Basis.repr_reindex, support_sum, Module.subsingletonEquiv_symm_apply, IsLocalizedModule.map_linearCombination, rank_finsupp_self', Module.Basis.algebraMapCoeffs_repr_apply_toFun, Algebra.PreSubmersivePresentation.naive_toPresentation, LinearMap.toMatrix_mulVec_repr, filter_eq_sum, finsuppTensorFinsupp'_symm_single_eq_single_one_tmul, Matrix.toLin_apply_eq_zero_iff, linearDepOn_iff, groupHomology.toCycles_comp_isoCyclesโ_hom_assoc, Module.Basis.algebraMapCoeffs_repr_apply_apply, Matrix.toLinearMapโโโ_apply, lcomapDomain_apply, lhom_ext'_iff, LinearMap.BilinForm.dualBasis_repr_apply, IsIsotypicOfType.linearEquiv_finsupp, linearIndepOn_iff_disjoint, mapRange.linearMap_apply, Module.Basis.sumQuot_repr_inl_of_mem, mapRange.linearEquiv_symm, Module.End.ringEquivEndFinsupp_apply_apply_apply, Submodule.set_smul_eq_map, lcongr_symm, TensorProduct.finsuppScalarRight_apply_tmul_apply, MvPolynomial.monomial_mem_pow_idealOfVars_iff, Module.Basis.repr_symm_single, Representation.finsuppToCoinvariants_single_mk, groupHomology.H2ฯ_comp_map_assoc, apply_eq_dotProduct_toMatrixโ_mulVec, MonoidAlgebra.ofCoeff_finsuppSum, TensorProduct.finsuppLeft_apply, MvPolynomial.irreducible_sumSMulX, support_ceilDiv_subset, finsuppTensorFinsuppRid_symm_single_smul, finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply, Representation.LinearizeMonoidal.ฮท_toLinearMap, AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly_assoc, Module.Basis.restrictScalars_repr_apply, Orthonormal.inner_finsupp_eq_sum_right, Representation.finsupp_single, Algebra.Generators.instIsScalarTowerRing, span_eq_range_linearCombination, Module.Basis.equivFunL_apply, isCompl_range_lmapDomain_span, Algebra.Generators.cotangentRestrict_bijective_of_isCompl, MvPolynomial.combinatorial_nullstellensatz_exists_linearCombination, MvPolynomial.finite_universalFactorizationMap, Module.Relations.map_single, MvPolynomial.rTensorAlgHom_toLinearMap, MvPolynomial.isRegular_prod_X, MvPolynomial.coeff_sumSMulX, MvPolynomial.universalFactorizationMapPresentation_map, linearCombinationOn_range, Algebra.TensorProduct.basisAux_tmul, Module.Basis.singleton_repr, KaehlerDifferential.derivationQuotKerTotal_apply, linearIndependent_single_of_ne_zero, LinearMap.polyCharpolyAux_map_eq_charpoly, LinearMap.polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff, MvPolynomial.coeff_prod_X_pow, CommRingCat.HomTopology.mvPolynomialHomeomorph_symm_apply_hom, LinearMap.toMatrix_transpose_apply, Pi.basis_repr, AlgebraicGeometry.AffineSpace.map_toSpecMvPoly, MvPolynomial.mk_eq_evalโ, Algebra.Generators.H1Cotangent.ฮดAux_ofComp, groupHomology.mapCyclesโ_comp_apply, Module.Relations.Quotient.linearMap_ext_iff, LinearIndependent.span_repr_eq, Algebra.Presentation.differentials.commโโ', InnerProductSpace.gramSchmidt_triangular, QuadraticAlgebra.basis_repr_apply, PowerBasis.repr_mul_isIntegral, MvPolynomial.pointToPoint_zeroLocus_le, Module.Basis.toDual_eq_repr, exists_integral_inj_algHom_of_quotient, Module.Basis.sum_repr_mul_repr, linearCombination_apply, Nat.factorization_ceilRoot, Subalgebra.LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent, NumberField.integralBasis_repr_apply, exists_finite_inj_algHom_of_fg, groupHomology.H2ฯ_eq_iff, Submodule.mulRightMap_eq_mulMap_comp, Module.Basis.linearMap_repr_apply, AddMonoidAlgebra.coeffLinearEquiv_apply, groupHomology.H1AddEquivOfIsTrivial_single, MultilinearMap.freeFinsuppEquiv_def, groupHomology.isoCyclesโ_hom_comp_i_apply, Algebra.Generators.toAlgHom_ofComp_rename, linearCombination_embDomain, Algebra.FinitePresentation.iff, LinearMap.splittingOfFinsuppSurjective_injective, MonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_support_val, Submodule.range_lsum_smul, Representation.LinearizeMonoidal.assoc_comp_ฮด, Representation.ofMulActionSelfAsModuleEquiv_apply, KaehlerDifferential.kerTotal_map, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, PiTensorProduct.ofFinsuppEquiv_apply, MvPolynomial.support_esymm', TensorProduct.finsuppScalarRight_symm_apply_single, groupHomology.cyclesMap_comp_isoCyclesโ_hom_assoc, Module.Basis.mem_span_image, Representation.linearizeOfMulActionIso_apply, LinearMap.CompatibleSMul.finsupp_cod, MvPolynomial.mkโ_eq_aeval, MvPolynomial.derivation_C, NumberField.mixedEmbedding.stdBasis_apply_isComplex_fst, Module.Basis.localizationLocalization_repr_algebraMap, instIsAlgebraicMvPolynomialOfNoZeroDivisors, groupHomology.inhomogeneousChains.d_single, Module.Basis.dualBasis_apply, Algebra.Generators.ฯ_smul, apply_eq_star_dotProduct_toMatrixโ_mulVec, MvPolynomial.mkDerivation_monomial, Complex.coe_basisOneI_repr, linearCombination_single, Module.Presentation.CokernelData.ฯ_lift, Module.Basis.reindexFinsetRange_repr_self, Algebra.Generators.comp_localizationAway_ker, MvPolynomial.prime_C_iff, Orthonormal.inner_right_finsupp, LinearMap.toMatrix_transpose_apply', Module.Basis.repr_symm_single_one, groupHomology.isBoundaryโ_iff, MvPolynomial.universalFactorizationMapPresentation_relation, Algebra.PreSubmersivePresentation.aevalDifferential_single, MvPolynomial.aeval_id_rename, Representation.LinearizeMonoidal.rTensor_comp_ฮด, coe_basis, mapRange.linearEquiv_toLinearMap, Submodule.smul_top_eq_range_lsum, LinearMap.toMatrix_smulRight, counit_single, NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul, RootPairing.Base.toCoweightBasis_repr_coroot, AdjoinRoot.powerBasisAux'_repr_symm_apply, MvPowerSeries.coeff_prod, groupHomology.mapCyclesโ_id_comp_assoc, coe_finset_sum, groupHomology.ฯ_comp_H1Iso_hom_apply, Representation.freeLift_toLinearMap, restrictDom_comp_subtype, lsum_apply, Basis.multilinearMap_apply_apply, Rep.standardComplex.d_of, MvPolynomial.vars_prod, Module.Basis.coe_finTwoProd_repr, MvPolynomial.sumToIter_iterToSum, Representation.LinearizeMonoidal.ฮผ_comp_lTensor, linearCombination_unique, groupHomology.toCycles_comp_isoCyclesโ_hom, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul, coe_lsum, groupHomology.cyclesMap_comp_isoCyclesโ_hom_apply, linearCombination_mapDomain, Span.finsupp_linearCombination_repr, MvPolynomial.coeff_linearCombination_X_pow, groupHomology.mapCyclesโ_id_comp, MvPolynomial.prod_X_pow_eq_monomial, lapply_comp_lsingle_same, instIsCocomm, Representation.LinearizeMonoidal.rightUnitor_ฮด, MvPolynomial.universalFactorizationMapPresentation_algebra_algebraMap, IsAdjoinRootMonic.coeff_apply_lt, DirectSum.IsInternal.collectedBasis_repr_of_mem_ne, MvPolynomial.frobenius_zmod, Module.Basis.toMatrix_apply, KaehlerDifferential.mvPolynomialBasis_repr_apply, LinearMap.exists_finsupp_nat_of_prod_injective, sigmaFinsuppLEquivPiFinsupp_apply, finsuppTensorFinsuppRid_single_tmul_single, LinearIndependent.linearCombinationEquiv_symm_apply, Module.DualBases.basis_repr_apply, LieAlgebra.LoopAlgebra.toFinsupp_single_tmul, Algebra.toMatrix_lmul', Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul, Representation.LinearizeMonoidal.ฮท_single, AlgebraicGeometry.AffineSpace.map_SpecMap, Module.Relations.Solution.isPresentation_iff, Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, Polynomial.derivativeFinsupp_map, disjoint_supported_supported, llift_symm_apply, TensorProduct.finsuppScalarLeft_apply_tmul_apply, DividedPowerAlgebra.submodule_span_prod_dp_eq_top, groupHomology.isoCyclesโ_hom_comp_i_apply, AddMonoidAlgebra.supported_eq_map, MvPolynomial.pderiv_C_mul, Polynomial.homogenize_finsetProd, Module.Basis.symmetricAlgebra_repr_apply, supportedEquivFinsupp_symm_apply_coe_support_val, ZLattice.exists_forall_abs_repr_le_norm, ringKrullDim_add_natCard_le_ringKrullDim_mvPolynomial, Matrix.toLin_apply, Representation.finsuppTensorRight_symm_apply_single, mapDomain_finset_sum, AlgebraicGeometry.AffineSpace.SpecIso_inv_over_assoc, Algebra.Generators.self_algebra_smul, MultilinearMap.freeFinsuppEquiv_apply, linearCombination_range, Algebra.Generators.toKaehler_tmul_D, Submodule.mulRightMap_apply, finsuppLEquivDirectSum_single, MvPolynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing, Orthonormal.inner_finsupp_eq_sum_left, comul_single, LinearIndependent.finsuppLinearCombination_injective, Representation.ker_leftRegular_norm_eq, lapply_apply, groupHomology.single_ฯ_self_add_single_inv_mem_boundariesโ, groupHomology.H1ToTensorOfIsTrivial_H1ฯ_single, MvPolynomial.comap_C_surjective, mapRange.linearMap_comp, MvPolynomial.evalโ_eta, MonoidAlgebra.coeffLinearEquiv_apply, AlgebraicIndependent.liftAlgHom_comp_reprField, AddMonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_support_val, support_floorDiv_subset, linearCombination_restrict, Algebra.Presentation.differentials.commโโ, Module.Basis.sumQuot_repr_inr_of_mem, Module.IsLocalRing.linearCombination_bijective_of_flat, coe_basisSingleOne, coe_lmapDomain, MvPolynomial.finSuccEquiv_eq, indicator_eq_sum_attach_single, lapply_comp_lsingle_of_ne, groupHomology.cyclesOfIsCycleโ_coe, Module.Basis.repr_injective, RingHom.IsStandardSmooth.exists_etale_mvPolynomial, LinearIndependent.repr_range, MvPolynomial.ker_evalโHom_universalFactorizationMap, Module.Basis.repr_apply_eq, MvPolynomial.monomial_sum_index, linearCombination_comp, MvPolynomial.degrees_prod_le, LinearMap.polyCharpolyAux_map_aeval, MvPolynomial.monic_monomial_eq, Pi.counit_coe_finsupp, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply, MvPolynomial.pderiv_monomial_single, MvPolynomial.degreeOf_prod_eq, groupHomology.dโโ_apply_mem_cyclesโ, NumberField.inverse_basisMatrix_mulVec_eq_repr, range_linearCombination, supported_empty, MvPolynomial.IsHomogeneous.aeval, Module.Relations.ker_toQuotient, groupHomology.cyclesMap_comp_isoCyclesโ_hom_apply, bilinearCombination_apply, groupHomology.toCycles_comp_isoCyclesโ_hom_apply, apply_linearCombination, Module.Relations.Solution.IsPresentation.surjective_ฯ, Module.finite_finsupp_iff, MvPolynomial.quotientEquivQuotientMvPolynomial_leftInverse, linearIndependent_single_iff, MultilinearMap.freeFinsuppEquiv_single, MonoidAlgebra.coeff_finsuppSum, Module.Basis.end_repr_symm_apply, InnerProductSpace.toMatrix_rankOne, MvPolynomial.rTensor_symm_apply_single, MvPolynomial.pderiv_X_of_ne, MvPolynomial.prod_X_add_C_coeff, Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, Representation.free_single_single, MvPolynomial.pderiv_monomial, lcongr_symm_single, Module.Basis.apply_eq_iff, Module.Flat.iff_forall_exists_factorization, sigmaFinsuppLequivDFinsupp_symm_apply, Module.Relations.Solution.ฯ_comp_map, domLCongr_symm, groupHomology.mem_cyclesโ_of_mem_boundariesโ, MvPolynomial.quotient_mk_comp_C_injective, setBasisOfTopLeSpanOfCardEqFinrank_repr_apply, LinearMap.polyCharpolyAux_coeff_eval, AlgebraicClosure.Monics.map_eq_prod, MonomialOrder.degree_prod_le, MonoidAlgebra.supportedEquivFinsupp_apply_support_val, disjoint_lsingle_lsingle, linearCombination_comp_addSingleEquiv, Matrix.toLinAlgEquiv_apply, Module.Basis.coe_ofRepr, Module.equiv_free_prod_directSum, codisjoint_supported_supported_iff, MonomialOrder.div_set, MvPolynomial.aeval_eq_bindโ, TensorProduct.equivFinsuppOfBasisRight_apply, Submodule.mulLeftMap_eq_mulMap_comp, Finset.sum_single_ite, groupHomology.mapCyclesโ_hom, groupHomology.isoCyclesโ_inv_comp_iCycles_apply, groupHomology.isoCyclesโ_inv_comp_iCycles_assoc, KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination, univ_sum_single, mapRange.linearMap_id, Rep.indCoindIso_hom_hom_toLinearMap, lcongr_single, Module.Flat.exists_factorization_of_apply_eq_zero_of_free, Matrix.toLinearMapโ_apply, linearEquivFunOnFinite_apply, ZLattice.abs_repr_lt_of_norm_lt, MonoidAlgebra.supportedEquivFinsupp_apply_apply, groupHomology.cyclesMkโ_eq, LieAlgebra.LoopAlgebra.residuePairing_apply_apply, MvPolynomial.rTensor_apply_monomial_tmul, MvPolynomial.IsWeightedHomogeneous.prod, Algebra.Generators.repr_CotangentSpaceMap, Module.Basis.dualBasis_repr, groupHomology.H1ฯ_eq_zero_iff, DividedPowerAlgebra.dp_sum_smul, groupHomology.isoCyclesโ_inv_comp_iCycles_assoc, sumFinsuppLEquivProdFinsupp_symm_inr, groupHomology.ฯ_comp_H1Iso_hom_assoc, Pi.comul_coe_finsupp, MvPolynomial.pderiv_pow, supported_mono, AddMonoidAlgebra.coeffLinearEquiv_symm_apply, groupHomology.H2ฯ_comp_map, NumberField.mixedEmbedding.stdBasis_apply_isReal, MvPowerSeries.algebraMap_apply', HahnSeries.coeff_toMvPowerSeries_symm, groupHomology.mem_cyclesโ_of_mem_boundariesโ, Module.Basis.linearCombination_repr, union_support_maximal_linearIndependent_eq_range_basis, Representation.LinearizeMonoidal.leftUnitor_ฮด, StandardEtalePresentation.toPresentation_ฯ', Module.FinitePresentation.out, Representation.finsuppTensorLeft_symm_apply_single, MvPolynomial.isIntegral_iff_isIntegral_coeff, witt_structure_prop, Nat.factorization_floorRoot, Module.Basis.linearCombination_coord, Representation.FiniteCyclicGroup.coinvariantsKer_leftRegular_eq_ker, coe_floorDiv, MvPolynomial.evalโHom_eq_bindโ, Module.Basis.tensorAlgebra_repr_apply, Nat.floorRoot_def, MvPolynomial.prod_C_add_X_eq_sum_esymm, Module.projective_def', Algebra.Presentation.instFinitePresentationModelOfHasCoeffsOfFinite, MvPolynomial.evalโ_map_comp_C, groupHomology.H1ฯ_comp_map_assoc, Representation.coinvariantsTprodLeftRegularLEquiv_symm_apply, MvPolynomial.optionEquivRight_apply, Module.Basis.equivFun_apply, MvPolynomial.finSuccEquiv_apply, TensorProduct.finsuppScalarLeft_apply_tmul, groupHomology.instEpiModuleCatH1ฯ, Module.Basis.mulOpposite_repr_eq, Module.Basis.coe_repr_symm, Module.Basis.smulTower'_repr, Module.Relations.toQuotient_map_apply, LinearMap.snd_prodOfFinsuppNat, LinearEquiv.finsuppUnique_apply, linearCombination_fin_zero, Module.Relations.Solution.ฯ_relation, exteriorPower.basis_repr_apply, linearEquivFunOnFinite_symm_single, LinearIndependent.repr_eq, Module.Basis.toMatrix_update, PiLp.basis_toMatrix_basisFun_mul, single_multiset_sum, groupHomology.single_one_snd_sub_single_one_snd_mem_boundariesโ, linearCombination_equivMapDomain, DividedPowerAlgebra.dp_sum, mapRange.linearEquiv_apply, Multiset.support_sum_eq, groupHomology.instEpiModuleCatH2ฯ, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom_appTop, AddMonoidAlgebra.coeff_finsuppSum, Module.Basis.baseChange_repr_tmul, MvPolynomial.sumAlgEquiv_apply, Algebra.SubmersivePresentation.exists_sum_eq_ฯ_jacobian_mul_ฯ_jacobian_inv_sub_one, ZSpan.repr_fract_apply, finsuppLEquivDirectSum_apply, Algebra.Generators.ker_comp_eq_sup, Algebra.TensorProduct.basis_repr_symm_apply, Rep.indCoindIso_inv_hom_toLinearMap, LinearMap.polyCharpoly_map_eq_charpoly, MvPolynomial.sumToIter_Xr, Orthonormal.inner_finsupp_eq_zero, Submodule.mulLeftMap_apply_single, single_mem_span_single, KaehlerDifferential.quotKerTotalEquiv_symm_apply, finsuppTensorFinsuppLid_apply_apply, Representation.LinearizeMonoidal.ฮท_ฮต, LinearIndependent.repr_ker, Representation.LinearizeMonoidal.lTensor_comp_ฮด, MvPolynomial.algebraicIndependent_X, Representation.leftRegularTensorTrivialIsoFree_apply_single_tmul_single, groupHomology.H1ฯ_comp_map, groupHomology.chainsMap_f_hom, groupHomology.dโโ_apply_mem_cyclesโ, mapRange.linearMap_toAddMonoidHom, MvPolynomial.esymmAlgHom_apply, MvPolynomial.monomial_eq, QuaternionAlgebra.coe_basisOneIJK_repr, Representation.LinearizeMonoidal.ฮด_apply_single, MonoidAlgebra.supported_eq_map, MvPolynomial.rename_prod_mk_evalโ, Ideal.range_finsuppTotal, AlgebraicIndependent.aevalEquivField_apply_coe, Lex.isOrderedCancelAddMonoid, MonoidAlgebra.ofCoeff_sum, IsTranscendenceBasis.mvPolynomial, groupHomology.boundariesOfIsBoundaryโ_coe, MvPolynomial.pderiv_map, groupHomology.cyclesMkโ_eq, finsuppLequivDFinsupp_apply_apply, liftAddHom_singleAddHom, Representation.linearizeOfMulActionIso_symm_apply, Algebra.Generators.naive_ฯ, MvPolynomial.esymm_eq_sum_monomial, groupHomology.mapCyclesโ_comp_i_assoc, toMultiset_sum, domLCongr_apply, curryLinearEquiv_apply, QuadraticMap.apply_linearCombination', Finset.support_sum_eq, groupHomology.mapCyclesโ_id_comp_apply, Representation.linearizeMap_single, finsuppTensorFinsupp_symm_single, AlgebraicGeometry.AffineSpace.isoOfIsAffine_hom, linearCombination_linearCombination, Module.Relations.Solution.IsPresentation.desc_comp_ฯ, MvPolynomial.pderiv_inr_universalFactorizationMap_X, MvPolynomial.sumAlgEquiv_symm_apply, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul, lift_symm_apply, MvPolynomial.instIsPushout_1, groupHomology.H2ฯ_comp_map_apply, NumberField.mixedEmbedding.latticeBasis_repr_apply, MvPolynomial.C_mem_pow_idealOfVars_iff, Module.Basis.ext_elem_iff, instIsAlgebraicMvPolynomialOfNoZeroDivisors_1, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, Algebra.Generators.toExtension_algebraโ, KaehlerDifferential.mvPolynomialBasis_repr_D, HahnSeries.coeff_toMvPowerSeries, AddMonoidAlgebra.supportedEquivFinsupp_symm_apply_coe_apply, Representation.LinearizeMonoidal.ฮผ_toLinearMap, MvPolynomial.pderiv_eq_zero_of_notMem_vars, Representation.LinearizeMonoidal.ฮผ_leftUnitor, finsuppTensorFinsuppRid_apply_apply, Module.Basis.repr_sum_self, MvPolynomial.aeval_C_comp_left, RootPairing.Base.toWeightBasis_repr_root, linearCombination_option, Polynomial.derivativeFinsupp_one, Algebra.leftMulMatrix_mulVec_repr, Rep.standardComplex.d_apply, linearCombination_eq_fintype_linearCombination, KaehlerDifferential.ker_map_of_surjective, basisSingleOne_repr, supportedEquivFinsupp_symm_apply_coe, Module.Basis.smulTower_repr_mk, Module.Basis.repr_support_subset_of_mem_span, MvPolynomial.mapAlgHom_apply, Algebra.Generators.cotangentRestrict_mk, supportedEquivFinsupp_apply_support_val, finsuppLequivDFinsupp_symm_apply, AddMonoidAlgebra.ofCoeff_sum, lsum_comp_lsingle, Algebra.Generators.cotangentRestrict_bijective_of_basis_kaehlerDifferential, TensorProduct.finsuppRight_symm_apply_single, Representation.diagonalOneEquivLeftRegular_symm_apply_single, DegLex.instIsOrderedCancelAddMonoidDegLexNat, Algebra.SubmersivePresentation.ofSubsingleton_algebra_smul, Module.Basis.linearMap_repr_symm_apply, Representation.finsuppTensorLeft_apply_tmul_apply, KaehlerDifferential.mvPolynomialBasis_repr_comp_D, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, MvPolynomial.optionEquivLeft_symm_apply, finsuppTensorFinsuppLid_single_tmul_single, Representation.LinearizeMonoidal.ฮผ_rightUnitor, MvPolynomial.isLocalization_C_mk', groupHomology.isoCyclesโ_hom_comp_i_assoc, MvPolynomial.evalโHom_id_X_eq_joinโ, Algebra.Generators.Hom.comp_val, isArtinian_finsupp, span_range_eq_top_iff_surjective_finsuppLinearCombination, MvPolynomial.instIsPushout, prod_sum_index, Module.Relations.Solution.ofฯ_var, CommRingCat.HomTopology.mvPolynomialHomeomorph_apply_fst, Representation.LinearizeMonoidal.ฮด_ฮผ, MvPolynomial.esymm_eq_multiset_esymm, mapDomain_sum, AlgebraicGeometry.AffineSpace.over_over, Representation.leftRegular_norm_apply, IsTranscendenceBasis.mvPolynomial', supported_iUnion, Representation.coinvariantsToFinsupp_mk_single, Module.Relations.Solution.fromQuotient_comp_toQuotient, Module.Basis.SmithNormalForm.repr_comp_embedding_eq_smul, Representation.ind_mk, Module.Basis.toDual_linearCombination_right, AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp, MvPolynomial.support_esymm'', MvPolynomial.isLocalization, TensorProduct.finsuppLeft_apply_tmul, PiTensorProduct.ofFinsuppEquiv'_apply_apply, StandardEtalePresentation.toPresentation_val, AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly, LinearMap.toMatrix_toSpanSingleton, linearDepOn_iffโ, MvPolynomial.aeval_id_eq_joinโ, Representation.coinvariantsFinsuppLEquiv_symm_apply, Module.finrank_finsupp_self, Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero, Polynomial.support_derivativeFinsupp_subset_range, TensorProduct.equivFinsuppOfBasisRight_symm, exteriorPower.basis_repr, Algebra.mvPolynomial, groupHomology.ฯ_comp_H2Iso_hom_apply, MonomialOrder.leadingCoeff_prod_of_mem_nonZeroDivisors, indicator_eq_sum_single, Module.Relations.Solution.span_relation_le_ker_ฯ, MonomialOrder.degree_prod, IsBaseChange.basis_repr_comp, mapRange.linearEquiv_trans, ringKrullDim_add_enatCard_le_ringKrullDim_mvPolynomial, OrthonormalBasis.coe_toBasis_repr_apply, mapDomain.toLinearMap_linearEquiv, Rep.coinvariantsTensorIndHom_mk_tmul_indVMk, ZLattice.normBound_spec, QuadraticMap.apply_linearCombination, groupHomology.mapCyclesโ_hom, Rep.indToCoind_coindToInd, groupHomology.isoCyclesโ_inv_comp_iCycles, MvPolynomial.prod_X_pow, MvPolynomial.universalFactorizationMapPresentation_algebra_smul, 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, Module.Basis.traceDual_repr_apply, groupHomology.cyclesMap_comp_isoCyclesโ_hom_assoc, linearIndependent_single, MvPolynomial.iterToSum_C_C, groupHomology.single_mem_cyclesโ_of_mem_invariants, groupHomology.coe_mapCyclesโ, groupHomology.toCycles_comp_isoCyclesโ_hom, Module.Relations.toQuotient_relation, Module.Flat.exists_factorization_of_comp_eq_zero_of_free, MvPolynomial.evalโ_C_mk_eq_zero, moduleIsTorsionFree, Module.Basis.ofZLatticeComap_repr_apply, MvPolynomial.universalFactorizationMap_freeMonic, Algebra.Generators.Hom.toAlgHom_monomial, MvPolynomial.universalFactorizationMapPresentation_val, Module.projective_def, coe_univ_sum_single, HahnSeries.toMvPowerSeries_apply, MvPolynomial.coe_expand, Rep.indResHomEquiv_symm_apply, Module.End.ringEquivEndFinsupp_apply_apply_support, groupHomology.mapCyclesโ_comp_i_apply, MvPolynomial.aeval_sumElim, Module.annihilator_finsupp, MvPolynomial.universalFactorizationMapPresentation_ฯ', Representation.linearizeMap_toLinearMap, LinearMap.toMvPolynomial_eval_eq_apply, KaehlerDifferential.mvPolynomialBasis_repr_symm_single, groupHomology.boundariesToCyclesโ_apply, Module.Basis.toMatrix_transpose_apply, Module.finite_finsupp_self_iff, groupHomology.cyclesOfIsCycleโ_coe, rank_finsupp', groupHomology.isoCyclesโ_hom_comp_i, AddMonoidAlgebra.ofCoeff_finsuppSum, AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe, Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial, groupHomology.ฯ_comp_H1Iso_hom, MvPolynomial.monomial_sum_one, groupHomology.isoCyclesโ_inv_comp_iCycles, Module.Basis.ofZLatticeBasis_repr_apply, groupHomology.mkH1OfIsTrivial_apply, span_single_image, IsIsotypic.linearEquiv_finsupp, Algebra.Presentation.quotientEquiv_mk, lp.zeroBasis_repr_symm_apply_coe, LinearMap.toMatrixAlgEquiv_apply', MonomialOrder.div, AlgebraicGeometry.AffineSpace.SpecIso_inv_over, linearCombination_surjective, IntermediateField.LinearDisjoint.basisOfBasisLeft_repr_apply, MvPolynomial.scalarRTensor_symm_apply_single, lsingle_range_le_ker_lapply, TensorProduct.equivFinsuppOfBasisLeft_apply, Module.Basis.prod_repr_inr, range_lmapDomain, groupHomology.single_one_mem_boundariesโ, single_sum, linearCombination_comp_lmapDomain, mem_span_image_iff_linearCombination, MvPolynomial.IsHomogeneous.prod, MvPolynomial.irreducible_sumSMulXSMulY, sum_apply, BilinForm.apply_eq_dotProduct_toMatrix_mulVec, Module.Relations.toQuotient_map, Representation.leftRegularMapEquiv_symm_single, mapDomain.linearEquiv_symm, Module.Basis.constr_def, MvPolynomial.isJacobsonRing_MvPolynomial_fin, MvPolynomial.degreeOf_prod_le, comul_comp_lsingle, groupHomology.cyclesโIsoOfIsTrivial_inv_apply, coe_sum, Module.Basis.toDual_apply_left, MonomialOrder.sPolynomial_mem_sup_ideal, QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar, MvPolynomial.rTensor_apply, Module.DualBases.lc_def, MvPolynomial.joinโ_map, MvPolynomial.evalโHom_C_left, MvPolynomial.transcendental_supported_polynomial_aeval_X_iff, groupHomology.isoCyclesโ_hom_comp_i, AlgebraicGeometry.AffineSpace.isoOfIsAffine_inv_over, Module.Relations.Solution.IsPresentation.exact, StandardEtalePresentation.toPresentation_relation, NumberField.canonicalEmbedding_eq_basisMatrix_mulVec, Algebra.PreSubmersivePresentation.ofHasCoeffs_val, Module.Basis.reindexFinsetRange_repr, Module.Basis.continuous_coe_repr, TensorProduct.finsuppScalarLeft_apply, Algebra.Generators.self_algebra_algebraMap, MvPolynomial.esymm_eq_sum_subtype, Module.Basis.smulTower_repr, Module.Basis.toDual_apply_right, groupHomology.single_inv_ฯ_self_add_single_mem_boundariesโ, MonomialOrder.Monic.prod, MvPolynomial.ringKrullDim_of_isNoetherianRing, linearCombination_comapDomain, MvPolynomial.pderiv_X_self, MvPolynomial.quotientEquivQuotientMvPolynomial_rightInverse, MvPolynomial.pderiv_C, MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_smul, ZSpan.repr_floor_apply, MvRatFunc.rank_eq_max_lift, MvPolynomial.aeval_prod, Module.Basis.repr_symm_apply, apply_linearCombination_id, Polynomial.Bivariate.pderiv_one_equivMvPolynomial, Module.Basis.tensorProduct_repr_tmul_apply, Representation.freeLiftLEquiv_symm_apply, not_linearIndependent_iff_linearCombination, Representation.free_asModule_free, Basis.piTensorProduct_repr_tprod_apply, Module.Relations.Solution.ฯ_comp_map_apply, SymmetricAlgebra.IsSymmetricAlgebra.mvPolynomial, groupHomology.single_mem_cyclesโ_iff, TensorProduct.finsuppScalarLeft_symm_apply_single, Module.Basis.repr_smul', Representation.LinearizeMonoidal.ฮผ_apply_apply, lmap_finsuppLEquivDirectSum_eq, subtypeDomain_sum, ker_lsingle, Module.Projective.out, groupHomology.boundariesโ_le_cyclesโ, Module.Basis.repr_unitsSMul, Representation.ind_apply, equivFunOnFinite_symm_eq_sum, MvPolynomial.sumToIter_C, RingHom.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial, MonoidAlgebra.coeff_sum, Module.Basis.constr_apply, Module.Finite.finsupp, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, MvPolynomial.derivation_eqOn_supported, linearCombination_eq_fintype_linearCombination_apply, Representation.leftRegularMapEquiv_apply, MvPolynomial.IsHomogeneous.evalโ, Subalgebra.LinearDisjoint.basisOfBasisLeft_repr_apply, disjoint_supported_supported_iff, MonomialOrder.degree_prod_of_regular, mem_finsuppAffineCoords_iff_linearCombination, LinearMap.splittingOfFinsuppSurjective_splits, MvPolynomial.trdeg_of_isDomain, Submodule.LinearDisjoint.linearIndependent_left_of_flat, Module.Basis.repr_eq_iff', linearDepOn_iff', prod_finset_sum_index, Module.End.ringEquivEndFinsupp_symm_apply_apply, sum_single, supportedEquivFinsupp_symm_apply_coe_apply, MvPolynomial.support_esymm, iSupIndep_range_lsingle, Rep.coinvariantsTensorIndInv_mk_tmul_indMk, sum_finset_sum_index, MvPolynomial.transcendental_supported_X, mapRange_finset_sum, Module.Basis.norm_repr_le_norm, Representation.freeLiftLEquiv_apply, MvPolynomial.scalarRTensor_apply_tmul_apply, Module.Basis.mem_span_repr_support, Pi.basisFun_repr, Algebra.leftMulMatrix_eq_repr_mul, Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op, finsuppProdLEquiv_symm_apply_apply, Module.Basis.sum_repr, lmapDomain_disjoint_ker, instFreeCarrierXโModuleCatProjectiveShortComplex, supportedEquivFinsupp_apply_apply, ZSpan.mem_fundamentalDomain, Rep.standardComplex.d_single, Submodule.image_smul_top_eq_range_lsum, groupHomology.H1AddEquivOfIsTrivial_symm_tmul, Module.Basis.toMatrix_mulVec_repr, groupHomology.single_mem_cyclesโ_iff, single_mem_supported, TensorProduct.sum_tmul_basis_left_injective, finsetBasisOfLinearIndependentOfCardEqFinrank_repr_apply, Module.End.ringHomEndFinsupp_surjective, Algebra.Presentation.instFinitePresentationQuotientOfFinite, TensorProduct.equivFinsuppOfBasisRight_symm_apply, MvPolynomial.evalโ_assoc, Module.Basis.algebraMapCoeffs_repr, toMultiset_sum_single, Bundle.Trivialization.localFrame_coeff_apply_of_mem_baseSet, Nat.factorization_prod, Module.Basis.coord_apply, support_sum_eq_biUnion, DividedPowerAlgebra.prod_dp, exists_integral_inj_algHom_of_fg, Module.Basis.mem_span_iff_repr_mem, Module.Basis.SmithNormalForm.repr_eq_zero_of_notMem_range, Module.Relations.Solution.IsPresentation.ker_ฯ, KaehlerDifferential.quotKerTotalEquiv_apply, KaehlerDifferential.kerTotal_map', Rep.barComplex.d_single, domLCongr_refl, MvPolynomial.eval_assoc, LinearMap.toMatrixAlgEquiv_transpose_apply, mapRange_multiset_sum, Module.Basis.repr_self, TensorProduct.finsuppRight_apply_tmul_apply, Algebra.Generators.ker_naive, linearCombination_zero, MvPolynomial.vanishingIdeal_zeroLocus_eq_radical, instFreeMvPolynomialKaehlerDifferential, TensorProduct.finsuppRight_apply_tmul, Module.subsingletonEquiv_apply, groupHomology.isBoundaryโ_iff, rank_mvPolynomial_mvPolynomial, Polynomial.degreeLT.basis_repr, Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial, Module.Basis.repr_reindex_apply, MvPolynomial.algebraMap_def, groupHomology.mapCyclesโ_quotientGroupMk'_epi, groupHomology.mapCyclesโ_comp_i_assoc, LinearMap.toMatrix_apply, linearDepOn_iff'โ, Representation.linearize_apply, NumberField.house.basis_repr_norm_le_const_mul_house, Rep.coinvariantsTensorFreeToFinsupp_mk_tmul_single, Representation.diagonalOneEquivLeftRegular_apply_single, linearIndependent_single_one, LinearMap.map_finsupp_linearCombination, Algebra.PreSubmersivePresentation.jacobian_eq_jacobiMatrix_det, MvPolynomial.derivation_ext_iff, Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination, range_restrictDom, LinearMap.toMatrixAlgEquiv_transpose_apply', Module.Relations.Solution.ฯ_single, lmapDomain_apply, linearIndepOn_iff_linearCombinationOnโ, ringKrullDim_mvPolynomial_of_isEmpty, MvPolynomial.IsHomogeneous.pderiv, SkewMonoidAlgebra.toFinsupp_sum', domLCongr_single, groupHomology.mem_cyclesโ_iff, sum_sum_index, Algebra.SubmersivePresentation.basisDeriv_apply, MvPolynomial.bindโ_monomial, TensorProduct.coe_finsuppScalarRight', LinearMap.polyCharpoly_coeff_eval, lsum_comp_mapRange_toSpanSingleton, Representation.finsuppTensorRight_apply_tmul_apply, Module.Basis.repr_unop_eq_mulOpposite_repr, groupHomology.boundariesToCyclesโ_apply, groupHomology.single_mem_cyclesโ_iff_inv, MvPolynomial.mem_image_comap_C_basicOpen, Algebra.Presentation.mem_ker_naive, linearIndepOn_iff_linearCombinationOn, Representation.linearizeTrivial_def, lsingle_apply, Representation.IndV.hom_ext_iff, Module.Relations.Solution.IsPresentation.ฯ_desc_apply, Pi.comul_comp_finsuppLcoeFun, exteriorPower.basis_repr_self, TensorProduct.finsuppLeft'_apply, Polynomial.derivativeFinsupp_C, TensorProduct.finsuppRight_tmul_single, Submodule.mulRightMap_apply_single, Module.finrank_finsupp, groupHomology.isoCyclesโ_hom_comp_i_assoc, Polynomial.derivativeFinsupp_X, finsuppLEquivDirectSum_symm_lof, Module.Flat.exists_factorization_of_isFinitelyPresented, instIsPushoutFractionRingMvPolynomial_1, groupHomology.H2ฯ_eq_zero_iff, curryLinearEquiv_symm_apply, KaehlerDifferential.linearCombination_surjective, lsubtypeDomain_apply, HahnSeries.coeff_ofFinsuppLinearMap, Module.Basis.sumQuot_repr_inr, linearCombination_onFinset, lsum_symm_apply, Module.Basis.coord_repr_symm, Module.Relations.Solution.linearCombination_var_relation, lcongr_apply_apply, MonomialOrder.degree_prod_of_mem_nonZeroDivisors, Algebra.Generators.toExtension_commRing, MvPowerSeries.prod_monomial, ZLattice.abs_repr_le, DirectSum.IsInternal.collectedBasis_repr_of_mem, Module.Basis.coe_sumCoords, iSup_lsingle_range, MvPolynomial.universalFactorizationMapPresentation_jacobian, Representation.LinearizeMonoidal.ฮต_toLinearMap, LinearMap.sum_repr_mul_repr_mul, mem_supported', lmapDomain_supported, Representation.linearizeTrivialIso_symm_apply, MvPolynomial.commAlgEquiv_C_X, groupHomology.ฮดโ_apply, Module.Basis.ofIsLocalizedModule_repr_apply, Representation.leftRegularMapEquiv_symm_apply_toFun, Module.Relations.Solution.ofQuotient_ฯ, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, groupHomology.H1ฯ_eq_iff, LinearMap.fst_prodOfFinsuppNat, TensorProduct.finsuppLeft_apply_tmul_apply, MvPolynomial.transcendental_supported_polynomial_aeval_X, instIsPushoutFractionRingMvPolynomial, MvPolynomial.sumToIter_Xl, LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly, Representation.ofMulAction_def, groupHomology.cyclesMap_comp_isoCyclesโ_hom, MvPolynomial.pderiv_inl_universalFactorizationMap_X, MvPolynomial.instFaithfulSMul, sigmaFinsuppLequivDFinsupp_apply, Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val, MvPolynomial.rTensorAlgHom_apply_eq
|
instAddGroup ๐ | CompOp | 1 mathmath: mem_finsuppAffineCoords_iff_linearCombination
|
instAddMonoid ๐ | CompOp | 866 mathmath: image_prodMap_embDomain_antidiagonal, MvPolynomial.pUnitAlgEquiv_symm_monomial, MvPolynomial.joinโ_rename, MvPolynomial.vanishingIdeal_anti_mono, MvPolynomial.aeval_sum, MvPolynomial.dvd_monomial_one_iff_exists, WittVector.bindโ_frobeniusPoly_wittPolynomial, KaehlerDifferential.mvPolynomialBasis_apply, Algebra.PreSubmersivePresentation.jacobiMatrix_naive, MvPolynomial.algHom_ext_iff, MonomialOrder.span_leadingTerm_sdiff_singleton_zero, MvPolynomial.map_bindโ, Algebra.Generators.aeval_val_surjective, wittPolynomial_zmod_self, MvPolynomial.aeval_X_left, MvPolynomial.pUnitAlgEquiv_apply, MvPolynomial.exists_finset_rename, MonomialOrder.monic_X_sub_C, MvPolynomial.support_finSuccEquiv, Algebra.PreSubmersivePresentation.cotangentComplexAux_apply, WittVector.aeval_verschiebung_poly', MvPolynomial.rTensorAlgEquiv_apply, Algebra.Generators.H1Cotangent.ฮดAux_mul, Algebra.Presentation.naive_toGenerators, MvPolynomial.mem_image_support_coeff_finSuccEquiv, MvPolynomial.comapEquiv_symm_coe, Matrix.charpoly.univ_map_map, MvPolynomial.evalโ_expand, MvPolynomial.universalFactorizationMap_comp_map, MvPolynomial.aeval_algebraMap_eq_zero_iff, Algebra.PreSubmersivePresentation.ofHasCoeffs_map, MvPolynomial.expand_X, algebraicIndependent_iff_ker_eq_bot, Algebra.Generators.cotangentSpaceBasis_apply, MvPolynomial.instIsReduced, MvPolynomial.X_pow_eq_monomial, WittVector.ghostComponent_apply, MvPolynomial.ker_map, aeval_wittPolynomial, MvPolynomial.aeval_range, KaehlerDifferential.mvPolynomialBasis_repr_D_X, MvPolynomial.optionEquivLeft_C, MvPolynomial.rename_rename, Algebra.Generators.toAlgHom_ofComp_localizationAway, MvPolynomial.leibniz_iff_X, MvPowerSeries.trunc'_expand_trunc', MvPolynomial.optionEquivLeft_X_some, MvPolynomial.aeval_X_left_apply, Polynomial.toPowerSeries_toMvPowerSeries, MvPolynomial.le_vanishingIdeal_zeroLocus, MvPolynomial.pUnitAlgEquiv_symm_apply, MvPolynomial.expand_eq_zero, Algebra.Presentation.localizationAway_relation, MvPolynomial.weightedHomogeneousSubmodule_mul, Ideal.span_pow_eq_map_homogeneousSubmodule, MvPolynomial.natDegree_finSuccEquiv, StandardEtalePresentation.toPresentation_algebra_smul, MvPolynomial.totalDegree_X_pow, Ideal.span_eq_map_homogeneousSubmodule, MvPolynomial.algHom_ext'_iff, IntermediateField.mem_adjoin_iff, AlgebraicIndependent.repr_ker, chevalley_mvPolynomial_mvPolynomial, MvPolynomial.aeval_X, MvPolynomial.comapEquiv_coe, MvPolynomial.vars_sub_of_disjoint, MvPolynomial.exists_dvd_map_of_isAlgebraic, Polynomial.pUnitAlgEquiv_symm_toPowerSeries, MvPolynomial.evalโ_pow, MvPolynomial.irreducible_mul_X_add, AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin, MonomialOrder.degree_sub_le, Algebra.PreSubmersivePresentation.cotangentComplexAux_zero_iff, MvPolynomial.optionEquivLeft_apply, MvPolynomial.instIsScalarTower, MvPolynomial.totalDegree_coeff_finSuccEquiv_add_le, MvPolynomial.map_comp_rename, MvPolynomial.ACounit_X, WittVector.mul_polyOfInterest_aux2, MvPolynomial.prime_rename_iff, bindโ_xInTermsOfW_wittPolynomial, MvPolynomial.constantCoeff_rename, Algebra.PreSubmersivePresentation.jacobiMatrix_reindex, AlgebraicClosure.maxIdeal.isMaximal, CommRingCat.free_map_coe, Algebra.FinitePresentation.mvPolynomial_of_finitePresentation, Algebra.SubmersivePresentation.ofSubsingleton_algebra_algebraMap, MvPolynomial.killCompl_comp_rename, MvPolynomial.supportedEquivMvPolynomial_symm_X, Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp, MvPolynomial.ACounit_surjective, MvPolynomial.supported_eq_adjoin_X, MvPolynomial.aeval_eq_eval, MvPolynomial.aeval_ite_mem_eq_self, MvPolynomial.evalโHom_C_id_eq_joinโ, PolynomialLaw.exists_lift', MvPolynomial.pow_idealOfVars, PolynomialLaw.toFun_eq_rTensor_ฯ_toFun', MvPolynomial.comap_id, MvPolynomial.eval_rename_prod_mk, MvPolynomial.optionEquivRight_C, Polynomial.Bivariate.Polynomial.Bivariate.pderiv_one_equivMvPolynomial, MvPolynomial.aevalTower_comp_C, MvPolynomial.rename_msymm, MvPolynomial.comap_comp_apply, MvPolynomial.evalโHom_C_eq_bindโ, MvPolynomial.sum_antidiagonal_card_esymm_psum_eq_zero, Algebra.PreSubmersivePresentation.ofHasCoeffs_relation, MvPolynomial.degreeOf_coeff_finSuccEquiv, MvPolynomial.mem_pow_idealOfVars_iff, MvPolynomial.rename_id_apply, MvPolynomial.nonempty_support_finSuccEquiv, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, MvPolynomial.pderiv_rename, Algebra.Presentation.comp_relation_inr, LinearMap.nilRankAux_basis_indep, MvPolynomial.support_killCompl, AlgebraicIndependent.aeval_comp_repr, MvPolynomial.esymmAlgHomMonomial_single, MvPolynomial.map_expand, MvPolynomial.map_aeval, MvPolynomial.map_frobenius_expand, MvPolynomial.renameEquiv_trans, MvPolynomial.expand_monomial, MvPolynomial.expand_char, MvPolynomial.map_rename, Algebra.PreSubmersivePresentation.ofHasCoeffs_ฯ', MvPolynomial.killCompl_C, Algebra.Presentation.quotientEquiv_symm, MvPolynomial.evalโ_const_pUnitAlgEquiv_symm, MvPolynomial.eval_comp_toMvPolynomial, Algebra.Generators.map_toComp_ker, MvPolynomial.support_finSuccEquiv_nonempty, Algebra.Generators.Hom.toExtensionHom_toAlgHom_apply, MvPolynomial.bindโ_X_left, MvPolynomial.monomial_one_dvd_iff_modMonomial_eq_zero, MvPolynomial.sumAlgEquiv_comp_rename_inr, MvPolynomial.aevalTower_toAlgHom, LinearMap.polyCharpoly_coeff_isHomogeneous, MvPolynomial.degree_optionEquivLeft, MvPolynomial.mapAlgHom_id, Algebra.Generators.naive_val, MvPolynomial.coeff_expand_smul, Algebra.Generators.algebraMap_apply, MvPolynomial.expand_C, instIsIntegralMvPolynomial, Algebra.Generators.compLocalizationAwayAlgHom_X_inl, MvPolynomial.optionEquivRight_X_none, MvPolynomial.rename_psum, Algebra.Generators.map_ofComp_ker, WeierstrassCurve.Jacobian.polynomialY_eq, MvPolynomial.expand_zero, MvPolynomial.degreesLE_nsmul, MvPolynomial.totalDegree_rename_le, MvPolynomial.coe_mapEquivMonic_comp', Algebra.Presentation.naive_relation, Polynomial.toMvPolynomial_eq_rename_comp, DividedPowerAlgebra.dp_mul, Polynomial.aeval_homogenize_X_one, MvPolynomial.adjoin_range_X, MonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure, AddMonoidAlgebra.mvPolynomial_aeval_of_surjective_of_closure, antidiagonal_single, MvPolynomial.X_dvd_X, MvPolynomial.transcendental_polynomial_aeval_X_iff, MvPolynomial.aeval_algebraMap_eq_zero_iff_of_injective, Algebra.Generators.algebraMap_eq, Algebra.SubmersivePresentation.ofSubsingleton_relation, StandardEtalePair.equivMvPolynomialQuotient_symm_apply, MvPolynomial.support_rename_of_injective, Algebra.IsSmoothAt.exists_isStandardEtale_mvPolynomial, MvPolynomial.comap_comp, xInTermsOfW_eq, LinearMap.nilRank_eq_polyCharpoly_natTrailingDegree, MvPolynomial.eval_eq_eval_mv_eval', MvPolynomial.ACounit_C, LinearMap.polyCharpoly_baseChange, MvPolynomial.transcendental_supported_X_iff, MvPolynomial.optionEquivLeft_X_none, MvPolynomial.algebraicIndependent_polynomial_aeval_X, MvPolynomial.IsHomogeneous.HomogeneousSubmodule.gcommSemiring, MvPolynomial.degreeOf_rename_of_injective, MvPolynomial.degreesLE_add, MvPolynomial.exists_rename_eq_of_vars_subset_range, MonomialOrder.span_leadingTerm_eq_span_monomial, MvPolynomial.optionEquivRight_symm_apply, MvPolynomial.instIsPrimeVanishingIdealSingletonForallSet, MonomialOrder.span_leadingTerm_eq_span_monomialโ, LinearMap.polyCharpolyAux_map_eval, LinearMap.polyCharpoly_coeff_eq_zero_of_basis, Algebra.Generators.Hom.aeval_val, Polynomial.MonicDegreeEq.freeMonic_coe, DividedPowerAlgebra.natFactorial_mul_dp_eq, Algebra.Presentation.comp_aeval_relation_inl, WittVector.mulN_coeff, MvPolynomial.isUnit_iff_totalDegree_of_isReduced, Algebra.SubmersivePresentation.jacobianRelations_spec, MvPolynomial.support_expand_subset, WeierstrassCurve.Projective.polynomialZ_eq, Matrix.charpoly.univ_monic, MvPolynomial.totalDegree_pow, MvPolynomial.coeff_rename_embDomain, MvPolynomial.isUnit_iff, MvPolynomial.X_dvd_monomial, MvPolynomial.finSuccEquiv_coeff_coeff, MvPolynomial.rename_comp_expand, Algebra.PreSubmersivePresentation.aevalDifferential_toMatrix'_eq_mapMatrix_jacobiMatrix, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C', MvPowerSeries.coeff_inv, MvPolynomial.rename_esymm, MvPolynomial.IsHomogeneous.sub, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_algebraMap_apply, MvPolynomial.quotient_map_C_eq_zero, MvPolynomial.coeff_X_pow, MvPolynomial.pow_idealOfVars_eq_span, MvPolynomial.IsHomogeneous.pow, Algebra.Generators.toAlgHom_ofComp_surjective, MvPolynomial.bindโ_comp_bindโ, MvPolynomial.commAlgEquiv_C, Algebra.Generators.Hom.algebraMap_toAlgHom', Algebra.FinitePresentation.ker_fg_of_mvPolynomial, Algebra.Generators.cotangentSpaceBasis_repr_tmul, MvPolynomial.aevalTower_X, MvPolynomial.vars_sub_subset, MvPolynomial.irreducible_of_forall_totalDegree_le, MvPolynomial.commAlgEquiv_X, Matrix.charpoly.univ_coeff_evalโHom, MvPolynomial.optionEquivRight_X_some, MvPolynomial.aeval_expand, AlgebraicIndependent.lift_reprField, MvPolynomial.aeval_algebraMap_apply, Algebra.SubmersivePresentation.linearIndependent_aeval_val_pderiv_relation, wittPolynomial_one, Algebra.FiniteType.baseChangeAux_surj, Algebra.Generators.H1Cotangent.ฮดAux_toAlgHom, Subalgebra.mvPolynomial_aeval_coe, IsLocalization.Away.mvPolynomialQuotientEquiv_apply, Algebra.Presentation.naive_relation_apply, PolynomialLaw.exists_lift, WittVector.mul_polyOfInterest_aux4, MvPolynomial.rename_evalโ, MvPolynomial.coeff_sum_X_pow_of_fintype, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_X_some, MvPowerSeries.expand_eq_expand, MvPolynomial.irreducible_of_disjoint_support, Algebra.Generators.localizationAway_ฯ, MvPolynomial.mapAlgEquiv_apply, Polynomial.Bivariate.equivMvPolynomial_symm_X_0, MvPolynomial.algebraTensorAlgEquiv_symm_comp_aeval, MvPolynomial.finitePresentation_universalFactorizationMap, MvPolynomial.mapAlgEquiv_refl, WittVector.frobeniusPoly_zmod, Algebra.FiniteType.iff_quotient_mvPolynomial', MvPolynomial.tensorEquivSum_one_tmul_C, MonomialOrder.Monic.pow, Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom, Polynomial.degree_freeMonic, MvPolynomial.evalโHom_rename, MvPolynomial.degreeOf_pow_eq, LieModule.rank_eq_natTrailingDegree, MvPolynomial.sumAlgEquiv_comp_rename_inl, MvPolynomial.dvd_monomial_iff_exists, AlgebraicIndependent.aeval_of_algebraicIndependent, MvPolynomial.aeval_bindโ, MvPolynomial.X_dvd_mul_iff, MonomialOrder.leadingCoeff_pow_of_pow_leadingCoeff_ne_zero, MvPolynomial.algebraMap_apply, MvPolynomial.mkDerivationโ_monomial, MvPolynomial.killCompl_monomial_eq_zero_of_not_subset, MvPolynomial.exists_fin_rename, MvPolynomial.optionEquivLeft_coeff_coeff, Matrix.charpoly.optionEquivLeft_symm_univ_isHomogeneous, MvPolynomial.pderiv_def, MvPolynomial.mem_pow_idealOfVars_iff', MvPolynomial.mem_supported, MvPolynomial.renameEquiv_apply, MvPolynomial.degrees_pow_le, MvPolynomial.rename_esymmAlgHom, MvPolynomial.aeval_eq_zero, MvPolynomial.evalโ_cast_comp, Algebra.PreSubmersivePresentation.naive_toPresentation, MonomialOrder.span_leadingTerm_eq_span_monomial', MvPolynomial.bindโ_C_right, Polynomial.toTupleMvPolynomial_one_eq, MvPolynomial.rename_zero, MvPolynomial.instIsLocalHomRingHomAlgebraMap, WittVector.bindโ_wittMulN_wittPolynomial, PolynomialLaw.exists_range_ฯ_eq_of_fg, Algebra.FinitePresentation.mvPolynomial, MvPolynomial.coeff_single_X_pow, MvPolynomial.dvd_X_mul_iff, MonomialOrder.degree_X_sub_C, MvPolynomial.aevalTower_C, MvPolynomial.expand_one_apply, MvPolynomial.map_expand_pow_char, xInTermsOfW_aux, Algebra.Presentation.span_range_relation_eq_ker, MvPolynomial.monomial_mem_pow_idealOfVars_iff, MonomialOrder.degree_smul_le, MvPolynomial.irreducible_sumSMulX, AnalyticOnNhd.aeval_mvPolynomial, Algebra.Generators.Hom.toAlgHom_X, MvPolynomial.bindโ_rename, MvPolynomial.degreeOf_sub_le, wittStructureRat_prop, MvPolynomial.degrees_rename, Algebra.Presentation.comp_relation, Polynomial.Bivariate.equivMvPolynomial_symm_C, Algebra.Generators.instIsScalarTowerRing, MvPowerSeries.aeval_coe, Polynomial.homogenize_X_pow, WittVector.IsPoly.poly, MvPolynomial.combinatorial_nullstellensatz_exists_linearCombination, MvPolynomial.finite_universalFactorizationMap, MvPolynomial.rTensorAlgHom_toLinearMap, wittStructureRat_rec, WittVector.mul_polyOfInterest_vars, MvPolynomial.homogeneousSubmodule_zero, MvPolynomial.expand_eq_C, MvPowerSeries.trunc'_expand, MvPolynomial.universalFactorizationMapPresentation_map, MvPolynomial.coeff_rename_mapDomain, MvPolynomial.algebraTensorAlgEquiv_symm_X, MvPolynomial.expand_injective, MvPolynomial.support_coeff_finSuccEquiv, Algebra.Presentation.aeval_val_relation, LinearMap.polyCharpolyAux_map_eq_charpoly, MvPolynomial.expand_one, MvPolynomial.esymmAlgHom_fin_surjective, MvPolynomial.expand_inj, LinearMap.polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff, MvPolynomial.coeff_prod_X_pow, MvPolynomial.coeffsIn_mul, MvPowerSeries.rename_coe, MonomialOrder.sPolynomial_def, MvPolynomial.mk_eq_evalโ, Algebra.Generators.H1Cotangent.ฮดAux_ofComp, MvPolynomial.restrictSupport_zero, MvPolynomial.killCompl_monomial_mapDomain, MonomialOrder.mem_nonZeroDivisors_of_leadingCoeff_mem_nonZeroDivisors, MvPolynomial.isUnit_iff_eq_C_of_isReduced, MvPolynomial.monomial_add_single, MvPolynomial.le_coeffsIn_pow, MvPolynomial.supported_strictMono, MvPolynomial.IsWeightedHomogeneous.pow, MonomialOrder.degree_pow_le, MvPolynomial.pointToPoint_zeroLocus_le, exists_integral_inj_algHom_of_quotient, MvPolynomial.isNilpotent_iff, exists_finite_inj_algHom_of_fg, MvPolynomial.zeroLocus_bot, MvPolynomial.aeval_def, MvPolynomial.degrees_sub_le, Algebra.Generators.toAlgHom_ofComp_rename, Algebra.FinitePresentation.iff, DividedPowerAlgebra.dp_zero, wittStructureRat_rec_aux, Polynomial.Bivariate.equivMvPolynomial_symm_X_1, MvPowerSeries.coeff_inv_aux, MvPolynomial.supported_mono, Algebra.Generators.ker_localizationAway, MonomialOrder.sPolynomial_decomposition, MvPolynomial.totalDegree_expand, MvPolynomial.algHom_C, wittStructureInt_prop, MvPolynomial.eval_pow, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, MvPolynomial.le_zeroLocus_iff_le_vanishingIdeal, MvPolynomial.mkโ_eq_aeval, MvPolynomial.mem_support_coeff_optionEquivLeft, Algebra.Presentation.fg_ker, instIsAlgebraicMvPolynomialOfNoZeroDivisors, Polynomial.eval_X_toTupleMvPolynomial_zero_eq, MvPolynomial.dvd_smul_X_iff_exists, MvPolynomial.mem_supported_vars, MvPolynomial.mkDerivation_monomial, Algebra.Presentation.relation_mem_ker, Algebra.Generators.Hom.toExtensionHom_toRingHom, Algebra.Generators.comp_localizationAway_ker, MvPolynomial.mem_map_C_iff, MvPolynomial.rename_monomial, MvPolynomial.aeval_toMvPolynomial, MvPolynomial.mul_esymm_eq_sum, MvPolynomial.restrictScalars_restrictSupportIdeal, MvPolynomial.degreesLE_zero, MvPolynomial.universalFactorizationMapPresentation_relation, MvPolynomial.aevalTower_comp_algebraMap, Algebra.PreSubmersivePresentation.aevalDifferential_single, AlgebraicIndependent.algebraMap_aevalEquiv, MvPolynomial.aeval_id_rename, WeierstrassCurve.Projective.polynomialX_eq, Algebra.adjoin_range_eq_range_aeval, MvPolynomial.evalโ_sub, Algebra.Generators.aeval_val_ฯ, MvPolynomial.mem_zeroLocus_iff, MvPolynomial.totalDegree_coeff_optionEquivLeft_add_le, WeierstrassCurve.Projective.polynomialY_eq, MvPolynomial.aeval_eq_constantCoeff_of_vars, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul, SymmetricAlgebra.equivMvPolynomial_symm_X, MvPolynomial.coeff_linearCombination_X_pow, MvPolynomial.expand_bindโ, MvPolynomial.prod_X_pow_eq_monomial, MvPolynomial.smul_eval, MvPowerSeries.substAlgHom_coe, MvPolynomial.universalFactorizationMapPresentation_algebra_algebraMap, MvPolynomial.coeff_rTensorAlgHom_tmul, MvPolynomial.aeval_zero, MvPolynomial.killCompl_rename_app, MvPolynomial.comp_aeval, MvPolynomial.frobenius_zmod, KaehlerDifferential.mvPolynomialBasis_repr_apply, WittVector.frobeniusPolyAux_eq, MvPolynomial.optionEquivLeft_coeff_some_coeff_none, IntermediateField.mem_adjoin_range_iff, DividedPowerAlgebra.mkAlgHom_surjective, WittVector.coeff_frobeniusFun, MvPolynomial.renameEquiv_refl, MvPolynomial.totalDegree_renameEquiv, MvPolynomial.expand_mul, Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul, MvPolynomial.isLocalHom_expand, Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, MvPolynomial.C_mul', AlgebraicClosure.le_maxIdeal, MvPolynomial.isEmptyAlgEquiv_apply, MvPolynomial.of_irreducible_expand, Algebra.Generators.cMulXSubOneCotangent_eq, DividedPowerAlgebra.submodule_span_prod_dp_eq_top, LinearMap.polyCharpolyAux_baseChange, Polynomial.Bivariate.equivMvPolynomial_X, sum_antidiagonal_swap, MvPolynomial.C_dvd_iff_dvd_coeff, Module.Basis.symmetricAlgebra_repr_apply, MonomialOrder.degree_smul_of_isRegular, AlgebraicClosure.toSplittingField_coeff, MvPolynomial.coe_pow, MvPolynomial.natDegree_optionEquivLeft, Matrix.charpoly.univ_coeff_isHomogeneous, Algebra.Generators.self_algebra_smul, MvPolynomial.restrictSupport_nsmul, MvPolynomial.mem_support_finSuccEquiv, MvPolynomial.isNoetherianRing_fin, MvPolynomial.X_dvd_iff_modMonomial_eq_zero, MvPolynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing, algebraicIndependent_iff_injective_aeval, MvPolynomial.aeval_map_algebraMap, Algebra.Generators.Hom.toAlgHom_C, MvPolynomial.rename_comp_toMvPolynomial, MvPolynomial.finSuccEquiv_comp_C_eq_C, MvPolynomial.coeToMvPowerSeries.algHom_apply, AlgebraicIndependent.liftAlgHom_comp_reprField, DividedPowerAlgebra.algHom_ext_iff, MvPolynomial.rename_rightInverse, Algebra.SubmersivePresentation.sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs, WeierstrassCurve.Jacobian.polynomialZ_eq, MvPolynomial.finSuccEquiv_eq, SymmetricAlgebra.equivMvPolynomial_ฮน_apply, LinearMap.polyCharpoly_eq_of_basis, MvPolynomial.ker_evalโHom_universalFactorizationMap, MvPolynomial.bindโ_comp_rename, LinearMap.polyCharpolyAux_map_aeval, MvPolynomial.monic_monomial_eq, MvPolynomial.image_support_finSuccEquiv, MvPolynomial.evalโ_rename, AlgebraicIndependent.aeval_repr, MvPolynomial.support_expand, Polynomial.Bivariate.equivMvPolynomial_C_X, MvPolynomial.IsSymmetric.rename, MvPolynomial.IsHomogeneous.aeval, antidiagonal_zero, WittVector.mul_polyOfInterest_aux1, MvPolynomial.quotientEquivQuotientMvPolynomial_leftInverse, MvPolynomial.aeval_bindโ, MvPolynomial.rename_bindโ, MvPolynomial.support_X_pow, MvPolynomial.prod_X_add_C_coeff, MvPolynomial.renameSymmetricSubalgebra_symm_apply_coe, Algebra.Generators.Hom.toAlgHom_comp_apply, MvPolynomial.degree_finSuccEquiv, Polynomial.Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, MvPolynomial.isNoetherianRing_fin_0, MvPolynomial.nonempty_support_optionEquivLeft, MvPolynomial.isRegular_X_pow, bindโ_rename_expand_wittPolynomial, Algebra.adjoin_eq_range, MvPolynomial.mapAlgEquiv_symm, Algebra.Generators.toComp_toAlgHom_monomial, MvPolynomial.rename_injective, MvPolynomial.quotient_mk_comp_C_injective, MvPolynomial.monomial_mem_homogeneousSubmodule_pow_degree, Algebra.SubmersivePresentation.aeval_jacobianOfHasCoeffs, LinearMap.polyCharpolyAux_coeff_eval, MvPolynomial.esymmAlgHomMonomial_single_one, AlgebraicClosure.Monics.map_eq_prod, MvPolynomial.coe_smul, MvPolynomial.dvd_monomial_mul_iff_exists, MvPolynomial.killCompl_map, MonomialOrder.span_leadingTerm_insert_zero, Algebra.FiniteType.iff_quotient_mvPolynomial, MonomialOrder.div_set, MvPolynomial.aeval_eq_bindโ, MvPolynomial.support_optionEquivLeft, MvPolynomial.degreeOf_pow_le, MvPolynomial.dvd_X_iff_exists, MvPolynomial.finSuccEquiv_X_succ, MvPolynomial.aeval_ofNat, Algebra.Presentation.aeval_val_relationOfHasCoeffs, MvPolynomial.expand_comp_bindโ, MvPolynomial.mapAlgEquiv_trans, Algebra.SubmersivePresentation.aeval_invJacobianOfHasCoeffs, MvPolynomial.ker_mapAlgHom, MvPolynomial.aeval_injective_iff_of_isEmpty, Algebra.Generators.ofComp_kerCompPreimage, MvPolynomial.X_mem_supported, MvPolynomial.eval_sub, MvPolynomial.esymmAlgHom_fin_injective, MvPolynomial.aeval_comp_bindโ, MvPolynomial.totalDegree_sub, Polynomial.monic_freeMonic, MvPolynomial.evalโ_const_pUnitAlgEquiv, Algebra.Generators.repr_CotangentSpaceMap, DividedPowerAlgebra.dp_sum_smul, MvPolynomial.pderiv_pow, MvPolynomial.aeval_esymm_eq_multiset_esymm, MvPolynomial.supported_le_supported_iff, MonomialOrder.coeff_pow_nsmul_degree, MvPolynomial.eval_rename, StandardEtalePresentation.toPresentation_ฯ', MvPolynomial.isIntegral_iff_isIntegral_coeff, witt_structure_prop, MvPolynomial.coe_evalโAlgHom, LinearMap.toMvPolynomial_comp, MvPolynomial.IsHomogeneous.rename_isHomogeneous_iff, MvPolynomial.vars_bindโ, MonomialOrder.leadingCoeff_pow, WittVector.bindโ_verschiebungPoly_wittPolynomial, MvPolynomial.prod_C_add_X_eq_sum_esymm, Algebra.Presentation.instFinitePresentationModelOfHasCoeffsOfFinite, MonomialOrder.degree_pow, MvPolynomial.optionEquivRight_apply, MvPolynomial.finSuccEquiv_apply, MvPolynomial.vanishingIdeal_empty, MvPolynomial.tensorEquivSum_X_tmul_X, MvPolynomial.comp_aeval_apply, Algebra.Presentation.relation_comp_localizationAway_inl, WittVector.coeff_select, MvPolynomial.aeval_unique, DividedPowerAlgebra.dp_def, MvPolynomial.coeff_rTensorAlgHom_monomial_tmul, MvPolynomial.bindโ_bindโ, MvPolynomial.algebraTensorAlgEquiv_symm_map, MvPolynomial.coeff_sub, MvPolynomial.rename_polynomial_aeval_X, MvPolynomial.coeff_expand_of_not_dvd, DividedPowerAlgebra.dp_sum, Algebra.Generators.Hom.equivAlgHom_symm_apply_val, MvPolynomial.isHomogeneous_C_mul_X_pow, MvPolynomial.tensorEquivSum_C_tmul_one, MvPolynomial.map_iterateFrobenius_expand, MvPolynomial.vars_pow, Polynomial.toMvPolynomial_X, MvPolynomial.sumAlgEquiv_apply, Algebra.SubmersivePresentation.exists_sum_eq_ฯ_jacobian_mul_ฯ_jacobian_inv_sub_one, Algebra.Generators.ker_comp_eq_sup, instIsAddTorsionFree, LinearMap.polyCharpoly_map_eq_charpoly, LinearMap.polyCharpoly_monic, Polynomial.natDegree_freeMonic, Algebra.Generators.ofComp_toAlgHom_monomial_sumElim, MvPolynomial.exists_finset_renameโ, Matrix.charpoly.univ_natDegree, MvPolynomial.algebraMap_eq, MvPolynomial.eval_toMvPolynomial, Algebra.Presentation.algebraTensorAlgEquiv_symm_relation, Algebra.Generators.aeval_val_eq_zero, MvPolynomial.coeffsIn_pow, MvPolynomial.esymmAlgHom_apply, MvPolynomial.monomial_eq, MvPolynomial.aeval_eq_evalโHom, MvPolynomial.rename_prod_mk_evalโ, AlgebraicIndependent.aevalEquivField_apply_coe, MvPolynomial.IsSymmetric.smul, MvPolynomial.aeval_C, MvPolynomial.toMvPowerSeries_pUnitAlgEquiv, MvPolynomial.transcendental_polynomial_aeval_X, MvPowerSeries.coeff_invOfUnit, MvPolynomial.aeval_comp_expand, Algebra.Generators.naive_ฯ, AlgebraicIndependent.aevalEquiv_apply_coe, MvPolynomial.rename_C, MvPolynomial.HomogeneousSubmodule.gradedMonoid, StandardEtalePresentation.aeval_val_equivMvPolynomial, MvPolynomial.aevalTower_comp_toAlgHom, MvPolynomial.zeroLocus_vanishingIdeal_galoisConnection, MvPolynomial.restrictSupport_add, MvPolynomial.evalโ_X_pow, MvPolynomial.zeroLocus_span, MvPolynomial.IsHomogeneous.rename_isHomogeneous, WittVector.polyOfInterest_vars_eq, MvPolynomial.isNoetherianRing, MvPolynomial.pderiv_inr_universalFactorizationMap_X, MvPolynomial.sumAlgEquiv_symm_apply, MvPolynomial.evalโ_pUnitAlgEquiv_symm, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul, MvPolynomial.dvd_C_iff_exists, Algebra.Generators.ker_eq_ker_aeval_val, Algebra.Generators.ker_ofAlgHom, MvPolynomial.supported_empty, MvPolynomial.C_mem_pow_idealOfVars_iff, instIsAlgebraicMvPolynomialOfNoZeroDivisors_1, distribMulActionHom_ext'_iff, KaehlerDifferential.mvPolynomialBasis_repr_D, WeierstrassCurve.Jacobian.polynomialX_eq, MvPolynomial.aeval_C_comp_left, MvPolynomial.transcendental_X, MvPolynomial.C_mul_X_pow_eq_monomial, MvPolynomial.degrees_rename_of_injective, PolynomialLaw.range_ฯ, MvPolynomial.psum_eq_mul_esymm_sub_sum, MvPolynomial.mapAlgHom_apply, Algebra.Generators.cotangentRestrict_mk, MvPolynomial.optionEquivLeft_monomial, MvPolynomial.rename_eq_zero_iff_of_injective, Algebra.Generators.H1Cotangent.ฮด_eq_ฮดAux, Algebra.SubmersivePresentation.ofSubsingleton_algebra_smul, KaehlerDifferential.mvPolynomialBasis_repr_comp_D, LieAlgebra.rank_eq_natTrailingDegree, WittVector.bindโ_onePoly_wittPolynomial, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, MvPolynomial.optionEquivLeft_symm_apply, MvPolynomial.algebraTensorAlgEquiv_tmul, MvPolynomial.mem_support_coeff_finSuccEquiv, Algebra.Generators.aeval_val_ฯ', MvPolynomial.support_sub, Algebra.Generators.Hom.toAlgHom_id, Algebra.Generators.Hom.comp_val, MvPolynomial.comap_apply, MvPolynomial.vars_rename, WittVector.bindโ_zero_wittPolynomial, StandardEtalePresentation.toPresentation_val, MvPolynomial.rename_comp_bindโ, MvPolynomial.zeroLocus_top, MvPolynomial.aeval_id_eq_joinโ, MvPolynomial.rename_X, MvPolynomial.pUnitAlgEquiv_monomial, Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero, Polynomial.homogenize_sub, MvPolynomial.mem_ideal_span_monomial_image_iff_dvd, Matrix.charpoly.univ_map_evalโHom, MvPolynomial.comap_id_apply, MvPolynomial.aeval_one_tmul, MvPolynomial.monomial_pow, prod_antidiagonal_swap, MvPolynomial.degreeOf_sub_lt, MvPolynomial.smul_eq_C_mul, MvPolynomial.finSuccEquiv_rename_finSuccEquiv, MvPolynomial.rename_expand, MvPolynomial.homogeneousSubmodule_one_pow, Algebra.Generators.fg_ker_of_finitePresentation, MvPolynomial.prod_X_pow, MvPolynomial.universalFactorizationMapPresentation_algebra_smul, MonomialOrder.degree_smul, Algebra.FiniteType.instMvPolynomialOfFinite, MvPolynomial.derivation_C_mul, MvPolynomial.aeval_sumElim_pderiv_inl, MvPolynomial.monomial_one_dvd_monomial_one, AnalyticAt.aeval_mvPolynomial, MvPolynomial.tensorEquivSum_one_tmul_X, LinearMap.polyCharpoly_coeff_eq_zero_iff_of_basis, MvPolynomial.totalDegree_sub_C_le, MvPolynomial.supported_univ, MvPolynomial.isSymmetric_rename, MvPolynomial.universalFactorizationMap_freeMonic, Algebra.Generators.Hom.toAlgHom_monomial, MonomialOrder.sPolynomial_mem_ideal, MvPolynomial.mem_ideal_of_coeff_mem_ideal, MvPolynomial.irreducible_of_totalDegree_eq_one, MvPolynomial.universalFactorizationMapPresentation_val, MvPolynomial.rename_comp_rename, MonomialOrder.leadingCoeff_sub_of_lt, MvPolynomial.coe_expand, MvPolynomial.aeval_sumElim, MvPolynomial.universalFactorizationMapPresentation_ฯ', MvPolynomial.aeval_comp_rename, KaehlerDifferential.mvPolynomialBasis_repr_symm_single, MvPolynomial.mem_symmetricSubalgebra, MvPolynomial.support_rename_killCompl_subset, MvPolynomial.evalโ_rename_prod_mk, AlgebraicIndependent.aevalEquivField_algebraMap_apply_coe, Algebra.IsAlgebraic.rank_fractionRing_mvPolynomial, MvPolynomial.coeff_linearCombination_X_pow_of_fintype, MvPolynomial.mapAlgHom_coe_ringHom, bindโ_wittPolynomial_xInTermsOfW, Algebra.FinitePresentation.out, MvPolynomial.rename_leftInverse, Algebra.FiniteType.iff_quotient_mvPolynomial'', Algebra.Presentation.quotientEquiv_mk, MvPolynomial.esymmAlgHom_fin_bijective, MvPolynomial.esymmAlgEquiv_apply, Polynomial.homogenize_C, MvPolynomial.evalโAlgHom_X, MvPolynomial.mem_vanishingIdeal_iff, MvPolynomial.mem_vanishingIdeal_singleton_iff, MonomialOrder.div, WittVector.mul_polyOfInterest_aux5, MvPolynomial.expand_zmod, MvPolynomial.aeval_zero', MvPolynomial.weightedTotalDegree_rename_of_injective, MvPolynomial.range_mapAlgHom, MvPolynomial.irreducible_sumSMulXSMulY, MvPolynomial.mem_ideal_span_monomial_image, MvPolynomial.rename_toMvPolynomial, MvPolynomial.aeval_rename, WittVector.bindโ_frobeniusPolyRat_wittPolynomial, MvPolynomial.optionEquivLeft_symm_C_X, WittVector.aeval_verschiebungPoly, MvPolynomial.evalโHom_bindโ, Polynomial.homogenize_X, MvPolynomial.finSuccEquiv_X_zero, MvPolynomial.degreeOf_eq_natDegree, MonomialOrder.degree_sub_leadingTerm_lt_degree, MonomialOrder.sPolynomial_mem_sup_ideal, MvPolynomial.bindโ_X_right, MvPolynomial.coeff_rename_eq_zero, MvPolynomial.evalโHom_C_left, MvPolynomial.transcendental_supported_polynomial_aeval_X_iff, MvPolynomial.aeval_monomial, StandardEtalePresentation.toPresentation_relation, DividedPowerAlgebra.dp_smul, Polynomial.toMvPolynomial_injective, MvPolynomial.coeff_eval_eq_eval_coeff, MvPolynomial.C_pow, LinearMap.polyCharpoly_natDegree, Algebra.PreSubmersivePresentation.ofHasCoeffs_val, MvPolynomial.C_sub, Algebra.Generators.self_algebra_algebraMap, MvPolynomial.quotientEquivQuotientMvPolynomial_rightInverse, WittVector.mul_polyOfInterest_aux3, MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_smul, MvPolynomial.C_dvd_iff_zmod, MvRatFunc.rank_eq_max_lift, MvPolynomial.aeval_prod, MvPolynomial.homogeneousSubmodule_mul, Matrix.toMvPolynomial_mul, Polynomial.Bivariate.pderiv_one_equivMvPolynomial, MvPolynomial.exists_restrict_to_vars, wittStructureInt_rename, MvPolynomial.algebraTensorAlgEquiv_symm_monomial, FirstOrder.Ring.mvPolynomial_zeroLocus_definable, MvPolynomial.aevalTower_algebraMap, MvPolynomial.optionEquivLeft_elim_eval, MvPolynomial.optionEquivLeft_symm_X, MvPolynomial.renameEquiv_symm, MvPolynomial.eval_expand, MvPolynomial.aeval_comp_toMvPolynomial, MvPolynomial.supportedEquivMvPolynomial_symm_C, MvPolynomial.killCompl_monomial_eq_monomial_comapDomain_of_subset, MvPolynomial.evalโAlgHom_apply, MvPolynomial.tensorEquivSum_X_tmul_one, MvPolynomial.instIsMaximalVanishingIdealSingletonForallSet, MvPolynomial.expand_mul_eq_comp, MvPolynomial.evalโ_pUnitAlgEquiv, MvPolynomial.killCompl_monomial, Polynomial.map_map_freeMonic, MvPolynomial.supported_eq_range_rename, MvPolynomial.rename_hsymm, MonomialOrder.sPolynomial_decomposition', MvPolynomial.transcendental_supported_X, DividedPowerAlgebra.dp_add, MvPolynomial.aeval_natDegree_le, MvPolynomial.optionEquivLeft_symm_C_C, C_p_pow_dvd_bindโ_rename_wittPolynomial_sub_sum, Algebra.Generators.Hom.algebraMap_toAlgHom, MvPolynomial.IsSymmetric.sub, WittVector.coeff_frobenius, Algebra.Generators.comp_ฯ, DividedPowerAlgebra.dp_null_of_ne_zero, MvPolynomial.tensorEquivSum_C_tmul_C, MvPolynomial.IsHomogeneous.finSuccEquiv_coeff_isHomogeneous, WittVector.wittSub_zero, DividedPowerAlgebra.mkRingHom_C, MvPolynomial.instIsDomainOfIsCancelAdd, MvPowerSeries.subst_coe, MvPolynomial.mapEquivMonic_symm_map_algebraMap, MvPolynomial.coe_aeval_eq_eval, DividedPowerAlgebra.prod_dp, exists_integral_inj_algHom_of_fg, MvPolynomial.instIsLocalHomRingHomC, MvPolynomial.coeff_add_pow, Matrix.charpoly.univ_coeff_card, Polynomial.Bivariate.equivMvPolynomial_C_C, MonomialOrder.degree_sub_of_lt, DividedPowerAlgebra.mkAlgHom_C, MvPolynomial.monomial_single_add, wittPolynomial_eq_sum_C_mul_X_pow, Polynomial.homogenize_one, Algebra.Generators.ker_naive, instFreeMvPolynomialKaehlerDifferential, MvPolynomial.hom_bindโ, MvPolynomial.coeff_expand_zero, MvPolynomial.C_dvd_iff_map_hom_eq_zero, rank_mvPolynomial_mvPolynomial, MvPolynomial.isMaximal_iff_eq_vanishingIdeal_singleton, Algebra.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial, Matrix.mvPolynomialX_mapMatrix_aeval, MvPolynomial.algebraMap_def, MvPolynomial.supported_eq_vars_subset, DividedPowerAlgebra.embed_def, MonomialOrder.degree_sub_leadingTerm_lt_iff, MvPolynomial.IsHomogeneous.coeff_isHomogeneous_of_optionEquivLeft_symm, Polynomial.aeval_homogenize_of_eq_one, MonomialOrder.degree_sub_leadingTerm_le, Polynomial.homogenize_dvd, MvPolynomial.rename_eq, MvPolynomial.totalDegree_coeff_optionEquivLeft_le, MvPolynomial.coeff_mul, MvPolynomial.evalโHom_smul, MvPolynomial.mapEquivMonic_symm_map, MvPolynomial.mem_ideal_span_X_image, MvPolynomial.isHomogeneous_X_pow, Algebra.SubmersivePresentation.basisDeriv_apply, MvPolynomial.bindโ_monomial, LinearMap.polyCharpoly_coeff_eval, MonomialOrder.degree_smul_of_mem_nonZeroDivisors, Algebra.Presentation.mem_ker_naive, MvPolynomial.C_eq_smul_one, MvPowerSeries.coeff_mul, MvPolynomial.coeff_killCompl, MvPolynomial.esymmAlgHom_surjective, MvPolynomial.aevalTower_ofNat, MvPolynomial.killCompl_monomial_eq_zero_of_notMem_range, MvPolynomial.WeightedHomogeneousSubmodule.gradedMonoid, MvPolynomial.esymmAlgEquiv_symm_apply, instIsPushoutFractionRingMvPolynomial_1, MvPolynomial.rename_surjective, MvPolynomial.evalโHom_comp_expand, Polynomial.toMvPolynomial_C, MonomialOrder.degree_pow_of_pow_leadingCoeff_ne_zero, Algebra.Generators.Hom.equivAlgHom_apply_coe, Algebra.Generators.C_mul_X_sub_one_mem_ker, MvPolynomial.universalFactorizationMapPresentation_jacobian, DividedPowerAlgebra.dp_eq_mkRingHom, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap, MvPolynomial.esymmAlgHom_injective, MvPolynomial.commAlgEquiv_C_X, MvPolynomial.expand_zero_apply, Polynomial.coeff_freeMonic, Polynomial.UniversalFactorizationRing.fromTensor_comp_universalFactorizationMap', MvPolynomial.renameSymmetricSubalgebra_apply_coe, Algebra.FinitePresentation.iff_quotient_mvPolynomial', MvPolynomial.monomial_dvd_monomial, MvPolynomial.coe_mapEquivMonic_comp, MvPolynomial.transcendental_supported_polynomial_aeval_X, instIsPushoutFractionRingMvPolynomial, MvPolynomial.eval_polynomial_eval_finSuccEquiv, MvPolynomial.constantCoeff_comp_algebraMap, LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly, DividedPowerAlgebra.dp_null, MvPolynomial.pderiv_inl_universalFactorizationMap_X, MvPolynomial.instFaithfulSMul, MvPolynomial.rename_id, Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val, MvPolynomial.idealOfVars_fg, MvPolynomial.rTensorAlgHom_apply_eq
|
instAddZeroClass ๐ | CompOp | 616 mathmath: MvPolynomial.is_id, MvPolynomial.funext_iff, MvPolynomial.eval_indicator_apply_eq_one, Height.logHeight_eval_ge, sum_toMultiset, finite_of_degree_le, mulHom_ext'_iff, MvPolynomial.coe_C, MvPolynomial.map_bindโ, degree_eq_sum, MvPolynomial.map_mapRange_eq_iff, MvPowerSeries.weightedOrder_monomial, MvPolynomial.map_comp_C, MvPolynomial.evalโHom_X, MvPolynomial.toMvPowerSeries_uniformContinuous, MonomialOrder.monic_X_sub_C, MvPolynomial.hom_C, Polynomial.homogenize_map, MvPolynomial.degrees_monomial, mapDomain.addMonoidHom_comp, Ideal.mem_span_iff_exists_isHomogeneous, toMultiset_strictMono, WeierstrassCurve.Projective.eval_polynomial, MvPolynomial.weightedDegree_eq_zero_iff, MvPolynomial.universalFactorizationMap_comp_map, singleAddHom_apply, MvPolynomial.IsSymmetric.map, FreeAbelianGroup.toFinsupp_toFreeAbelianGroup, MvPolynomial.isEmptyRingEquiv_apply, MvPolynomial.ker_map, MvPolynomial.map_leftInverse, MvPolynomial.optionEquivLeft_C, MvPolynomial.iterToSum_sumToIter, constantCoeff_wittStructureRat, Algebra.Generators.toAlgHom_ofComp_localizationAway, MvPolynomial.evalโHom_monomial, weight_single_one_apply, mapDomain_comapDomain_nat_add_one, WeierstrassCurve.Jacobian.baseChange_polynomialZ, Algebra.Presentation.localizationAway_relation, sigmaFinsuppAddEquivDFinsupp_apply, MvPolynomial.monomial_finsupp_sum_index, prod_toMultiset, toMultiset_zero, MvPolynomial.bindโ_comp_C, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C, MvPolynomial.evalโ_zero'_apply, MvPolynomial.degreeOf_C, WeierstrassCurve.Projective.polynomial_relation, le_weight_of_ne_zero', MvPolynomial.mvPolynomialEquivMvPolynomial_symm_apply, AlgebraicIndependent.repr_ker, MvPolynomial.mem_range_map_iff_coeffs_subset, MvPolynomial.exists_dvd_map_of_isAlgebraic, AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin, AnalyticOnNhd.eval_linearMap', MvPolynomial.bindโ_C_left, MvPolynomial.map_comp_rename, Polynomial.eval_eq_div_eval_toTupleMvPolynomial, WeierstrassCurve.Jacobian.eval_polynomialY, MvPolynomial.constantCoeff_rename, MvPolynomial.map_bindโ, MvPolynomial.iterToSum_C_X, MvPolynomial.map_evalโ, MvPolynomial.eval_map, MvPolynomial.map_evalโHom, char_dvd_card_solutions_of_add_lt, MvPolynomial.comp_evalโHom, MvPolynomial.aeval_eq_eval, MvPolynomial.schwartz_zippel_totalDegree, Algebra.SubmersivePresentation.map_jacobianOfHasCoeffs, MvPolynomial.le_weightedTotalDegree, MvPolynomial.evalโHom_C_id_eq_joinโ, toMultiset_toFinsupp, MvPolynomial.eval_mem, ax_grothendieck_of_definable, MvPolynomial.pow_idealOfVars, MvPolynomial.joinโ_comp_map, MvPolynomial.idealOfVars_eq_restrictSupportIdeal, Height.logHeight_eval_ge', MvPolynomial.eval_rename_prod_mk, coeFnAddHom_apply, MvPolynomial.optionEquivRight_C, MvPolynomial.map_mvPolynomial_eq_evalโ, MvPolynomial.eval_evalโ, MvPolynomial.aevalTower_comp_C, MvPolynomial.totalDegree_eq, MvPolynomial.evalโ_id, MvPolynomial.evalโHom_C_eq_bindโ, mapRange.addMonoidHom_apply, MvPolynomial.mem_pow_idealOfVars_iff, MvPolynomial.constantCoeff_C, MvPowerSeries.trunc_C, MvPolynomial.map_map, MvPolynomial.evalโHom_comp_bindโ, MvPolynomial.degrees_def, MvPolynomial.mvPolynomialEquivMvPolynomial_apply, sigmaFinsuppAddEquivDFinsupp_symm_apply, Module.End.ringHomEndFinsupp_apply_apply, MvPolynomial.weightedHomogeneousComponent_zero, MvPolynomial.esymmAlgHomMonomial_single, MvPolynomial.homogeneousComponent_C_mul, MvPolynomial.IsHomogeneous.map, liftAddHom_comp_single, MvPolynomial.map_expand, card_toMultiset, MvPolynomial.map_aeval, Sym.coe_equivNatSum_symm_apply, MvPolynomial.map_frobenius_expand, Height.logHeight_eval_le', FirstOrder.Ring.lift_genericPolyMap, MvPolynomial.expand_char, MvPolynomial.evalโHom_congr, WeierstrassCurve.Jacobian.eval_polynomialX_of_Z_ne_zero, MvPolynomial.map_rename, MvPolynomial.killCompl_C, MvPowerSeries.weightedOrder_monomial_of_ne_zero, MvPolynomial.eval_comp_toMvPolynomial, Algebra.Generators.H1Cotangent.ฮดAux_C, Algebra.Generators.ofComp_val, Algebra.Presentation.map_relationOfHasCoeffs, MvPolynomial.evalโ_map, MvPolynomial.X_mul_pderiv_monomial, MvPolynomial.map_esymm, MvPolynomial.expand_C, MonomialOrder.eq_C_of_degree_eq_zero, MvPolynomial.coeffs_C, MvPolynomial.optionEquivRight_X_none, toMultiset_apply, WeierstrassCurve.Jacobian.polynomialY_eq, WeierstrassCurve.Jacobian.eval_polynomialX, MvPolynomial.C_apply, WeierstrassCurve.Projective.eval_polynomialX, WeierstrassCurve.Projective.baseChange_polynomial, Matrix.toMvPolynomial_map, sigmaFinsuppEquivDFinsupp_add, MvPolynomial.coeff_C, WeierstrassCurve.Jacobian.eval_polynomialY_of_Z_ne_zero, MvPolynomial.bindโ_map, weight_single, constantCoeff_wittStructureInt, MvPolynomial.eval_ofNat, toFreeAbelianGroup_comp_singleAddHom, xInTermsOfW_eq, MvPolynomial.eval_eq_eval_mv_eval', MvPolynomial.degrees_map_of_injective, MvPolynomial.ACounit_C, MvPolynomial.evalโHom_zero_apply, MvPolynomial.degrees_C, WeierstrassCurve.Jacobian.polynomial_relation, MvPolynomial.eval_prod, MvPolynomial.C_mul_X_eq_monomial, Algebra.Presentation.comp_aeval_relation_inl, MvPolynomial.C_0, MvPolynomial.bindโ_monomial, MvPolynomial.monomialOneHom_apply, MvPolynomial.pderiv_sumToIter, MvPolynomial.coeff_homogeneousComponent, MvPolynomial.totalDegree_C, WeierstrassCurve.Projective.polynomialZ_eq, FreeAbelianGroup.equivFinsupp_symm_apply, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_C', MvPolynomial.coeff_C_mul, MvPolynomial.quotient_map_C_eq_zero, MvPolynomial.iterToSum_X, MvPolynomial.C_mul_monomial, comp_liftAddHom, MvPolynomial.pow_idealOfVars_eq_span, AnalyticOnNhd.eval_linearMap, mapRange.addMonoidHom_toZeroHom, MvPolynomial.commAlgEquiv_C, MvPolynomial.coeff_zero_C, MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported, MonomialOrder.monic_X_add_C, MvPolynomial.bindโ_monomial_one, MvPolynomial.commAlgEquiv_X, MvPolynomial.mapEquiv_apply, MvPolynomial.evalโHom_congr', Matrix.charpoly.univ_coeff_evalโHom, MvPolynomial.instCharZero, MvPolynomial.C_1, MvPolynomial.evalโHom_X', IsNonarchimedean.eval_mvPolynomial_le, Algebra.SubmersivePresentation.map_invJacobianOfHasCoeffs, wittPolynomial_one, MvPowerSeries.coeff_homogeneousComponent, MvPolynomial.eval_eq', degree_apply, exists_le_degree_eq, FreeAbelianGroup.toFinsupp_comp_toFreeAbelianGroup, MvPolynomial.evalโ_C, IsLocalization.Away.mvPolynomialQuotientEquiv_apply, MvPolynomial.C_add, toFreeAbelianGroup_single, MvPolynomial.isHomogeneous_C_mul_X, Algebra.Generators.localizationAway_ฯ, MvPolynomial.mapAlgEquiv_apply, WittVector.frobeniusPoly_zmod, finite_of_nat_weight_le, MvPolynomial.eval_neg, MvPolynomial.tensorEquivSum_one_tmul_C, WeierstrassCurve.Jacobian.baseChange_polynomialY, MvPolynomial.map_ofNat, MvPolynomial.evalโHom_rename, MvPolynomial.bindโ_id, le_degree, MvPolynomial.degree_degLexDegree, WeierstrassCurve.Projective.baseChange_polynomialY, MvPolynomial.algebraMap_apply, le_weight, LinearMap.toMvPolynomial_baseChange, MvPolynomial.IsWeightedHomogeneous.sum_weight_X_mul_pderiv, MvPowerSeries.truncFinset_C, MvPolynomial.C_surjective, MvPolynomial.isEmptyRingEquiv_symm_apply, MvPolynomial.hom_eq_hom, Polynomial.eval_homogenize, mem_toMultiset, MvPolynomial.bindโ_C_right, MvPolynomial.coe_coeffs_map, MvPowerSeries.truncFinset_map, MonomialOrder.degree_X_sub_C, MvPolynomial.aevalTower_C, MvPolynomial.map_expand_pow_char, xInTermsOfW_aux, coe_curryAddEquiv, MvPolynomial.mapRange_eq_map, MvPolynomial.monomial_mem_pow_idealOfVars_iff, MvPolynomial.totalDegree_eq_zero_iff_eq_C, WeierstrassCurve.Projective.eval_polynomialX_of_Z_ne_zero, MvPolynomial.evalโHom_zero', Polynomial.Bivariate.equivMvPolynomial_symm_C, MvPolynomial.map_hsymm, MvPolynomial.combinatorial_nullstellensatz_exists_linearCombination, wittStructureRat_rec, MvPolynomial.expand_eq_C, MvPowerSeries.le_weightedOrder_subst, count_toMultiset, FreeAbelianGroup.toFinsupp_of, MvPolynomial.degrees_map_le, LinearMap.polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff, MvPolynomial.eval_eq, MvPolynomial.isUnit_iff_eq_C_of_isReduced, MvPolynomial.psum_zero, MvPolynomial.eval_add, WeierstrassCurve.Projective.map_polynomialX, Algebra.SubmersivePresentation.map_jacobianRelationsOfHasCoeffs, MvPowerSeries.trunc_map, weight_single_index, WeierstrassCurve.Jacobian.baseChange_polynomial, MvPolynomial.eval_monomial, degree_preimage_add, MonomialOrder.degree_C, liftAddHom_apply, MvPolynomial.coe_evalโHom, MvPolynomial.vars_C_mul, AbsoluteValue.eval_mvPolynomial_le, Algebra.Generators.toAlgHom_ofComp_rename, wittStructureRat_rec_aux, WeierstrassCurve.Projective.eval_polynomialZ, Algebra.Generators.ker_localizationAway, DegLex.lt_iff, MvPolynomial.constantCoeff_smul, MvPolynomial.algHom_C, MvPolynomial.leadingCoeff_toLex_C, MvPowerSeries.coeff_weightedHomogeneousComponent, MvPolynomial.eval_pow, MvPowerSeries.order_le, MvPolynomial.evalโHom_zero'_apply, degLex_def, AlgebraicIndependent.mvPolynomialOptionEquivPolynomialAdjoin_apply, mapRange.addMonoidHom_comp, MvPolynomial.derivation_C, Height.mulHeight_eval_ge, MvPolynomial.dvd_smul_X_iff_exists, MvPolynomial.schwartz_zippel_sup_sum, MvPolynomial.mem_map_C_iff, MvPolynomial.prime_C_iff, MvPolynomial.eval_mul, degree_comapDomain_le_of_canonicallyOrderedAdd, MvPolynomial.universalFactorizationMapPresentation_relation, MvPolynomial.aevalTower_comp_algebraMap, MvPolynomial.evalโ_zero_apply, toMultiset_add, MonomialOrder.monic_C_one, MvPolynomial.eq_C_of_isEmpty, WeierstrassCurve.Projective.polynomialX_eq, Multiset.toFinsupp_symm_apply, MvPolynomial.monomial_zero', FreeAbelianGroup.equivFinsupp_apply, Polynomial.homogenize_C_mul, MvPowerSeries.exists_coeff_ne_zero_and_order, MvPolynomial.homogeneousComponent_apply, MvPolynomial.eval_indicator_apply_eq_zero, MvPolynomial.sumToIter_iterToSum, MvPolynomial.map_surjective_iff, constantCoeff_wittPolynomial, WeierstrassCurve.Projective.polynomialY_eq, MvPolynomial.aeval_eq_constantCoeff_of_vars, WeierstrassCurve.Projective.negDblY_eq, MvPolynomial.map_injective_iff, MvPolynomial.map_injective, MvPolynomial.constantCoeff_monomial, MvPolynomial.smul_eval, MvPolynomial.evalโHom_zero, MvPolynomial.C_eq_zero, MvPolynomial.supDegree_toLex_C, WeierstrassCurve.Projective.eval_polynomialY_of_Z_ne_zero, MvPolynomial.aeval_zero, MvPolynomial.hom_congr_vars, MvPolynomial.support_map_of_injective, MvPolynomial.constantCoeff_X, WittVector.frobeniusPolyAux_eq, WeierstrassCurve.Projective.baseChange_polynomialX, MvPolynomial.C_mul', MvPolynomial.isEmptyAlgEquiv_apply, MvPolynomial.bindโ_X_right, Algebra.Generators.cMulXSubOneCotangent_eq, MvPolynomial.map_C, MvPolynomial.C_dvd_iff_dvd_coeff, MvPolynomial.pderiv_C_mul, Matrix.toMvPolynomial_eval_eq_apply, WittVector.constantCoeff_wittMul, MvPolynomial.funext_set_iff, MvPolynomial.map_monomial, MvPolynomial.vars_map_of_injective, MvPolynomial.aeval_map_algebraMap, Algebra.Generators.Hom.toAlgHom_C, MvPolynomial.finSuccEquiv_comp_C_eq_C, MvPolynomial.esymmAlgHom_zero, char_dvd_card_solutions, WeierstrassCurve.Jacobian.polynomialZ_eq, MvPolynomial.evalโHom_map_hom, MvPolynomial.finSuccEquiv_eq, char_dvd_card_solutions_of_sum_lt, RingHom.IsStandardSmooth.exists_etale_mvPolynomial, MvPolynomial.homogeneousComponent_zero, MvPolynomial.ker_evalโHom_universalFactorizationMap, addHom_ext'_iff, MvPolynomial.coeff_map, MvPolynomial.monomial_sum_index, Matrix.mvPolynomialX_mapMatrix_eval, toFreeAbelianGroup_toFinsupp, MonomialOrder.degree_eq_zero_iff, MvPolynomial.isEmptyRingEquiv_symm_toRingHom, MonomialOrder.leadingTerm_C, MvPolynomial.quotientEquivQuotientMvPolynomial_leftInverse, MvPowerSeries.weightedOrder_eq_nat, Height.mulHeight_eval_le, MvPowerSeries.totalDegree_trunc', MvPolynomial.aeval_bindโ, sigmaFinsuppLequivDFinsupp_symm_apply, MvPolynomial.counit_surjective, WeierstrassCurve.Projective.negDblY_eq', MvPolynomial.monomial_mem_homogeneousSubmodule_pow_degree, Multiset.toFinsupp_toMultiset, LinearMap.polyCharpolyAux_coeff_eval, MvPolynomial.map_rightInverse, MvPolynomial.killCompl_map, MvPolynomial.dvd_X_iff_exists, MvPolynomial.evalโHom_eq_zero, MvPolynomial.instCharP, MonomialOrder.leadingCoeff_C, MvPolynomial.ker_mapAlgHom, degree_preimage_nsmul, WittVector.constantCoeff_wittAdd, MvPowerSeries.exists_coeff_ne_zero_and_weightedOrder, MvPolynomial.eval_sub, Height.logHeight_eval_le, MvPolynomial.pderiv_pow, constantCoeff_wittStructureRat_zero, WeierstrassCurve.Jacobian.map_polynomialZ, MvPolynomial.bindโ_C_right, add_closure_setOf_eq_single, mapRange.addEquiv_toAddMonoidHom, MvPolynomial.constantCoeff_eq, LinearMap.toMvPolynomial_constantCoeff, WeierstrassCurve.Projective.map_polynomialZ, MvPolynomial.eval_rename, MvPolynomial.mkDerivationโ_C, witt_structure_prop, MvPowerSeries.weightedOrder_le, MvPolynomial.map_surjective, WittVector.constantCoeff_wittNSMul, MvPolynomial.evalโ_map_comp_C, MvPolynomial.optionEquivRight_apply, MvPolynomial.finSuccEquiv_apply, MvPolynomial.C_eq_coe_nat, LinearMap.snd_prodOfFinsuppNat, MvPolynomial.bindโ_comp_bindโ, toFinset_toMultiset, degree_single, WeierstrassCurve.Jacobian.baseChange_polynomialX, applyAddHom_apply, MvPolynomial.degreeOf_mul_C_le, MvPolynomial.algebraTensorAlgEquiv_symm_map, MvPolynomial.weightedDecomposition.decompose'_eq, MvPolynomial.isHomogeneous_C_mul_X_pow, MvPolynomial.tensorEquivSum_C_tmul_one, le_weight_of_ne_zero, MvPolynomial.map_iterateFrobenius_expand, MvPolynomial.sumAlgEquiv_apply, Multiset.toFinsupp_eq_iff, MvPolynomial.degreeOf_C_mul_le, MvPolynomial.sumToIter_Xr, mapDomain.addMonoidHom_apply, WeierstrassCurve.Projective.eval_polynomial_of_Z_ne_zero, MvPolynomial.eval_toMvPolynomial, MvPolynomial.sum_C, MvPolynomial.monomial_eq, MvPolynomial.homogeneousSubmodule_eq_finsupp_supported, MvPolynomial.aeval_eq_evalโHom, MvPolynomial.vars_C, MvPolynomial.aeval_C, MvPolynomial.support_map_subset, MvPolynomial.pderiv_map, WeierstrassCurve.Jacobian.eval_polynomial, liftAddHom_singleAddHom, MvPolynomial.rename_C, toMultiset_sum, FirstOrder.realize_genericPolyMapSurjOnOfInjOn, MvPolynomial.evalโ_mul_C, range_single_one, MvPolynomial.C_neg, MvPolynomial.coeToMvPowerSeries.ringHom_apply, MvPolynomial.coeffs_map, MvPowerSeries.totalDegree_truncFinset, WeierstrassCurve.Jacobian.map_polynomial, MvPolynomial.constantCoeff_comp_C, MvPolynomial.sumAlgEquiv_symm_apply, MvPolynomial.evalโ_comp, MvPolynomial.weightedHomogeneousComponent_C_mul, WeierstrassCurve.Jacobian.eval_polynomial_of_Z_ne_zero, MvPolynomial.dvd_C_iff_exists, MvPolynomial.C_mem_pow_idealOfVars_iff, WittVector.map_frobeniusPoly, MvPolynomial.sum_eval_eq_zero, WittVector.constantCoeff_wittZSMul, WeierstrassCurve.Jacobian.polynomialX_eq, MvPolynomial.aeval_C_comp_left, MvPolynomial.C_mul_X_pow_eq_monomial, MvPowerSeries.order_monomial, MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_weight, MvPolynomial.eval_C, MvPolynomial.IsWeightedHomogeneous.C_mul, MvPolynomial.mapAlgHom_apply, liftAddHom_apply_single, mapDomain.addMonoidHom_id, degree_mapDomain_eq_of_subsingletonAddUnits, map_wittPolynomial, MvPolynomial.isLocalization_C_mk', MvPolynomial.algebraTensorAlgEquiv_tmul, MvPolynomial.vars_map, embDomain.addMonoidHom_apply, MvPolynomial.degreeOf_C_mul, MvPolynomial.C_injective, MvPolynomial.C_mul, MvPolynomial.evalโHom_eq_constantCoeff_of_vars, weight_sub_single_add, MvPolynomial.isLocalization, MvPolynomial.instExpChar, MvPolynomial.degrees_monomial_eq, MvPolynomial.IsSymmetric.C, MvPolynomial.ringHom_ext'_iff, MvPolynomial.eval_sum, MvPolynomial.smul_eq_C_mul, MvPolynomial.counitNat_C, Algebra.Presentation.HasCoeffs.relation_mem_range_map, MvPolynomial.IsHomogeneous.sum_X_mul_pderiv, MvPolynomial.derivation_C_mul, MvPolynomial.aeval_sumElim_pderiv_inl, MvPolynomial.evalโ_natCast, MvPolynomial.iterToSum_C_C, MvPolynomial.totalDegree_sub_C_le, MvPolynomial.coeffAddMonoidHom_apply, liftAddHom_symm_apply_apply, MvPolynomial.evalโ_C_mk_eq_zero, MvPolynomial.aeval_sumElim, MvPolynomial.universalFactorizationMapPresentation_ฯ', LinearMap.toMvPolynomial_eval_eq_apply, DegLex.le_iff, MvPolynomial.mapAlgHom_coe_ringHom, curryAddEquiv_symm_apply, liftAddHom_symm_apply, MvPolynomial.schwartz_zippel_sum_degreeOf, MvPolynomial.isHomogeneous_C, ax_grothendieck_of_locally_finite, degree_eq_zero_iff, toMultiset_single, Polynomial.homogenize_C, MvPolynomial.aeval_zero', MvPolynomial.counit_C, WeierstrassCurve.Projective.baseChange_polynomialZ, comapDomain.addMonoidHom_apply, MvPowerSeries.order_eq_nat, MvPolynomial.counitNat_X, MonomialOrder.degree_X_add_C, MvPolynomial.evalโHom_bindโ, MvPolynomial.bindโ_bindโ, MvPolynomial.evalโHom_bindโ, MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_degree, MvPolynomial.coeff_weightedHomogeneousComponent, WeierstrassCurve.Projective.dblX_eq, Algebra.Presentation.baseChange_relation, ax_grothendieck_univ, MvPolynomial.C_mem_coeffsIn, degree_mono, MvPolynomial.joinโ_map, MvPolynomial.evalโHom_C_left, Algebra.PreSubmersivePresentation.localizationAway_jacobiMatrix, MvPolynomial.coeff_eval_eq_eval_coeff, MvPolynomial.C_pow, MvPolynomial.coeffs_C_subset, eraseAddHom_apply, MvPolynomial.comp_C_integral_of_surjective_of_isJacobsonRing, MvPolynomial.C_sub, toMultiset_sup, MvPolynomial.quotientEquivQuotientMvPolynomial_rightInverse, MvPolynomial.pderiv_C, constantCoeff_xInTermsOfW, MvPolynomial.C_dvd_iff_zmod, Height.mulHeight_eval_le', MvPowerSeries.trunc_C_mul, WittVector.constantCoeff_wittNeg, map_wittStructureInt, MvPolynomial.constantCoeff_comp_map, MvPolynomial.optionEquivLeft_elim_eval, MvPolynomial.evalโHom_C, MvPolynomial.counitNat_surjective, DegLex.monotone_degree, MvPolynomial.sumToIter_C, Height.mulHeight_eval_ge', WeierstrassCurve.Projective.dblX_eq', MvPolynomial.eval_expand, RingHom.IsStandardSmoothOfRelativeDimension.exists_etale_mvPolynomial, MvPolynomial.supportedEquivMvPolynomial_symm_C, Matrix.toMvPolynomial_constantCoeff, MvPowerSeries.trunc'_map, MvPolynomial.evalโAlgHom_apply, MvPolynomial.C_inj, WeierstrassCurve.Jacobian.map_polynomialY, MvPolynomial.eval_X, mapDomain.addMonoidHom_comp_mapRange, Ideal.mem_span_pow_iff_exists_isHomogeneous, WeierstrassCurve.Projective.dblY_of_Y_eq', MvPolynomial.IsHomogeneous.C_mul, MvPolynomial.constantCoeff_map, AnalyticOnNhd.eval_continuousLinearMap', MvPolynomial.optionEquivLeft_symm_C_C, C_p_pow_dvd_bindโ_rename_wittPolynomial_sub_sum, MonomialOrder.C_mul_leadingCoeff_monomial_degree, nsmul_single_one_image, DegLex.lt_def, AnalyticOnNhd.eval_mvPolynomial, WeierstrassCurve.Projective.map_polynomialY, MvPolynomial.tensorEquivSum_C_tmul_C, MvPowerSeries.order_monomial_of_ne_zero, WeierstrassCurve.Projective.map_polynomial, DividedPowerAlgebra.mkRingHom_C, toMultiset_sum_single, WeierstrassCurve.Projective.eval_polynomialY, MvPolynomial.instIsLocalHomRingHomC, MvPolynomial.evalโ_eq_eval_map, weight_eq_zero_iff_eq_zero, toMultiset_map, Polynomial.Bivariate.equivMvPolynomial_C_C, Rep.barComplex.d_single, DividedPowerAlgebra.mkAlgHom_C, MvPolynomial.isWeightedHomogeneous_C, MvPolynomial.map_X, MvPolynomial.eval_assoc, ax_grothendieck_zeroLocus, wittPolynomial_eq_sum_C_mul_X_pow, mapRange.addMonoidHom_id, constantCoeff_wittStructureInt_zero, MvPolynomial.hom_bindโ, WeierstrassCurve.Jacobian.map_polynomialX, MvPolynomial.C_dvd_iff_map_hom_eq_zero, toMultiset_inf, AnalyticOnNhd.eval_continuousLinearMap, WeierstrassCurve.Jacobian.eval_polynomialZ, weight_apply, MvPolynomial.support_C, degree_def, MvPolynomial.evalโ_comp_right, MvPolynomial.weightedHomogeneousComponent_apply, coe_orderIsoMultiset, MvPolynomial.map_eval, MvPolynomial.evalโHom_smul, char_dvd_card_solutions_of_fintype_sum_lt, MvPolynomial.bindโ_monomial, LinearMap.polyCharpoly_coeff_eval, MvPolynomial.continuous_eval, MvPolynomial.C_eq_smul_one, MvPolynomial.evalโ_apply, toFreeAbelianGroup_comp_toFinsupp, toMultiset_eq_iff, MvPolynomial.map_id, MvPolynomial.evalโHom_comp_expand, Polynomial.toMvPolynomial_C, MvPowerSeries.trunc'_C, MvPolynomial.decomposition.decompose'_eq, Algebra.Generators.C_mul_X_sub_one_mem_ker, MvPolynomial.universalFactorizationMapPresentation_jacobian, MvPowerSeries.trunc'_C_mul, MvPolynomial.commAlgEquiv_C_X, MvPolynomial.expand_zero_apply, WeierstrassCurve.Projective.negDblY_of_Y_eq', MvPolynomial.eval_polynomial_eval_finSuccEquiv, MvPolynomial.constantCoeff_comp_algebraMap, MvPolynomial.sumToIter_Xl, image_pow_eq_finsuppProd_image, WittVector.constantCoeff_wittSub, MvPolynomial.counit_X, sigmaFinsuppLequivDFinsupp_apply, MvPolynomial.evalโHom_comp_C
|
instIntSMul ๐ | CompOp | โ |
instNatSMul ๐ | CompOp | 23 mathmath: MvPowerSeries.support_expand, factorization_pow, MvPowerSeries.trunc'_expand_trunc', PowerSeries.support_expand_subset, MvPolynomial.expand_monomial, PowerSeries.support_expand, MvPolynomial.coeff_expand_smul, MvPolynomial.support_expand_subset, MvPowerSeries.coeff_expand_smul, MvPowerSeries.trunc'_expand, MonomialOrder.degree_pow_le, nsmul_apply, MvPowerSeries.monomial_pow, MvPolynomial.support_expand, coe_nsmul, MvPowerSeries.expand_monomial, MonomialOrder.coeff_pow_nsmul_degree, MonomialOrder.degree_pow, MvPolynomial.monomial_pow, Nat.factorization_pow, MvPowerSeries.support_expand_subset, MvPowerSeries.monomial_smul_eq, MonomialOrder.degree_pow_of_pow_leadingCoeff_ne_zero
|
instNeg ๐ | CompOp | 21 mathmath: coe_neg, neLocus_neg, neLocus_neg_neg, mapRange_neg, subtypeDomain_neg, filter_neg, AddMonoidAlgebra.ofCoeff_neg, mapRange_neg', MonoidAlgebra.coeff_neg, sum_neg_index, erase_neg, SkewMonoidAlgebra.toFinsupp_neg, MonoidAlgebra.ofCoeff_neg, SkewMonoidAlgebra.ofFinsupp_neg, prod_neg_index, toDFinsupp_neg, neg_apply, support_neg, single_neg, DFinsupp.toFinsupp_neg, AddMonoidAlgebra.coeff_neg
|
instSub ๐ | CompOp | 45 mathmath: sub_apply, groupHomology.dโโ_single, groupHomology.dโโ_single_one_thd, neLocus_eq_support_sub, groupHomology.single_one_snd_sub_single_one_fst_mem_boundariesโ, AddMonoidAlgebra.coeff_sub, sum_sub_index, mapRange_sub', DFinsupp.toFinsupp_sub, single_sub, AddMonoidAlgebra.ofCoeff_sub, groupHomology.single_one_fst_sub_single_one_snd_mem_boundariesโ, MonoidAlgebra.ofCoeff_sub, SkewMonoidAlgebra.toFinsupp_sub, groupHomology.dโโ_single_inv_self_ฯ_sub_self_inv, groupHomology.single_one_fst_sub_single_one_fst_mem_boundariesโ, filter_sub, erase_eq_sub_single, groupHomology.H2ฯ_eq_iff, groupHomology.isBoundaryโ_iff, neLocus_sub_left, neLocus_self_sub_left, groupHomology.dโโ_single_one_fst, groupHomology.dโโ_single_self_inv_ฯ_sub_inv_self, mapRange_sub, exteriorPower.presentation_relation, update_eq_sub_add_single, toDFinsupp_sub, groupHomology.single_one_snd_sub_single_one_snd_mem_boundariesโ, SkewMonoidAlgebra.ofFinsupp_sub, groupHomology.dโโ_single_one_snd, neLocus_sub_right, subtypeDomain_sub, groupHomology.dโโ_single, coe_sub, mapDomain_sub, Module.Presentation.tautologicalRelations_relation, neLocus_self_sub_right, Module.Presentation.tautological_relation, exteriorPower.presentation.relations_relation, groupHomology.isBoundaryโ_iff, MonoidAlgebra.coeff_sub, erase_sub, support_sub, groupHomology.H1ฯ_eq_iff
|
singleAddHom ๐ | CompOp | 7 mathmath: mulHom_ext'_iff, singleAddHom_apply, liftAddHom_comp_single, toFreeAbelianGroup_comp_singleAddHom, addHom_ext'_iff, liftAddHom_singleAddHom, liftAddHom_symm_apply
|