Documentation Verification Report

Finsupp

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

Statistics

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

Cardinal

Theorems

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

(root)

Definitions

Name	Category	Theorems
`Finsupp` 📖	CompData	2184 math math: `Finsupp.coe_neg`, `Finsupp.instSMulPosReflectLE`, `MvPolynomial.pUnitAlgEquiv_symm_monomial`, `MvPowerSeries.coeff_zero_eq_constantCoeff_apply`, `TensorProduct.finsuppRight_apply`, `AddMonoidAlgebra.modOf_apply_add_self`, `Finsupp.range_mapRange`, `SkewMonoidAlgebra.ofFinsupp_eq_zero`, `Finsupp.snd_sumFinsuppLEquivProdFinsupp`, `Finsupp.sum_toMultiset`, `MvPolynomial.dvd_monomial_one_iff_exists`, `Finsupp.range_subset_insert_frange`, `LinearMap.exists_finsupp_nat_of_fin_fun_injective`, `Finsupp.fst_sumFinsuppLEquivProdFinsupp`, `Finsupp.instCanonicallyOrderedAddOfAddLeftMono`, `Finsupp.finite_of_degree_le`, `groupHomology.π_comp_H2Iso_hom_assoc`, `Finsupp.toDFinsupp_add`, `Finsupp.mulHom_ext'_iff`, `Finsupp.support_finset_sum`, `MvPowerSeries.WithPiTopology.tendsto_trunc_atTop`, `AddMonoidAlgebra.mul_single_apply`, `MvPolynomial.support_sum`, `Module.Presentation.cokernelRelations_relation`, `MonomialOrder.sPolynomial_leadingTerm_mul'`, `Module.Free.finsupp`, `Rep.coe_linearization_obj_ρ`, `Finsupp.mapRange_apply`, `Finsupp.coe_sumElim`, `MvPowerSeries.coeff_zero_eq_constantCoeff`, `MvPolynomial.support_mul`, `AddMonoidAlgebra.mapDomainRingEquiv_apply`, `HahnSeries.instNoZeroDivisorsFinsuppNat`, `groupHomology.mapCycles₂_comp_assoc`, `Orthonormal.inner_left_finsupp`, `IsSMulRegular.finsupp`, `Finsupp.mapRange.linearEquiv_refl`, `Finsupp.zero_update`, `Finsupp.Colex.addLeftStrictMono`, `Finsupp.degree_eq_sum`, `Module.Basis.end_repr_apply`, `AddMonoidAlgebra.mul_apply`, `Algebra.Presentation.differentials.comm₁₂_single`, `Finsupp.embDomain_apply`, `Nat.Prime.exists_orderOf_eq_pow_factorization_exponent`, `Finsupp.instPosSMulReflectLE`, `MvPolynomial.map_mapRange_eq_iff`, `MvPowerSeries.weightedOrder_monomial`, `Finsupp.embDomain_some_some`, `MvPowerSeries.eq_iff_frequently_trunc'_eq`, `Finsupp.single_injective`, `sigmaFinsuppEquivDFinsupp_support`, `Nat.Primes.prodNatEquiv_symm_apply`, `Nat.multiplicity_eq_factorization`, `Finsupp.neLocus_neg`, `Nat.factorization_eq_zero_of_not_dvd`, `Finsupp.mem_supported_support`, `IsPrimePow.exists_ordCompl_eq_one`, `List.toFinsupp_eq_sum_mapIdx_single`, `MvPolynomial.support_finSuccEquiv`, `MvPolynomial.rTensor_apply_tmul_apply`, `MvPolynomial.degrees_monomial`, `Nat.Prime.factorization_pos_of_dvd`, `Finsupp.mapDomain.addMonoidHom_comp`, `Finsupp.sumElim_inr`, `MvPolynomial.coeff_divMonomial`, `SkewMonoidAlgebra.toFinsupp_apply`, `Finsupp.sub_apply`, `SkewMonoidAlgebra.ofFinsupp_zero`, `groupHomology.d₁₀_single_one`, `MonomialOrder.degree_add_of_ne`, `MvPolynomial.sum_def`, `Finsupp.floorDiv_def`, `MvPolynomial.one_def`, `MvPowerSeries.coeff_mul_monomial`, `Finsupp.restrictDom_apply`, `groupHomology.boundaries₂_le_cycles₂`, `SkewMonoidAlgebra.ofFinsupp_smul`, `Multiset.toFinsupp_add`, `instIsOrderedCancelAddMonoidLexFinsupp`, `QuadraticMap.sum_polar_sub_repr_sq`, `Finsupp.curryEquiv_apply`, `Finsupp.card_Ioc`, `MvPolynomial.mem_image_support_coeff_finSuccEquiv`, `Finsupp.equivCongrLeft_apply`, `Finsupp.toMultiset_strictMono`, `MvPolynomial.scalarRTensor_apply_monomial_tmul`, `Finsupp.filter_smul`, `Module.basisUnique_repr_eq_zero_iff`, `Nat.ordCompl_le`, `MvPolynomial.weightedDegree_eq_zero_iff`, `finsuppTensorFinsupp_apply`, `Finsupp.onFinset_apply`, `Representation.ofMulActionSelfAsModuleEquiv_symm_apply`, `Rep.diagonalSuccIsoFree_inv_hom_single`, `MvPowerSeries.support_expand`, `PolynomialModule.smul_def`, `instCountableFinsupp`, `MonomialOrder.degree_monomial`, `MvPolynomial.coeff_X_mul'`, `IsBaseChange.finsuppPow`, `Finsupp.lmapDomain_id`, `IsPrimePow.minFac_pow_factorization_eq`, `Finsupp.coe_le_coe`, `NumberField.Units.fun_eq_repr`, `Finsupp.singleAddHom_apply`, `TensorProduct.equivFinsuppOfBasisLeft_symm_apply`, `factorization_pow`, `IsBaseChange.basis_repr_comp_apply`, `SkewMonoidAlgebra.toFinsupp_smul`, `Module.DualBases.basis_repr_symm_apply`, `Module.Basis.toDual_linearCombination_left`, `groupHomology.chainsMap_f_3_comp_chainsIso₃_apply`, `LinearMap.prodOfFinsuppNat_injective`, `FreeAbelianGroup.toFinsupp_toFreeAbelianGroup`, `Finsupp.sumFinsuppLEquivProdFinsupp_apply`, `IsAdjoinRootMonic.coeff_apply`, `Module.Relations.Solution.surjective_π_iff_span_eq_top`, `Finsupp.supportedEquivFinsupp_symm_single`, `groupHomology.d₃₂_single`, `Rep.coindToInd_of_support_subset_orbit`, `Representation.finsupp_apply`, `LinearMap.toMatrix_apply'`, `Finsupp.card_Ico`, `Finsupp.toColex_monotone`, `Finsupp.filter_apply_neg`, `Finsupp.mapRange.linearEquiv_toAddEquiv`, `groupHomology.mapCycles₁_comp_apply`, `groupHomology.cyclesIso₀_inv_comp_iCycles_apply`, `Rep.leftRegularHom_hom`, `Matrix.repr_toLin`, `Finsupp.embSigma_zero`, `MvPowerSeries.coeff_pow`, `PolynomialModule.add_apply`, `KaehlerDifferential.mvPolynomialBasis_repr_D_X`, `Finsupp.multiset_sum_sum_index`, `Finsupp.linearCombination_id_surjective`, `TensorProduct.sum_tmul_basis_right_injective`, `Finsupp.mem_frange_of_mem`, `Finsupp.isOrderedAddMonoid`, `Finsupp.sumElim_apply`, `Finsupp.domCongr_refl`, `Finsupp.sum_zsmul`, `Finsupp.neLocus_neg_neg`, `MvPowerSeries.constantCoeff_subst`, `Finsupp.neLocus_add_left`, `Finsupp.sumFinsuppAddEquivProdFinsupp_symm_inl`, `AddMonoidAlgebra.mapRangeAddEquiv_apply`, `Finsupp.erase_same`, `groupHomology.eq_d₃₂_comp_inv`, `AddCommMonCat.free_obj_coe`, `AList.lookupFinsupp_eq_zero_iff`, `rank_finsupp`, `LinearIndependent.linearCombination_repr`, `exteriorPower.basis_repr_ne`, `Nat.factorization_le_factorization_mul_left`, `Finsupp.if_mem_support`, `Finsupp.filter_apply_pos`, `Algebra.Presentation.differentials.comm₂₃`, `rank_finsupp_self`, `Representation.ofCoinvariantsTprodLeftRegular_mk_tmul_single`, `Finsupp.prod_add_index_of_disjoint`, `MvPowerSeries.coeff_monomial_mul`, `Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_left`, `Finsupp.weight_single_one_apply`, `MvPowerSeries.exists_finsupp_eq_lexOrder_of_ne_zero`, `Module.Basis.mk_repr`, `Module.Flat.finsupp`, `Finsupp.mapDomain_comapDomain_nat_add_one`, `MvPowerSeries.coeff_X_pow`, `MvPolynomial.support_monomial`, `Finsupp.instIsRightCancelAdd`, `sigmaFinsuppAddEquivDFinsupp_apply`, `List.toFinsupp_cons_eq_single_add_embDomain`, `MvPolynomial.monomial_finsupp_sum_index`, `Module.Relations.Solution.injective_fromQuotient_iff_ker_π_eq_span`, `Finsupp.sum_smul_index'`, `MvPolynomial.mul_def`, `Finsupp.linearEquivFunOnFinite_symm_coe`, `Module.Basis.repr_isUnitSMul`, `Finsupp.prod_toMultiset`, `Finsupp.bot_eq_zero`, `Finsupp.toMultiset_zero`, `Span.repr_def`, `Finsupp.mapRange.addEquiv_refl`, `Submodule.mem_iSup_iff_exists_finsupp`, `Finsupp.single_eq_same`, `MvPolynomial.image_comap_C_basicOpen`, `groupHomology.mem_cycles₂_iff`, `Finsupp.coe_ceilDiv_def`, `groupHomology.single_isCycle₂_iff_inv`, `Finsupp.le_weight_of_ne_zero'`, `MvPolynomial.mem_support_iff`, `Finsupp.filter_eq_indicator`, `DFinsupp.toFinsupp_add`, `Finsupp.subtypeDomain_add`, `Module.FaithfullyFlat.finsupp`, `groupHomology.cyclesMap_comp_isoCycles₂_hom`, `Finsupp.sum_smul_index_linearMap'`, `Finsupp.support_single_add_single`, `linearIndependent_iff_injective_finsuppLinearCombination`, `MvPolynomial.notMem_support_iff`, `Finsupp.sum_single_add_single`, `Finsupp.equivFunOnFinite_apply`, `AddMonoidAlgebra.mapDomainAddEquiv_apply`, `MvPolynomial.scalarRTensor_apply_X_tmul_apply`, `Nat.factorization_eq_of_coprime_right`, `groupHomology.comp_d₂₁_eq`, `Nat.factorization_mul_apply_of_coprime`, `Finsupp.smulCommClass`, `Finsupp.support_zero`, `groupHomology.mapCycles₁_comp_assoc`, `Finsupp.mapRange_neg`, `Module.Basis.prod_repr_inl`, `MvPowerSeries.LinearTopology.basis_le_iff`, `groupHomology.toCycles_comp_isoCycles₂_hom_assoc`, `MonomialOrder.degree_sub_le`, `Nat.ordCompl_dvd_ordCompl_iff_dvd`, `Finsupp.subtypeDomain_neg`, `Sym.coe_equivNatSum_apply_apply`, `Finsupp.sigmaFinsuppAddEquivPiFinsupp_apply`, `Equiv.finsuppUnique_symm_apply_support_val`, `Finsupp.neLocus_self_add_left`, `Module.Relations.Solution.surjective_fromQuotient_iff_surjective_π`, `Nat.ordProj_of_not_prime`, `Finsupp.filter_neg`, `Finsupp.linearCombination_zero_apply`, `MvPowerSeries.min_lexOrder_le`, `Finset.mem_finsuppAntidiag`, `Finsupp.mem_supported`, `MonoidAlgebra.single_one_mul_apply`, `Module.Basis.repr_self_apply`, `Finsupp.mem_range_mapDomain_iff`, `FractionalIdeal.count_finsuppProd`, `Cardinal.mk_finsupp_lift_of_infinite`, `Finsupp.add_sub_single_one`, `Finsupp.mem_span_iff_linearCombination`, `Nat.pow_succ_factorization_not_dvd`, `IsLocalFrameOn.coeff_apply_of_mem`, `setBasisOfLinearIndependentOfCardEqFinrank_repr_apply`, `Algebra.Presentation.differentials.hom₁_single`, `Finsupp.Lex.addLeftMono`, `Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_right`, `Finsupp.prod_add_index`, `Finsupp.Lex.single_strictAnti`, `LinearMap.sum_repr_mul_repr_mulₛₗ`, `Finsupp.single_smul`, `Representation.ofMulAction_apply`, `Finsupp.Colex.isOrderedCancelAddMonoid`, `Finsupp.comapDomain_smul_of_injective`, `groupHomology.d₃₂_single_one_thd`, `Ideal.Filtration.mem_submodule`, `TopModuleCat.coe_freeObj`, `finTwoArrowEquiv'_apply`, `Finsupp.Colex.isStrictOrder`, `Ideal.finsuppTotal_apply_eq_of_fintype`, `groupHomology.isoCycles₁_inv_comp_iCycles_apply`, `Finsupp.erase_ne`, `KaehlerDifferential.quotKerTotalEquiv_symm_comp_D`, `strongRankCondition_iff_forall_not_injective`, `IntermediateField.LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply`, `MvPolynomial.supDegree_esymmAlgHomMonomial`, `Finsupp.support_mul`, `PowerSeries.coeff_heval`, `MvPolynomial.support_sdiff_support_subset_support_add`, `Finsupp.eq_single_iff`, `finsuppTensorFinsupp'_symm_single_eq_tmul_single_one`, `Rep.finsuppToCoinvariantsTensorFree_single`, `Module.Relations.Solution.IsPresentation.linearEquiv_symm_var`, `Finsupp.toMultiset_toFinsupp`, `Nat.Partition.toFinsuppAntidiag_mem_finsuppAntidiag`, `Module.Presentation.cokernel_relation`, `MvPolynomial.pow_idealOfVars`, `MvPolynomial.idealOfVars_eq_restrictSupportIdeal`, `groupHomology.chains₁ToCoinvariantsKer_surjective`, `Rep.coinvariantsTensorFreeLEquiv_symm_apply`, `linearIndependent_iff_ker`, `Finsupp.coeFnAddHom_apply`, `SkewMonoidAlgebra.ofFinsupp_sum`, `Rep.standardComplex.d_eq`, `Module.presentationFinsupp_G`, `Finsupp.mapRange.addEquiv_apply`, `Pi.counit_comp_finsuppLcoeFun`, `Finsupp.curryLinearEquiv_symm_apply_apply`, `Finsupp.llift_apply`, `MvPolynomial.totalDegree_eq`, `AddMonoidAlgebra.single_apply`, `Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_single`, `Finsupp.linearCombination_smul`, `Nat.factorization_factorial`, `groupHomology.cycles₁_eq_top_of_isTrivial`, `MonoidAlgebra.opRingEquiv_symm_apply`, `AddCommMonCat.free_map`, `Finsupp.erase_apply`, `Finsupp.mapRange.addMonoidHom_apply`, `Multiset.toFinsupp_sum_eq`, `MvPolynomial.mem_pow_idealOfVars_iff`, `Ideal.finsuppTotal_apply`, `Finsupp.ext_iff'`, `groupHomology.d₃₂_comp_d₂₁_assoc`, `Finsupp.neLocus_eq_support_sub`, `linearIndepOn_iff`, `Finsupp.some_zero`, `TensorProduct.equivFinsuppOfBasisLeft_apply_tmul_apply`, `Finsupp.lmapDomain_linearCombination`, `Finsupp.notMem_support_iff`, `Finsupp.range_mapRange_linearMap`, `Finsupp.sumFinsuppAddEquivProdFinsupp_symm_apply`, `MvPolynomial.support_eq_empty`, `MonomialOrder.degree_mem_support_iff`, `Module.Basis.repr_algebraMap`, `Finsupp.mapRange_neg'`, `Multiset.support_sum_subset`, `MvPolynomial.degrees_def`, `AddMonoidAlgebra.uniqueRingEquiv_apply`, `Finsupp.fun_support_eq`, `Algebra.Generators.cotangentSpaceBasis_repr_one_tmul`, `Finsupp.univ_sum_single_apply'`, `sigmaFinsuppAddEquivDFinsupp_symm_apply`, `Finsupp.iInf_ker_lapply_le_bot`, `MonoidAlgebra.uniqueRingEquiv_apply`, `Rep.coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply`, `Finsupp.basis_repr`, `Matrix.toBilin_apply`, `IsLocalRing.basisQuotient_repr`, `Module.Relations.surjective_toQuotient`, `AddEquiv.finsuppUnique_symm`, `Module.End.ringHomEndFinsupp_apply_apply`, `MvPolynomial.mem_vars`, `MonomialOrder.toSyn_strictMono`, `MvPowerSeries.coeff_X`, `List.toFinsupp_apply_fin`, `Representation.ofMulAction_single`, `AddMonoidAlgebra.opRingEquiv_symm_apply`, `groupHomology.single_one_snd_sub_single_one_fst_mem_boundaries₂`, `MvPolynomial.weightedHomogeneousComponent_zero`, `Finsupp.linearCombination_one_tmul`, `Polynomial.coeff_ofFinsupp`, `Finset.mem_finsuppAntidiag_insert`, `groupHomology.d₁₀ArrowIso_hom_left`, `Finset.support_sum_subset`, `MonomialOrder.div_single`, `Module.Basis.map_repr`, `groupHomology.cycles₁IsoOfIsTrivial_hom_apply`, `PowerSeries.support_expand_subset`, `Finsupp.liftAddHom_comp_single`, `Representation.coinvariantsFinsuppLEquiv_apply`, `Finsupp.card_toMultiset`, `Finsupp.update_self`, `LinearMap.toMatrixAlgEquiv_apply`, `Finsupp.sum_sub_index`, `Algebra.TensorProduct.basis_repr_tmul`, `Sym.coe_equivNatSum_symm_apply`, `Finsupp.disjoint_iff`, `Finsupp.comapSMul_single`, `Finsupp.lmapDomain_comp`, `groupHomology.d₂₁_single_inv_mul_ρ_add_single`, `NumberField.mixedEmbedding.stdBasis_apply_isComplex_snd`, `FirstOrder.Ring.lift_genericPolyMap`, `Finsupp.Lex.wellFounded'`, `Nat.ordCompl_dvd_ordCompl_of_dvd`, `Finsupp.supported_inter`, `MvPolynomial.expand_monomial`, `Finsupp.sum_smul_index`, `Finsupp.LinearEquiv.finsuppUnique_symm_apply`, `Finsupp.span_le_supported_biUnion_support`, `Finsupp.cons_succ`, `Finset.finsuppAntidiag_empty_of_ne_zero`, `groupHomology.d₁₀_comp_coinvariantsMk_apply`, `LinearMap.BilinForm.apply_eq_dotProduct_toMatrix_mulVec`, `KaehlerDifferential.kerTotal_eq`, `Finsupp.span_image_eq_map_linearCombination`, `MvPowerSeries.hasSum_aeval`, `Rep.diagonalSuccIsoFree_inv_hom_single_single`, `MvPowerSeries.weightedOrder_monomial_of_ne_zero`, `AddMonoidAlgebra.divOf_apply`, `LinearIndependent.repr_eq_single`, `PowerSeries.support_expand`, `Finsupp.small`, `HahnSeries.toMvPowerSeries_symm_apply_coeff`, `IsAdjoinRootMonic.basis_repr`, `Representation.leftRegular_norm_eq_zero_iff`, `Finsupp.supported_eq_span_single`, `TensorProduct.finsuppLeft_smul'`, `Finsupp.support_add_single`, `groupHomology.chainsMap_f_3_comp_chainsIso₃`, `Finsupp.mapRange.addEquiv_toEquiv`, `Nat.factorization_mul`, `groupHomology.mapCycles₁_id_comp_assoc`, `Finsupp.filter_sum`, `Finsupp.finite_support`, `Algebra.TensorProduct.basisAux_map_smul`, `Pi.basis_repr_single`, `Module.Relations.Solution.fromQuotient_toQuotient`, `groupHomology.eq_d₂₁_comp_inv`, `Finsupp.eq_option_embedding_update_none_iff`, `TensorProduct.equivFinsuppOfBasisRight_apply_tmul`, `MvPolynomial.X_mul_pderiv_monomial`, `MvPowerSeries.lexOrder_def_of_ne_zero`, `MonomialOrder.degree_add_le`, `Module.Basis.ofEquivFun_repr_apply`, `Finsupp.mapRange_sub'`, `Finsupp.supported_univ`, `Finsupp.mapDomain_surjective`, `Module.Basis.sumQuot_repr_left`, `groupHomology.mapCycles₁_comp`, `MvPowerSeries.LinearTopology.mem_basis_iff`, `Representation.ofMulAction_self_smul_eq_mul`, `Module.Basis.reindexRange_repr'`, `Finsupp.sum_ite_eq`, `Ordinal.CNF.coeff_zero_apply`, `Finsupp.indicator_of_notMem`, `MvPolynomial.coeff_expand_smul`, `Finsupp.optionElim_some`, `Finsupp.sum_fintype`, `Module.Basis.reindexRange_repr`, `Finsupp.some_add`, `Finsupp.mapRange.equiv_refl`, `Finsupp.mem_rangeSingleton_apply_iff`, `Finsupp.sigmaFinsuppLEquivPiFinsupp_symm_apply`, `TensorProduct.equivFinsuppOfBasisLeft_apply_tmul`, `PiTensorProduct.ofFinsuppEquiv'_tprod_single`, `Nat.factorization_eq_card_pow_dvd_of_lt`, `MonoidAlgebra.single_mul_apply`, `Finsupp.single_eq_zero`, `factorization_mul`, `TensorProduct.equivFinsuppOfBasisLeft_symm`, `Rep.coe_linearization_obj`, `Module.Presentation.finsupp_R`, `DFinsupp.toFinsupp_sub`, `Submodule.mulLeftMap_apply`, `AddMonoidAlgebra.neg_apply`, `TensorProduct.finsuppScalarRight_apply`, `Finsupp.zipWith_apply`, `Module.Relations.Solution.ofQuotient_var`, `BoundedContinuousFunction.mem_charPoly`, `groupHomology.mapCycles₁_comp_i`, `Finsupp.Lex.isStrictOrder`, `Finsupp.toMultiset_apply`, `Finsupp.embDomain_injective`, `MvPowerSeries.lexOrder_mul`, `BoundedContinuousFunction.charAlgHom_apply`, `Finsupp.Colex.addRightMono`, `TensorProduct.finsuppScalarRight_apply_tmul`, `MvPolynomial.support_add`, `Finsupp.coe_pointwise_smul`, `Ordinal.CNF.coeff_of_not_mem_CNF`, `Polynomial.derivativeFinsupp_apply_toFun`, `MvPolynomial.C_apply`, `Finsupp.filter_curry`, `LieAlgebra.LoopAlgebra.toFinsupp_symm_single`, `Finsupp.DegLex.single_lt_iff`, `Finsupp.add_eq_zero_iff`, `Module.Basis.repr_smul`, `Nat.ordProj_dvd_ordProj_iff_dvd`, `MvPolynomial.single_eq_monomial`, `finsuppTensorFinsupp'_single_tmul_single`, `Finsupp.mapDomain.coe_linearEquiv`, `Finsupp.single_eq_of_ne`, `AddMonoidAlgebra.grade_eq_lsingle_range`, `NumberField.canonicalEmbedding.integralBasis_repr_apply`, `Finsupp.Colex.wellFoundedLT`, `sigmaFinsuppEquivDFinsupp_add`, `MvPolynomial.coeff_C`, `Finsupp.Colex.addRightStrictMono`, `Finsupp.lcoeFun_comp_lsingle`, `Finsupp.weight_single`, `Finset.sum_apply'`, `Nat.exists_factorization_lt_of_lt`, `Finsupp.isOrderedCancelAddMonoid`, `Finsupp.embSigma_add`, `Finsupp.antidiagonal_single`, `QuadraticMap.map_finsuppSum`, `Finsupp.lcoeFun_apply`, `Finsupp.single_sub`, `Finsupp.sub_add_single_one_cancel`, `basisOfLinearIndependentOfCardEqFinrank_repr_apply`, `Finsupp.mapRange.equiv_symm`, `MvPolynomial.support_rename_of_injective`, `MvPowerSeries.monomial_def`, `PiTensorProduct.ofFinsuppEquiv_tprod_single`, `Module.Presentation.finsupp_G`, `Finsupp.toFreeAbelianGroup_comp_singleAddHom`, `Finsupp.mapDomain_injOn`, `Module.Relations.range_map`, `Nat.factorization_eq_one_of_squarefree`, `Finsupp.unique_single`, `Finsupp.le_def`, `Nat.factorization_choose_prime_pow_add_factorization`, `Module.Basis.SmithNormalForm.repr_apply_embedding_eq_repr_smul`, `DFinsupp.toFinsupp_smul`, `MvPowerSeries.le_lexOrder_iff`, `groupHomology.single_one_fst_sub_single_one_snd_mem_boundaries₂`, `Finsupp.floorDiv_apply`, `Representation.coinvariantsTprodLeftRegularLEquiv_apply`, `Finsupp.sum_ite_eq'`, `finsuppTensorFinsuppLid_symm_single_smul`, `Finsupp.ker_mapRange`, `Nat.factorization_prod_apply`, `Finsupp.erase_add`, `Multiset.toFinsupp_union`, `groupHomology.mapCycles₂_id_comp`, `MvPolynomial.scalarRTensor_apply_tmul`, `Finsupp.supported_comap_lmapDomain`, `Finsupp.update_apply`, `Finsupp.prod_zpow`, `Finsupp.rangeIcc_toFun`, `KaehlerDifferential.kerTotal_mkQ_single_algebraMap_one`, `finsuppTensorFinsupp'_symm_single_mul`, `LinearMap.polyCharpolyAux_map_eval`, `ZSpan.repr_ceil_apply`, `AddMonoidAlgebra.mapRangeRingHom_apply`, `Finsupp.domLCongr_trans`, `SkewMonoidAlgebra.toFinsupp_sub`, `Finsupp.add_apply`, `Finsupp.mapRange_smul`, `Multiset.mem_sup_map_support_iff`, `Finset.mem_finsupp_iff`, `MvPowerSeries.WithPiTopology.as_tsum`, `Finsupp.indicator_apply`, `MvPolynomial.degreeOf_le_iff`, `groupHomology.d₂₁_single_inv_self_ρ_sub_self_inv`, `Module.Basis.addSubgroupOfClosure_repr_apply`, `MvPolynomial.isUnit_iff_totalDegree_of_isReduced`, `MvPolynomial.monomialOneHom_apply`, `Finsupp.sumFinsuppLEquivProdFinsupp_symm_apply`, `Finsupp.support_add_eq`, `Module.Basis.repr_range`, `basis_toMatrix_basisFun_mul`, `Finsupp.prod_add_index'`, `MvPolynomial.leadingCoeff_esymmAlgHomMonomial`, `Nat.factorization_one_right`, `Finsupp.neLocus_zero_left`, `instFinitePresentationFinsupp`, `Finsupp.finite_range`, `Finsupp.lex_iff_of_unique`, `MvPolynomial.coeff_homogeneousComponent`, `MvPolynomial.support_expand_subset`, `Module.Basis.isScalarTower_finsupp`, `Submodule.LinearDisjoint.linearIndependent_right_of_flat`, `TensorProduct.finsuppLeft_symm_apply_single`, `Finsupp.linearEquivFunOnFinite_symm_apply`, `Finsupp.toDFinsupp_coe`, `MonomialOrder.coeff_prod_sum_degree`, `MonomialOrder.lex_lt_iff_of_unique`, `finsuppTensorFinsupp'_apply_apply`, `Finsupp.finset_sum_apply`, `SkewMonoidAlgebra.toFinsuppAddEquiv_apply`, `MvPolynomial.isUnit_iff`, `FreeAbelianGroup.equivFinsupp_symm_apply`, `Rep.coinvariantsTensorFreeLEquiv_apply`, `Finsupp.uncurry_apply`, `PiTensorProduct.ofFinsuppEquiv_symm_single_tprod`, `Finsupp.leftInverse_lcomapDomain_mapDomain`, `Module.Basis.reindexRange_repr_self`, `AddCommGroup.equiv_free_prod_directSum_zmod`, `MonomialOrder.degLex_le_iff`, `groupHomology.toCycles_comp_isoCycles₁_hom_apply`, `Ordinal.CNF.coeff_of_mem_CNF`, `Finsupp.single_eq_of_ne'`, `MvPowerSeries.monomial_zero_eq_C`, `MvPowerSeries.coeff_inv`, `PolynomialModule.single_apply`, `Finsupp.support_mul_subset_right`, `Finsupp.single_apply_left`, `Finsupp.linearCombination_linear_comp`, `groupHomology.mapCycles₂_comp_i`, `Module.Basis.repr_eq_iff`, `MvPolynomial.coeff_X_pow`, `Finsupp.le_iff`, `Finsupp.mem_submodule_iff`, `Finsupp.comp_liftAddHom`, `Module.Basis.sumQuot_repr_inl`, `Finsupp.sigmaFinsuppEquivPiFinsupp_apply`, `MvPolynomial.pow_idealOfVars_eq_span`, `Nat.ordProj_mul_ordCompl_eq_self`, `Nat.pairwise_coprime_pow_primeFactors_factorization`, `LaurentPolynomial.C_apply`, `groupHomology.boundariesOfIsBoundary₁_coe`, `Finsupp.coe_neLocus`, `KaehlerDifferential.kerTotal_mkQ_single_add`, `IsBaseChange.of_basis`, `Finsupp.mapRange.addMonoidHom_toZeroHom`, `MvPolynomial.coeff_zero_C`, `MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported`, `Algebra.Generators.cotangentSpaceBasis_repr_tmul`, `finsuppEquivDFinsupp_apply`, `AddMonoidAlgebra.modOf_apply_of_not_exists_add`, `Finsupp.comul_comp_lapply`, `Algebra.TensorProduct.equivFinsuppOfBasis_apply`, `Multiset.toFinsupp_inter`, `Finsupp.sumFinsuppLEquivProdFinsupp_symm_inl`, `MonomialOrder.degree_le_iff`, `Module.Basis.repr_linearCombination`, `groupHomology.eq_d₃₂_comp_inv_apply`, `StdSimplex.nonneg`, `LaurentPolynomial.T_apply`, `Finsupp.embSigma_eq_zero`, `Finsupp.ceilDiv_apply`, `Algebra.TensorProduct.equivFinsuppOfBasis_symm_apply`, `List.coe_toFinsupp`, `MvPolynomial.rTensor_apply_X_tmul`, `MvPowerSeries.coeff_homogeneousComponent`, `MonoidAlgebra.mapRangeAlgHom_apply`, `MvPolynomial.eval_eq'`, `PiLp.basisFun_repr`, `MvPolynomial.restrictSupport_univ`, `Finsupp.degree_apply`, `Finsupp.domCongr_apply`, `Algebra.Generators.H1Cotangent.δAux_toAlgHom`, `Finsupp.linearCombination_single_index`, `Finsupp.prod_unique`, `FreeAbelianGroup.toFinsupp_comp_toFreeAbelianGroup`, `groupHomology.single_one_fst_sub_single_one_fst_mem_boundaries₂`, `Finsupp.lift_apply`, `LinearIndependent.linearCombinationEquiv_apply_coe`, `Nat.factorization_choose_le_one`, `Module.Relations.Solution.range_π`, `TensorProduct.equivFinsuppOfBasisRight_apply_tmul_apply`, `Finsupp.subtypeDomain_finsupp_sum`, `Finsupp.Colex.wellFoundedLT_of_finite`, `Multiset.toFinsupp_apply`, `groupHomology.mapCycles₁_id_comp_apply`, `MonoidAlgebra.single_mul_apply_aux`, `Finsupp.sum_add_index'`, `Finsupp.toFreeAbelianGroup_single`, `MvPolynomial.vars_eq_support_biUnion_support`, `Equiv.finsuppUnique_apply`, `LinearIndependent.linearCombination_comp_repr`, `Finsupp.single_eq_update`, `Finsupp.optionElim_eq_elim'`, `MvPowerSeries.coeff_subst`, `Finsupp.apply_surjective`, `Finsupp.embDomain_eq_zero`, `sigmaFinsuppEquivDFinsupp_symm_apply`, `Polynomial.derivativeFinsupp_apply_apply`, `Nat.dvd_ordCompl_of_dvd_not_dvd`, `Algebra.SubmersivePresentation.sectionCotangent_eq_iff`, `AddEquiv.finsuppUnique_apply`, `Finsupp.finite_of_nat_weight_le`, `Module.Presentation.finsupp_var`, `Algebra.Presentation.differentials.surjective_hom₁`, `Nat.Prime.dvd_iff_one_le_factorization`, `MvPolynomial.eq_modMonomial_single_iff`, `MvPolynomial.rTensor_apply_tmul`, `Finsupp.codisjoint_supported_supported`, `Finsupp.supported_union`, `Module.Basis.linearCombination_dualBasis`, `Finsupp.prod_of_support_subset`, `groupHomology.π_comp_H2Iso_hom`, `FiniteDimensional.basisSingleton_repr_apply`, `MonomialOrder.degree_mul_of_isRegular_right`, `Finsupp.mapDomain_mono`, `MvPolynomial.coeff_monomial_mul`, `Finset.mapRange_finsuppAntidiag_eq`, `Finsupp.sum_sum_index'`, `Rep.indResAdjunction_counit_app_hom_hom`, `Finsupp.instFaithfulSMulOfNonempty`, `Finsupp.le_degree`, `Module.Basis.equivFunL_symm_apply_repr`, `MvPolynomial.degree_degLexDegree`, `PowerBasis.repr_gen_pow_isIntegral`, `Finsupp.card_Icc`, `groupHomology.pOpcycles_comp_opcyclesIso_hom_apply`, `Rep.coindToInd_apply`, `Finsupp.equivFunOnFinite_symm_apply_support`, `groupHomology.mapCycles₁_comp_i_apply`, `Finsupp.sum_unique`, `Polynomial.derivativeFinsupp_derivative`, `Subalgebra.LinearDisjoint.algebraMap_basisOfBasisRight_repr_apply`, `Finsupp.lsum_single`, `KaehlerDifferential.ker_map`, `MvPolynomial.dvd_monomial_iff_exists`, `Finsupp.ceilDiv_def`, `groupHomology.mapCycles₂_comp`, `LinearMap.CompatibleSMul.finsupp_dom`, `LinearMap.BilinForm.sum_repr_mul_repr_mul`, `Finsupp.linearEquivFunOnFinite_single`, `Finsupp.supported_iInter`, `Module.Basis.mulOpposite_repr_op`, `Module.Basis.smulTower'_repr_mk`, `Finsupp.single_finset_sum`, `Finsupp.rangeIcc_apply`, `MonomialOrder.degree_sum_le`, `instTwoUniqueSumsFinsupp`, `MonomialOrder.degree_mul_of_mul_leadingCoeff_ne_zero`, `instIsLocalizedModuleFinsuppLinearMap`, `Matrix.GeneralLinearGroup.toLin'_apply`, `MvPolynomial.mkDerivationₗ_monomial`, `Finsupp.counit_comp_lsingle`, `Finsupp.le_weight`, `TensorProduct.finsuppScalarRight_smul`, `AList.lookupFinsupp_eq_iff_of_ne_zero`, `Finset.mem_finsupp_iff_of_support_subset`, `MonomialOrder.degree_subsingleton`, `Finsupp.filter_add`, `groupHomology.coe_mapCycles₂`, `finsuppTensorFinsupp_single`, `Nat.factorization_zero`, `Finsupp.instSMulPosReflectLT`, `Cardinal.mk_finsupp_nat`, `Finsupp.card_uIcc`, `AList.empty_lookupFinsupp`, `groupHomology.comp_d₁₀_eq`, `MvPolynomial.finsupp_support_eq_support`, `Finsupp.card_Ioo`, `groupHomology.H1π_comp_map_apply`, `Nat.ceilRoot_def`, `Module.Basis.repr_reindex`, `Finsupp.comapDomain_surjective`, `Finsupp.DegLex.single_antitone`, `Finsupp.Lex.single_lt_iff`, `Finsupp.support_sum`, `Module.subsingletonEquiv_symm_apply`, `Nat.dvd_iff_div_factorization_eq_tsub`, `Finsupp.mk_mem_graph_iff`, `IsLocalizedModule.map_linearCombination`, `rank_finsupp_self'`, `Module.Basis.algebraMapCoeffs_repr_apply_toFun`, `Finsupp.filter_sub`, `LinearMap.toMatrix_mulVec_repr`, `Finsupp.sum_filter_index`, `AddMonoidAlgebra.apply_add_of_supDegree_le`, `Finsupp.sum_neg_index`, `Finsupp.single_eq_set_indicator`, `SkewMonoidAlgebra.ofFinsupp_injective`, `Finsupp.filter_eq_sum`, `Finsupp.snd_sumFinsuppAddEquivProdFinsupp`, `finsuppTensorFinsupp'_symm_single_eq_single_one_tmul`, `Matrix.toLin_apply_eq_zero_iff`, `Finsupp.erase_eq_sub_single`, `AddMonoidAlgebra.modOf_apply_of_exists_add`, `Finsupp.mem_toMultiset`, `linearDepOn_iff`, `AddMonoidAlgebra.coe_add`, `DFinsupp.toFinsupp_coe`, `groupHomology.toCycles_comp_isoCycles₁_hom_assoc`, `Module.Basis.algebraMapCoeffs_repr_apply_apply`, `Matrix.toLinearMapₛₗ₂_apply`, `Finsupp.lcomapDomain_apply`, `Finsupp.lhom_ext'_iff`, `LinearMap.BilinForm.dualBasis_repr_apply`, `MvPowerSeries.coeff_one`, `IsIsotypicOfType.linearEquiv_finsupp`, `Finsupp.support_subset_singleton`, `Finsupp.filter_eq_zero_iff`, `PolynomialModule.zero_apply`, `Finsupp.curry_single`, `linearIndepOn_iff_disjoint`, `Finsupp.mapRange.linearMap_apply`, `Module.Basis.sumQuot_repr_inl_of_mem`, `Finsupp.mapRange.linearEquiv_symm`, `Rep.freeLiftLEquiv_apply`, `Module.End.ringEquivEndFinsupp_apply_apply_apply`, `Submodule.set_smul_eq_map`, `MvPolynomial.coe_basisMonomials`, `Nat.exponent_eq_exponent_mul_factorization_of_prime_pow_eq_base_pow`, `Finsupp.lcongr_symm`, `Finsupp.sumFinsuppEquivProdFinsupp_symm_inr`, `TensorProduct.finsuppScalarRight_apply_tmul_apply`, `MonomialOrder.degree_mul_lt_iff_left_lt_of_ne_zero`, `Finsupp.coe_curryAddEquiv`, `MvPolynomial.mapRange_eq_map`, `Finset.mem_sup_support_iff`, `MvPolynomial.monomial_mem_pow_idealOfVars_iff`, `Finsupp.infinite_of_left`, `AddMonoidAlgebra.mul_single_zero_apply`, `Module.Basis.repr_symm_single`, `Representation.finsuppToCoinvariants_single_mk`, `groupHomology.H2π_comp_map_assoc`, `apply_eq_dotProduct_toMatrix₂_mulVec`, `MonomialOrder.degree_smul_le`, `TensorProduct.finsuppLeft_apply`, `MvPolynomial.irreducible_sumSMulX`, `factorization_zero`, `Finsupp.support_ceilDiv_subset`, `MvPolynomial.totalDegree_eq_zero_iff_eq_C`, `finsuppTensorFinsuppRid_symm_single_smul`, `MvPowerSeries.coeff_expand_smul`, `finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply`, `Finsupp.uncurry_single`, `MvPolynomial.weightedTotalDegree_eq_zero_iff`, `Finsupp.inf_apply`, `Nat.Partition.toFinsuppAntidiag_injective`, `Module.Basis.restrictScalars_repr_apply`, `Orthonormal.inner_finsupp_eq_sum_right`, `Representation.finsupp_single`, `Finsupp.span_eq_range_linearCombination`, `Module.Basis.equivFunL_apply`, `Nat.factorization_centralBinom_eq_zero_of_two_mul_lt`, `Finsupp.prod_eq_zero_iff`, `Finsupp.isCompl_range_lmapDomain_span`, `Finsupp.mapRange.addEquiv_symm`, `Squarefree.natFactorization_le_one`, `MvPowerSeries.eval₂_eq_tsum`, `Finsupp.instSMulPosMono`, `Algebra.Generators.cotangentRestrict_bijective_of_isCompl`, `MvPolynomial.combinatorial_nullstellensatz_exists_linearCombination`, `Module.Relations.map_single`, `Module.presentationFinsupp_R`, `MvPolynomial.rTensorAlgHom_toLinearMap`, `groupHomology.d₁₀ArrowIso_inv_right`, `Finsupp.mapDomain_zero`, `Finsupp.single_left_injective`, `MonoidAlgebra.mapRangeAddEquiv_apply`, `Rep.finsuppTensorRight_hom_hom`, `MvPolynomial.coeff_sumSMulX`, `Finsupp.single_mul`, `Finsupp.multinomial_eq_of_support_subset`, `Finsupp.coe_strictMono`, `MvPowerSeries.le_weightedOrder_subst`, `Finsupp.mapDomainEmbedding_apply`, `MvPowerSeries.trunc'_expand`, `Finsupp.linearCombinationOn_range`, `Nat.factorization_choose_of_lt_three_mul`, `Algebra.TensorProduct.basisAux_tmul`, `Finsupp.multinomial_update`, `MvPowerSeries.monomial_zero_eq_C_apply`, `MonomialOrder.degree_mul_le`, `Module.Basis.singleton_repr`, `KaehlerDifferential.derivationQuotKerTotal_apply`, `Finsupp.count_toMultiset`, `MonoidAlgebra.coe_add`, `Finsupp.neLocus_add_right`, `Finsupp.linearIndependent_single_of_ne_zero`, `MvPolynomial.mem_restrictDegree`, `MvPolynomial.support_coeff_finSuccEquiv`, `LinearMap.polyCharpolyAux_map_eq_charpoly`, `Finsupp.sum_add_index_of_disjoint`, `FreeAbelianGroup.toFinsupp_of`, `LinearMap.polyCharpolyAux_eval_eq_toMatrix_charpoly_coeff`, `MvPolynomial.supDegree_esymm`, `Nat.factorization_lt`, `LinearMap.toMatrix_transpose_apply`, `Pi.basis_repr`, `Finsupp.cons_tail`, `Finsupp.erase_neg`, `Finsupp.mapRange_injective`, `MvPolynomial.eval_eq`, `MonoidAlgebra.mul_apply_mul_eq_mul_of_uniqueMul`, `groupHomology.d₁₀_comp_coinvariantsMk`, `MonomialOrder.sPolynomial_def`, `groupHomology.d₂₁_comp_d₁₀_apply`, `Nat.not_dvd_ordCompl`, `MvPolynomial.restrictSupport_zero`, `groupHomology.mapCycles₂_comp_apply`, `Module.Relations.Quotient.linearMap_ext_iff`, `Module.Presentation.ofExact_relation`, `Nat.factorization_lcm`, `LinearIndependent.span_repr_eq`, `Rep.coindFunctorIso_inv_app_hom_hom_apply_coe`, `sigmaFinsuppEquivDFinsupp_smul`, `MonomialOrder.le_add_right`, `MvPolynomial.as_sum`, `MonomialOrder.degree_mul_of_left_mem_nonZeroDivisors`, `Finsupp.cons_right_injective`, `Algebra.Presentation.differentials.comm₂₃'`, `Finsupp.equivMapDomain_trans'`, `InnerProductSpace.gramSchmidt_triangular`, `MvPolynomial.monomial_add_single`, `QuadraticAlgebra.basis_repr_apply`, `Finsupp.embSigma_injective`, `Finsupp.instPosSMulStrictMono`, `MonomialOrder.degree_pow_le`, `Module.Basis.toDual_eq_repr`, `Finsupp.prod_hom_add_index`, `Finsupp.smul_single'`, `Finsupp.weight_single_index`, `Finsupp.single_le_single`, `Finsupp.domCongr_symm`, `Module.Basis.sum_repr_mul_repr`, `Finsupp.addCommute_of_disjoint`, `Finsupp.linearCombination_apply`, `Finsupp.prod_filter_index`, `Nat.factorization_ceilRoot`, `Subalgebra.LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent`, `Finsupp.update_eq_single_add_erase`, `NumberField.integralBasis_repr_apply`, `MvPolynomial.eval₂_eq'`, `groupHomology.H2π_eq_iff`, `Submodule.mulRightMap_eq_mulMap_comp`, `Finsupp.wellFoundedLT'`, `Finsupp.fst_sumFinsuppEquivProdFinsupp`, `Module.Basis.linearMap_repr_apply`, `Finsupp.isPWO`, `groupHomology.H1AddEquivOfIsTrivial_single`, `Finsupp.degree_preimage_add`, `Finsupp.split_embSigma_of_ne`, `Relation.cutExpand_le_invImage_lex`, `MultilinearMap.freeFinsuppEquiv_def`, `MonomialOrder.degree_C`, `Finsupp.single_mono`, `Finsupp.liftAddHom_apply`, `MvPolynomial.coeff_monomial_mul'`, `groupHomology.range_d₁₀_eq_coinvariantsKer`, `Finsupp.smul_apply`, `MonomialOrder.toSyn_monotone`, `ArithmeticFunction.sigma_eq_prod_primeFactors_sum_range_factorization_pow_mul`, `MvPowerSeries.coeff_trunc'`, `Finsupp.Colex.le_iff_of_unique`, `Finsupp.Lex.le_iff_of_unique`, `Finsupp.coe_update`, `MvPolynomial.coeff_zero_X`, `MvPowerSeries.coeff_zero_mul_X`, `groupHomology.isoCycles₂_hom_comp_i_apply`, `Finsupp.linearCombination_embDomain`, `MvPowerSeries.coeff_inv_aux`, `Finsupp.erase_zero`, `Finsupp.DegLex.lt_iff`, `MonomialOrder.degLex_single_le_iff`, `MvPolynomial.leadingCoeff_toLex_C`, `MvPolynomial.support_mul_X`, `Finsupp.comapDomain_apply`, `SkewMonoidAlgebra.toFinsuppAddEquiv_symm_apply`, `MvPowerSeries.coeff_weightedHomogeneousComponent`, `Finsupp.support_eq_singleton`, `Finsupp.single_nonpos`, `MvPowerSeries.order_le`, `Finsupp.mul_apply`, `Representation.ofMulActionSelfAsModuleEquiv_apply`, `Finsupp.mapDomain_apply`, `KaehlerDifferential.kerTotal_map`, `MvPowerSeries.lexOrder_zero`, `QuadraticMap.map_finsuppSum'`, `groupHomology.eq_d₂₁_comp_inv_assoc`, `Finsupp.degLex_def`, `Rep.ofMulActionSubsingletonIsoTrivial_inv_hom`, `Finsupp.univ_sum_single_apply`, `SkewMonoidAlgebra.toFinsupp_injective`, `PiTensorProduct.ofFinsuppEquiv_apply`, `Finsupp.equivFunOnFinite_symm_coe`, `Finsupp.mapRange.addMonoidHom_comp`, `MvPolynomial.support_esymm'`, `TensorProduct.finsuppScalarRight_symm_apply_single`, `List.toFinsupp_concat_eq_toFinsupp_add_single`, `Finsupp.lt_def`, `Equiv.finsuppUnique_symm_apply_apply`, `groupHomology.cyclesMap_comp_isoCycles₂_hom_assoc`, `Module.Basis.mem_span_image`, `Finsupp.mapRange_add'`, `LinearMap.CompatibleSMul.finsupp_cod`, `Finsupp.sumFinsuppAddEquivProdFinsupp_apply`, `Finset.mapRange_finsuppAntidiag_subset`, `NumberField.mixedEmbedding.stdBasis_apply_isComplex_fst`, `MvPolynomial.mem_support_coeff_optionEquivLeft`, `Finsupp.lex_lt_iff_of_unique`, `Module.Basis.localizationLocalization_repr_algebraMap`, `groupHomology.inhomogeneousChains.d_single`, `Module.Basis.dualBasis_apply`, `MvPowerSeries.coeff_trunc`, `apply_eq_star_dotProduct_toMatrix₂_mulVec`, `MvPolynomial.mkDerivation_monomial`, `Complex.coe_basisOneI_repr`, `Finsupp.linearCombination_single`, `Module.Presentation.CokernelData.π_lift`, `Finsupp.embDomain_apply_self`, `Finsupp.equivMapDomain_zero`, `Finsupp.ofSupportFinite_fin_two_eq`, `MvPolynomial.schwartz_zippel_sup_sum`, `PolynomialModule.smul_apply`, `Module.Basis.reindexFinsetRange_repr_self`, `AddMonoidAlgebra.mul_apply_left`, `Finsupp.orderEmbeddingToFun_apply`, `Finsupp.single_tsub`, `SkewMonoidAlgebra.toFinsupp_neg`, `Orthonormal.inner_right_finsupp`, `LinearMap.toMatrix_transpose_apply'`, `Finsupp.piecewise_apply`, `MvPolynomial.mem_restrictSupport_iff`, `Module.Basis.repr_symm_single_one`, `Rep.diagonalOneIsoLeftRegular_inv_hom`, `groupHomology.isBoundary₂_iff`, `HahnSeries.coeff_ofFinsupp`, `Finsupp.coe_onFinset`, `MvPolynomial.monic_esymm`, `Finsupp.sum_nsmul`, `Finsupp.toMultiset_add`, `Nat.primeFactorsList_count_eq`, `Multiset.toFinsupp_singleton`, `Finsupp.coe_basis`, `MvPolynomial.eq_C_of_isEmpty`, `Finsupp.mapRange.linearEquiv_toLinearMap`, `MvPolynomial.coeff_one`, `LinearMap.toMatrix_smulRight`, `Finsupp.single_apply_eq_zero`, `Module.Relations.solutionFinsupp_var`, `Finsupp.subtypeDomain_apply`, `Prime.dvd_finsuppProd_iff`, `Multiset.toFinsupp_symm_apply`, `MvPolynomial.monomial_zero'`, `Nat.setOf_pow_dvd_eq_Icc_factorization`, `FreeAbelianGroup.equivFinsupp_apply`, `MvPowerSeries.coeff_truncFun'`, `Finsupp.sumFinsuppEquivProdFinsupp_symm_apply`, `Finsupp.counit_single`, `SkewMonoidAlgebra.toFinsupp_zero`, `NumberField.mixedEmbedding.stdBasis_repr_eq_matrixToStdBasis_mul`, `RootPairing.Base.toCoweightBasis_repr_coroot`, `Finsupp.single_swap`, `AdjoinRoot.powerBasisAux'_repr_symm_apply`, `MvPowerSeries.coeff_prod`, `groupHomology.mapCycles₂_id_comp_assoc`, `MvPowerSeries.exists_coeff_ne_zero_and_order`, `Finsupp.coe_finset_sum`, `groupHomology.π_comp_H1Iso_hom_apply`, `Nat.factorization_choose'`, `Finsupp.restrictDom_comp_subtype`, `AddMonoidAlgebra.coeff_smul`, `Finsupp.lsum_apply`, `groupHomology.single_isCycle₂_iff`, `Finsupp.filter_single_of_neg`, `Basis.multilinearMap_apply_apply`, `Finsupp.neLocus_zero_right`, `Nat.factorization_choose_le_log`, `MvPolynomial.homogeneousComponent_apply`, `Nat.factorization_eq_zero_of_not_prime`, `Rep.standardComplex.d_of`, `Module.Basis.coe_finTwoProd_repr`, `Finsupp.linearCombination_unique`, `groupHomology.toCycles_comp_isoCycles₂_hom`, `SkewMonoidAlgebra.ofFinsupp_neg`, `Finsupp.coe_lsum`, `Finsupp.isCentralScalar`, `Finsupp.neLocus_sub_left`, `Finsupp.sum_uncurry_index'`, `groupHomology.cyclesMap_comp_isoCycles₂_hom_apply`, `Finsupp.linearCombination_mapDomain`, `Span.finsupp_linearCombination_repr`, `groupHomology.mapCycles₁_id_comp`, `MvPolynomial.coeff_mul_X'`, `PolynomialModule.smul_single_apply`, `Finset.finsuppAntidiag_mono`, `MvPolynomial.prod_X_pow_eq_monomial`, `Finsupp.lapply_comp_lsingle_same`, `Finsupp.instIsCocomm`, `MvPolynomial.constantCoeff_monomial`, `MvPolynomial.coeff_mul_X`, `Finsupp.multinomial_eq`, `Finsupp.mapRange_surjective`, `Finsupp.instIsCancelAdd`, `MonoidAlgebra.mapRangeRingEquiv_apply`, `MvPolynomial.supDegree_toLex_C`, `Cardinal.mk_finsupp_of_fintype`, `Module.Presentation.finsupp_relation`, `IsAdjoinRootMonic.coeff_apply_lt`, `Nat.Icc_factorization_eq_pow_dvd`, `Nat.factorization_le_iff_dvd`, `Finsupp.neLocus_self_sub_left`, `List.mem_foldr_sup_support_iff`, `Finsupp.mem_rangeIcc_apply_iff`, `Nat.ordCompl_pos`, `DirectSum.IsInternal.collectedBasis_repr_of_mem_ne`, `Module.Basis.toMatrix_apply`, `KaehlerDifferential.mvPolynomialBasis_repr_apply`, `LinearMap.exists_finsupp_nat_of_prod_injective`, `MvPolynomial.optionEquivLeft_coeff_some_coeff_none`, `MvPowerSeries.coeff_zero_one`, `Finsupp.sigmaFinsuppLEquivPiFinsupp_apply`, `groupHomology.eq_d₁₀_comp_inv`, `Nat.ordCompl_mul`, `Rep.diagonalSuccIsoTensorTrivial_hom_hom_single`, `Finsupp.sum_curry_index`, `finsuppTensorFinsuppRid_single_tmul_single`, `LinearIndependent.linearCombinationEquiv_symm_apply`, `Nat.ordProj_le`, `Module.DualBases.basis_repr_apply`, `LieAlgebra.LoopAlgebra.toFinsupp_single_tmul`, `Algebra.toMatrix_lmul'`, `AddMonoidAlgebra.single_mul_apply`, `groupHomology.isoShortComplexH1_inv`, `Module.Relations.Solution.isPresentation_iff`, `Nat.factorization_le_factorization_choose_add`, `Module.DualBases.dual_lc`, `MvPolynomial.exists_mem_support_not_dvd_of_forall_totalDegree_le`, `Polynomial.derivativeFinsupp_map`, `groupHomology.eq_d₁₀_comp_inv_assoc`, `Finsupp.disjoint_supported_supported`, `Finsupp.llift_symm_apply`, `Finsupp.Colex.lt_iff`, `TensorProduct.finsuppScalarLeft_apply_tmul_apply`, `AddMonoidAlgebra.modOf_apply_self_add`, `Finsupp.apply_single'`, `groupHomology.chainsMap_f_1_comp_chainsIso₁_assoc`, `Finsupp.equivMapDomain_symm_apply`, `SkewMonoidAlgebra.ofFinsupp_add`, `MonoidAlgebra.smul_apply`, `Finsupp.prod_pow`, `Finsupp.sum_antidiagonal_swap`, `groupHomology.isoCycles₁_hom_comp_i_apply`, `Finsupp.mk_mem_graph`, `Finsupp.coe_add`, `Finsupp.nsmul_apply`, `Nat.card_divisors`, `Module.Basis.symmetricAlgebra_repr_apply`, `Finsupp.comapSMul_def`, `Finsupp.supportedEquivFinsupp_symm_apply_coe_support_val`, `ZLattice.exists_forall_abs_repr_le_norm`, `groupHomology.lsingle_comp_chainsMap_f`, `groupHomology.coinvariantsMk_comp_opcyclesIso₀_inv_apply`, `Nat.Prime.factorization_self`, `MvPowerSeries.coeff_add_mul_monomial`, `AddMonoidAlgebra.single_mul_apply_of_not_exists_add`, `MonomialOrder.degree_one`, `Finsupp.card_pi`, `Matrix.toLin_apply`, `AddMonoidAlgebra.single_mem_grade`, `MvPolynomial.totalDegree_eq_zero_iff`, `Finsupp.mapDomain_finset_sum`, `MvPowerSeries.monomial_pow`, `MultilinearMap.freeFinsuppEquiv_apply`, `AddMonoidAlgebra.apply_eq_zero_of_not_le_supDegree`, `Finsupp.filter_apply`, `Finsupp.linearCombination_range`, `Finsupp.mapRange_smul'`, `Nat.ordProj_dvd_ordProj_of_dvd`, `Finsupp.coe_smul`, `MvPolynomial.restrictSupport_nsmul`, `groupHomology.d₃₂_single_one_fst`, `MvPolynomial.mem_support_finSuccEquiv`, `Submodule.mulRightMap_apply`, `Finsupp.comapSMul_apply`, `Finsupp.coe_orderIsoMultiset_symm`, `finsuppLEquivDirectSum_single`, `Finsupp.some_single_none`, `groupHomology.d₂₁_comp_d₁₀`, `Orthonormal.inner_finsupp_eq_sum_left`, `Sylow.card_eq_multiplicity`, `Finsupp.comul_single`, `MvPolynomial.monomial_mem_restrictSupport`, `SkewMonoidAlgebra.toFinsupp_add`, `groupHomology.d₂₁_single_self_inv_ρ_sub_inv_self`, `Finsupp.subtypeDomain_eq_zero_iff'`, `LinearIndependent.finsuppLinearCombination_injective`, `Representation.ker_leftRegular_norm_eq`, `Finsupp.lapply_apply`, `MvPowerSeries.coeff_zero_X_mul`, `groupHomology.chainsMap_f_3_comp_chainsIso₃_assoc`, `groupHomology.single_ρ_self_add_single_inv_mem_boundaries₁`, `Finsupp.support_single_add_single_subset`, `groupHomology.H1ToTensorOfIsTrivial_H1π_single`, `Finsupp.mapRange.linearMap_comp`, `Finsupp.fst_sumFinsuppAddEquivProdFinsupp`, `MvPolynomial.esymmAlgHom_zero`, `Nat.factorization_centralBinom_of_two_mul_self_lt_three_mul`, `Rep.ofMulActionSubsingletonIsoTrivial_hom_hom`, `Finsupp.zero_apply`, `Finsupp.DegLex.single_le_iff`, `MvPolynomial.degreeOf_eq_sup`, `Module.length_finsupp`, `Finsupp.support_floorDiv_subset`, `Finsupp.ofSupportFinite_coe`, `Finsupp.linearCombination_restrict`, `Algebra.Presentation.differentials.comm₁₂`, `Module.Basis.sumQuot_repr_inr_of_mem`, `Finsupp.wellQuasiOrderedLE`, `MonomialOrder.sPolynomial_monomial_mul`, `Finsupp.coe_basisSingleOne`, `Finsupp.coe_lmapDomain`, `Finsupp.mapRange_sub`, `Finsupp.indicator_eq_sum_attach_single`, `List.toFinsupp_apply_le`, `Rep.linearizationTrivialIso_inv_hom`, `Finsupp.lapply_comp_lsingle_of_ne`, `Nat.ordCompl_self_pow_mul`, `groupHomology.cyclesOfIsCycle₁_coe`, `Module.Basis.repr_injective`, `Finsupp.support_single_add`, `MonoidAlgebra.mul_single_apply_of_not_exists_mul`, `MvPolynomial.homogeneousComponent_zero`, `LinearIndependent.repr_range`, `Finsupp.prod_neg_index`, `MvPolynomial.monomial_left_injective`, `Finsupp.addHom_ext'_iff`, `MvPolynomial.monomial_sum_index`, `groupHomology.inhomogeneousChains.ext_iff`, `Finsupp.linearCombination_comp`, `MonomialOrder.degree_eq_zero_iff_totalDegree_eq_zero`, `exteriorPower.presentation_relation`, `LinearMap.polyCharpolyAux_map_aeval`, `Pi.counit_coe_finsupp`, `MvPolynomial.image_support_finSuccEquiv`, `MvPolynomial.support_nonempty`, `AddMonoidAlgebra.mul_single_apply_aux`, `groupHomology.d₂₁_apply_mem_cycles₁`, `MvPolynomial.support_expand`, `NumberField.inverse_basisMatrix_mulVec_eq_repr`, `Finsupp.range_linearCombination`, `Finsupp.toFreeAbelianGroup_toFinsupp`, `MonomialOrder.degree_eq_zero_iff`, `Finsupp.sum_update_add`, `MonomialOrder.degree_mem_support`, `Finsupp.Lex.addRightStrictMono`, `Nat.factorization_one`, `Finsupp.supported_empty`, `Module.Relations.ker_toQuotient`, `groupHomology.cyclesMap_comp_isoCycles₁_hom_apply`, `Finsupp.bilinearCombination_apply`, `groupHomology.toCycles_comp_isoCycles₂_hom_apply`, `Finsupp.coe_nsmul`, `Finsupp.embSigma_apply_of_ne`, `Finsupp.antidiagonal_zero`, `Finsupp.apply_linearCombination`, `Module.Relations.Solution.IsPresentation.surjective_π`, `Module.finite_finsupp_iff`, `Finsupp.erase_add_single`, `Finsupp.mapRange_eq_zero`, `MonoidAlgebra.mul_single_one_apply`, `MvPolynomial.support_monomial_subset`, `MvPolynomial.monomial_mul`, `MonomialOrder.toSyn_eq_zero_iff`, `Finsupp.toDFinsupp_smul`, `KaehlerDifferential.kerTotal_mkQ_single_mul`, `LaurentPolynomial.ext_iff`, `Finsupp.linearIndependent_single_iff`, `PointedCone.mem_span_set`, `MultilinearMap.freeFinsuppEquiv_single`, `MvPowerSeries.weightedOrder_eq_nat`, `MvPowerSeries.totalDegree_trunc'`, `groupHomology.eq_d₃₂_comp_inv_assoc`, `Module.Basis.end_repr_symm_apply`, `MvPowerSeries.expand_monomial`, `FirstOrder.Ring.MvPolynomialSupportLEEquiv_symm_apply_coeff`, `InnerProductSpace.toMatrix_rankOne`, `MvPolynomial.support_X_pow`, `MvPolynomial.rTensor_symm_apply_single`, `finTwoArrowEquiv'_symm_apply`, `Finsupp.update_eq_sub_add_single`, `Finsupp.optionElim_zero`, `AddMonoidAlgebra.mul_apply_add_eq_mul_of_uniqueAdd`, `Representation.free_single_single`, `Finsupp.toDFinsupp_neg`, `MvPolynomial.pderiv_monomial`, `Finsupp.mapRange_zero`, `Finsupp.lcongr_symm_single`, `Module.Basis.apply_eq_iff`, `Finsupp.sum_uncurry_index`, `Module.Flat.iff_forall_exists_factorization`, `Finsupp.coe_sym2Mul`, `sigmaFinsuppLequivDFinsupp_symm_apply`, `sigmaFinsuppEquivDFinsupp_single`, `Nat.prod_pow_primeFactors_factorization`, `Algebra.Generators.toComp_toAlgHom_monomial`, `Module.Relations.Solution.π_comp_map`, `Finsupp.equivMapDomain_apply`, `Finsupp.domLCongr_symm`, `Multiset.toFinsupp_zero`, `Rep.finsuppTensorRight_inv_hom`, `MvPolynomial.monomial_mem_homogeneousSubmodule_pow_degree`, `Finsupp.single_add_erase`, `Multiset.toFinsupp_toMultiset`, `setBasisOfTopLeSpanOfCardEqFinrank_repr_apply`, `LinearMap.polyCharpolyAux_coeff_eval`, `Cardinal.mk_finsupp_lift_of_fintype`, `MonomialOrder.degree_prod_le`, `Finsupp.disjoint_lsingle_lsingle`, `Finsupp.coe_eq_zero`, `Finsupp.subset_support_tsub`, `MvPolynomial.dvd_monomial_mul_iff_exists`, `Finsupp.linearCombination_comp_addSingleEquiv`, `Finsupp.DegLex.isStrictOrder`, `Finsupp.rangeSingleton_apply`, `Matrix.toLinAlgEquiv_apply`, `Module.Basis.coe_ofRepr`, `Module.equiv_free_prod_directSum`, `AddMonoidAlgebra.opRingEquiv_apply`, `Finsupp.codisjoint_supported_supported_iff`, `MonomialOrder.div_set`, `MvPolynomial.support_optionEquivLeft`, `Finsupp.single_add`, `TensorProduct.equivFinsuppOfBasisRight_apply`, `Submodule.mulLeftMap_eq_mulMap_comp`, `Finset.sum_single_ite`, `MvPowerSeries.WithPiTopology.hasSum_of_monomials_self`, `groupHomology.mapCycles₂_hom`, `Finsupp.toDFinsupp_sub`, `MonomialOrder.degree_zero`, `groupHomology.isoCycles₂_inv_comp_iCycles_apply`, `Ordinal.CNF.coeff_zero_right`, `groupHomology.isoCycles₂_inv_comp_iCycles_assoc`, `Finsupp.support_smul`, `Finsupp.le_iff'`, `KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination`, `Finsupp.instPosSMulMono`, `Finsupp.embDomain_add`, `Nat.ordProj_self_pow`, `Finsupp.univ_sum_single`, `Finsupp.mapRange.linearMap_id`, `exists_ordCompl_eq_one_iff_isPrimePow`, `Finsupp.degree_preimage_nsmul`, `Nat.factorization_le_factorization_mul_right`, `PowerSeries.coeff_prod`, `Finsupp.lcongr_single`, `Module.Flat.exists_factorization_of_apply_eq_zero_of_free`, `MvPowerSeries.exists_coeff_ne_zero_and_weightedOrder`, `Nat.prod_factorization_eq_prod_primeFactors`, `Nat.factorization_eq_zero_iff_remainder`, `Finsupp.Lex.addLeftStrictMono`, `List.toFinsupp_apply_lt`, `Matrix.toLinearMap₂_apply`, `Finsupp.linearEquivFunOnFinite_apply`, `Nat.Prime.pow_dvd_iff_dvd_ordProj`, `ZLattice.abs_repr_lt_of_norm_lt`, `groupHomology.cyclesMk₂_eq`, `groupHomology.chainsMap_f_1_comp_chainsIso₁`, `Rep.coindVEquiv_apply_hom`, `Finsupp.optionElim_apply_some`, `Finsupp.embDomain_zero`, `Finsupp.prod_option_index`, `LieAlgebra.LoopAlgebra.residuePairing_apply_apply`, `KaehlerDifferential.kerTotal_mkQ_single_smul`, `MvPolynomial.rTensor_apply_monomial_tmul`, `Algebra.Generators.repr_CotangentSpaceMap`, `Module.Basis.dualBasis_repr`, `groupHomology.H1π_eq_zero_iff`, `groupHomology.isoCycles₁_inv_comp_iCycles_assoc`, `Finsupp.sumFinsuppLEquivProdFinsupp_symm_inr`, `MonomialOrder.degLex_lt_iff`, `MvPolynomial.coeff_X'`, `groupHomology.π_comp_H1Iso_hom_assoc`, `Pi.comul_coe_finsupp`, `Finsupp.sum_hom_add_index`, `groupHomology.chainsMap_f_2_comp_chainsIso₂`, `groupHomology.d₂₁_single_one_fst`, `Finsupp.supported_mono`, `MvPowerSeries.coeff_truncFun`, `MonomialOrder.coeff_pow_nsmul_degree`, `groupHomology.H2π_comp_map`, `NumberField.mixedEmbedding.stdBasis_apply_isReal`, `Finsupp.coe_rangeIcc`, `Finsupp.add_closure_setOf_eq_single`, `Finsupp.mapRange.addEquiv_toAddMonoidHom`, `MvPolynomial.constantCoeff_eq`, `HahnSeries.coeff_toMvPowerSeries_symm`, `MonoidAlgebra.uniqueRingEquiv_symm_apply`, `Module.Basis.linearCombination_repr`, `union_support_maximal_linearIndependent_eq_range_basis`, `Module.FinitePresentation.out`, `Nat.factorization_eq_primeFactorsList_multiset`, `Finsupp.mapRange.equiv_apply`, `PolynomialModule.lsingle_apply`, `Finsupp.lex_eq_invImage_dfinsupp_lex`, `MvPowerSeries.weightedOrder_le`, `Nat.factorization_floorRoot`, `Module.Basis.linearCombination_coord`, `Finsupp.sup_apply`, `Representation.FiniteCyclicGroup.coinvariantsKer_leftRegular_eq_ker`, `Finsupp.coe_floorDiv`, `Finsupp.cons_zero`, `Finsupp.addLeftReflectLE`, `Module.Basis.tensorAlgebra_repr_apply`, `Nat.floorRoot_def`, `Module.projective_def'`, `groupHomology.H1π_comp_map_assoc`, `MonomialOrder.degree_pow`, `MvPowerSeries.coeff_zero_C`, `Representation.coinvariantsTprodLeftRegularLEquiv_symm_apply`, `Module.Basis.equivFun_apply`, `Finsupp.add_sum_erase'`, `Finsupp.sum_option_index_smul`, `Finset.finsuppAntidiag_empty_zero`, `TensorProduct.finsuppScalarLeft_apply_tmul`, `MvPowerSeries.coeff_monomial`, `groupHomology.instEpiModuleCatH1π`, `MvPowerSeries.coeff_C`, `Finsupp.mapRange.zeroHom_comp`, `Module.Relations.directSum_relation`, `Module.Basis.mulOpposite_repr_eq`, `Module.Basis.coe_repr_symm`, `Finsupp.coe_equivFunOnFinite_symm`, `Module.Basis.smulTower'_repr`, `Module.Relations.toQuotient_map_apply`, `Rep.finsuppTensorLeft_inv_hom`, `LinearMap.snd_prodOfFinsuppNat`, `AddMonoidAlgebra.uniqueRingEquiv_symm_apply`, `Finsupp.toFinset_toMultiset`, `Finsupp.apply_single`, `Finsupp.degree_single`, `MonoidAlgebra.mul_apply`, `Module.Presentation.tensor_relation`, `Finsupp.LinearEquiv.finsuppUnique_apply`, `linearIndependent_iff`, `Finsupp.applyAddHom_apply`, `Finsupp.mapDomain_equiv_apply`, `MvPolynomial.coeff_rTensorAlgHom_monomial_tmul`, `Finsupp.linearCombination_fin_zero`, `MvPolynomial.support_sum_monomial_coeff`, `Module.Relations.Solution.π_relation`, `MvPolynomial.esymmAlgHomMonomial_add`, `Finsupp.wellFoundedLT`, `exteriorPower.basis_repr_apply`, `Finsupp.linearEquivFunOnFinite_symm_single`, `Module.Basis.toMatrix_update`, `Finsupp.range_single_subset`, `PiLp.basis_toMatrix_basisFun_mul`, `Finsupp.single_multiset_sum`, `groupHomology.single_one_snd_sub_single_one_snd_mem_boundaries₂`, `MvPolynomial.weightedDecomposition.decompose'_eq`, `Finsupp.subtypeDomain_eq_iff_forall`, `Polynomial.toFinsupp_apply`, `Finsupp.linearCombination_equivMapDomain`, `MvPowerSeries.lexOrder_eq_top_iff_eq_zero`, `Finsupp.mapRange.equiv_trans`, `Finsupp.neg_apply`, `Finsupp.le_weight_of_ne_zero`, `Finsupp.mapRange.linearEquiv_apply`, `Finset.finsuppAntidiag_empty`, `Finsupp.instSMulPosStrictMono`, `groupHomology.instEpiModuleCatH2π`, `Finsupp.Lex.single_antitone`, `Module.Basis.baseChange_repr_tmul`, `SkewMonoidAlgebra.coeff_ofFinsupp`, `List.support_sum_subset`, `Finsupp.lex_le_iff_of_unique`, `ZSpan.repr_fract_apply`, `finsuppLEquivDirectSum_apply`, `Multiset.toFinsupp_eq_iff`, `Rep.leftRegularTensorTrivialIsoFree_inv_hom`, `Finsupp.instIsAddTorsionFree`, `Algebra.TensorProduct.basis_repr_symm_apply`, `LinearMap.polyCharpoly_map_eq_charpoly`, `MvPolynomial.coeffsIn_eq_span_monomial`, `Finsupp.filter_pos_add_filter_neg`, `Submodule.mulLeftMap_apply_single`, `Finsupp.single_mem_span_single`, `KaehlerDifferential.quotKerTotalEquiv_symm_apply`, `Finsupp.mapDomain.addMonoidHom_apply`, `finsuppTensorFinsuppLid_apply_apply`, `LaurentPolynomial.invert_apply`, `LinearIndependent.repr_ker`, `groupHomology.H1π_comp_map`, `groupHomology.chainsMap_f_hom`, `groupHomology.d₃₂_apply_mem_cycles₂`, `Finsupp.mapRange.linearMap_toAddMonoidHom`, `Finsupp.single_apply_mem`, `QuaternionAlgebra.coe_basisOneIJK_repr`, `MvPolynomial.homogeneousSubmodule_eq_finsupp_supported`, `Ideal.range_finsuppTotal`, `Nat.factorization_div`, `Finsupp.Lex.isOrderedCancelAddMonoid`, `MvPolynomial.support_map_subset`, `Nat.factorization_choose_eq_zero_of_lt`, `Finsupp.sum_smul_index_semilinearMap'`, `groupHomology.boundariesOfIsBoundary₂_coe`, `centralBinom_factorization_small`, `Finsupp.Lex.wellFounded`, `Finsupp.subtypeDomain_eq_zero_iff`, `groupHomology.cyclesMk₁_eq`, `finsuppLequivDFinsupp_apply_apply`, `Nat.prod_pow_factorization_choose`, `Finsupp.support_add`, `Finsupp.graph_zero`, `Finsupp.liftAddHom_singleAddHom`, `MvPowerSeries.coeff_invOfUnit`, `Finsupp.support_inf_union_support_sup`, `MvPolynomial.esymm_eq_sum_monomial`, `AddEquiv.finsuppUnique_symm_apply_support_val`, `Finsupp.logHeight_eq_log_mulHeight`, `groupHomology.mapCycles₂_comp_i_assoc`, `Finsupp.toMultiset_sum`, `Finsupp.uncurry_apply_pair`, `Nat.factorization_prime_le_iff_dvd`, `Finsupp.domLCongr_apply`, `Rep.linearization_δ_hom`, `Finsupp.coe_lt_coe`, `Nat.sum_divisors`, `Finsupp.prod_ite_eq`, `Finsupp.range_single_one`, `AddMonoidAlgebra.mapRangeRingEquiv_apply`, `Finsupp.extendDomain_toFun`, `MvPolynomial.restrictSupport_add`, `Finsupp.curryLinearEquiv_apply`, `QuadraticMap.apply_linearCombination'`, `Finsupp.card_Iic`, `Nat.factorization_pow_self`, `groupHomology.mapCycles₂_id_comp_apply`, `Finsupp.optionElim_apply_eq_elim`, `finsuppTensorFinsupp_symm_single`, `Finsupp.single_le_iff`, `Finsupp.linearCombination_linearCombination`, `MvPowerSeries.WithPiTopology.tendsto_trunc'_atTop`, `Module.Relations.Solution.IsPresentation.desc_comp_π`, `Finsupp.mapRange.zeroHom_apply`, `Finsupp.Colex.addLeftMono`, `Finsupp.equivCongrLeft_symm`, `Finsupp.split_apply`, `Finsupp.lift_symm_apply`, `MvPowerSeries.coeff_zero_X`, `groupHomology.H2π_comp_map_apply`, `NumberField.mixedEmbedding.latticeBasis_repr_apply`, `Finsupp.card_Iio`, `Finsupp.smul_eq`, `Module.Basis.ext_elem_iff`, `Finsupp.default_eq_zero`, `Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply`, `Finsupp.distribMulActionHom_ext'_iff`, `KaehlerDifferential.mvPolynomialBasis_repr_D`, `MonomialOrder.sPolynomial_monomial_mul'`, `HahnSeries.coeff_toMvPowerSeries`, `Finsupp.restrictSupportEquiv_symm_single`, `MonoidAlgebra.mapDomainRingEquiv_apply`, `Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply`, `Finsupp.single_add_single_eq_single_add_single`, `Nat.factorization_eq_card_pow_dvd`, `Finsupp.prod_fintype`, `MvPolynomial.support_divMonomial`, `finsuppTensorFinsuppRid_apply_apply`, `Module.Basis.repr_sum_self`, `RootPairing.Base.toWeightBasis_repr_root`, `finsuppEquivDFinsupp_symm_apply`, `Rep.finsuppTensorLeft_hom_hom`, `Finsupp.linearCombination_option`, `Polynomial.derivativeFinsupp_one`, `Algebra.leftMulMatrix_mulVec_repr`, `MvPowerSeries.order_monomial`, `factorization_eq_count`, `Finsupp.linearCombination_eq_fintype_linearCombination`, `Nat.factorization_factorial_mul_succ`, `Finsupp.mapRange_add`, `KaehlerDifferential.ker_map_of_surjective`, `Finsupp.basisSingleOne_repr`, `Finsupp.supportedEquivFinsupp_symm_apply_coe`, `groupHomology.inhomogeneousChains.d_comp_d`, `MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_weight`, `Module.Basis.smulTower_repr_mk`, `Module.Basis.repr_support_subset_of_mem_span`, `MvPolynomial.support_zero`, `Algebra.Generators.cotangentRestrict_mk`, `Nat.factorization_ordCompl`, `Finsupp.liftAddHom_apply_single`, `Finsupp.supportedEquivFinsupp_apply_support_val`, `MvPolynomial.optionEquivLeft_monomial`, `finsuppLequivDFinsupp_symm_apply`, `Finsupp.lsum_comp_lsingle`, `Finsupp.mapDomain.addMonoidHom_id`, `Finsupp.lex_lt_iff`, `Algebra.Generators.cotangentRestrict_bijective_of_basis_kaehlerDifferential`, `TensorProduct.finsuppRight_symm_apply_single`, `Polynomial.coeff_homogenize`, `Finsupp.mul_prod_erase`, `Finsupp.DegLex.instIsOrderedCancelAddMonoidDegLexNat`, `Module.Basis.linearMap_repr_symm_apply`, `KaehlerDifferential.mvPolynomialBasis_repr_comp_D`, `Derivation.mapCoeffs_apply`, `Finsupp.tsub_apply`, `Nat.factorizationEquiv_inv_apply`, `finsuppTensorFinsuppLid_single_tmul_single`, `Finsupp.embSigma_apply_self`, `SkewMonoidAlgebra.ofFinsupp_sub`, `Finsupp.embDomain_notin_range`, `Finsupp.support_neg`, `Rep.indMap_hom`, `groupHomology.isoCycles₁_hom_comp_i_assoc`, `MvPolynomial.mem_support_coeff_finSuccEquiv`, `Nat.factorization_eq_zero_iff'`, `Finsupp.embDomain.addMonoidHom_apply`, `MvPolynomial.support_sub`, `AddMonoidAlgebra.ext_iff`, `isArtinian_finsupp`, `span_range_eq_top_iff_surjective_finsuppLinearCombination`, `Finsupp.prod_sum_index`, `Fintype.card_finsupp`, `sigmaFinsuppEquivDFinsupp_apply`, `LaurentPolynomial.support_C_mul_T_of_ne_zero`, `Finsupp.mapDomain_sum`, `Finsupp.single_apply`, `Finsupp.sumFinsuppEquivProdFinsupp_symm_inl`, `Finsupp.lex_def`, `groupHomology.d₁₀_eq_zero_of_isTrivial`, `Representation.leftRegular_norm_apply`, `Finsupp.weight_sub_single_add`, `Finsupp.supported_iUnion`, `Representation.coinvariantsToFinsupp_mk_single`, `Finsupp.single_add_apply`, `Module.Relations.Solution.fromQuotient_comp_toQuotient`, `MonomialOrder.lex_lt_iff`, `Module.Basis.SmithNormalForm.repr_comp_embedding_eq_smul`, `Nat.sub_one_mul_factorization_factorial`, `MvPowerSeries.aeval_eq_sum`, `Representation.ind_mk`, `Module.Basis.toDual_linearCombination_right`, `MvPolynomial.support_esymm''`, `TensorProduct.finsuppLeft_apply_tmul`, `PiTensorProduct.ofFinsuppEquiv'_apply_apply`, `AddMonoidAlgebra.single_zero_mul_apply`, `Finsupp.restrictSupportEquiv_apply`, `Finsupp.smul_apply_addAction`, `groupHomology.d₂₁_single_one_snd`, `Nat.ordProj_dvd`, `LinearMap.toMatrix_toSpanSingleton`, `MvPolynomial.divMonomial_zero`, `MonoidAlgebra.ext_iff`, `MvPolynomial.sum_monomial_eq`, `Finsupp.curryEquiv_symm_apply`, `Finsupp.unique_ext_iff`, `linearDepOn_iffₛ`, `MvPolynomial.degrees_monomial_eq`, `Finsupp.Lex.wellFounded_of_finite`, `Finsupp.Icc_eq`, `Finsupp.addCommute_iff_inter`, `Representation.coinvariantsFinsuppLEquiv_symm_apply`, `Module.finrank_finsupp_self`, `Finsupp.support_smul_eq`, `MvPolynomial.pUnitAlgEquiv_monomial`, `Polynomial.support_derivativeFinsupp_subset_range`, `MvPolynomial.coeff_monomial`, `TensorProduct.equivFinsuppOfBasisRight_symm`, `Cardinal.mk_finsupp_of_infinite`, `MvPolynomial.coeff_mul_monomial`, `groupHomology.d₃₂_comp_d₂₁`, `groupHomology.d₃₂_single_one_snd`, `MvPolynomial.eval₂_eq`, `exteriorPower.basis_repr`, `MvPolynomial.mem_ideal_span_monomial_image_iff_dvd`, `Finsupp.support_eq_empty`, `groupHomology.π_comp_H2Iso_hom_apply`, `finsuppAddEquivDFinsupp_apply`, `Finsupp.indicator_eq_sum_single`, `Finsupp.graph_eq_empty`, `Module.Relations.Solution.span_relation_le_ker_π`, `Nat.factorization_def`, `MvPolynomial.monomial_pow`, `Finsupp.prod_antidiagonal_swap`, `AddMonoidAlgebra.domCongr_apply`, `MonomialOrder.degree_prod`, `IsBaseChange.basis_repr_comp`, `MvPowerSeries.monomial_zero_one`, `Rep.diagonalOneIsoLeftRegular_hom_hom`, `Finsupp.mapRange.linearEquiv_trans`, `OrthonormalBasis.coe_toBasis_repr_apply`, `Finsupp.mapDomain.toLinearMap_linearEquiv`, `Nat.coprime_ordCompl`, `Rep.coinvariantsTensorIndHom_mk_tmul_indVMk`, `ZLattice.normBound_spec`, `QuadraticMap.apply_linearCombination`, `Finsupp.support_mul_subset_left`, `groupHomology.mapCycles₁_hom`, `Nat.Prime.pow_dvd_iff_le_factorization`, `MvPolynomial.coeff_mapRange`, `Finsupp.Colex.single_le_iff`, `finsuppAddEquivDFinsupp_symm_apply`, `groupHomology.isoCycles₁_inv_comp_iCycles`, `Finsupp.embSigma_apply`, `AdjoinRoot.powerBasisAux'_repr_apply_to_fun`, `IsAdjoinRootMonic.coeff_apply_coe`, `Module.Basis.mapCoeffs_repr`, `MvPolynomial.monomial_one_dvd_monomial_one`, `Module.Basis.traceDual_repr_apply`, `groupHomology.cyclesMap_comp_isoCycles₁_hom_assoc`, `Finsupp.linearIndependent_single`, `Nat.factorization_factorial_le_div_pred`, `groupHomology.single_mem_cycles₁_of_mem_invariants`, `groupHomology.isoShortComplexH2_inv`, `Finsupp.liftAddHom_symm_apply_apply`, `groupHomology.coe_mapCycles₁`, `MvPolynomial.coeff_X_mul`, `AddMonoidAlgebra.single_mul_apply_aux`, `groupHomology.toCycles_comp_isoCycles₁_hom`, `Module.Relations.toQuotient_relation`, `Module.Flat.exists_factorization_of_comp_eq_zero_of_free`, `Finsupp.moduleIsTorsionFree`, `Module.Basis.ofZLatticeComap_repr_apply`, `Finsupp.toDFinsupp_zero`, `Finsupp.DegLex.wellFoundedLT`, `Module.projective_def`, `Finsupp.coe_univ_sum_single`, `groupHomology.chainsMap_f_2_comp_chainsIso₂_assoc`, `Finset.finsuppAntidiag_insert`, `HahnSeries.toMvPowerSeries_apply`, `Module.End.ringEquivEndFinsupp_apply_apply_support`, `Finsupp.coe_tsub`, `groupHomology.mapCycles₂_comp_i_apply`, `Module.annihilator_finsupp`, `Finsupp.neLocus_sub_right`, `PolynomialModule.monomial_smul_apply`, `Finsupp.orderedSub`, `LinearMap.toMvPolynomial_eval_eq_apply`, `KaehlerDifferential.mvPolynomialBasis_repr_symm_single`, `groupHomology.boundariesToCycles₂_apply`, `Module.Basis.toMatrix_transpose_apply`, `Module.finite_finsupp_self_iff`, `HahnSeries.SummableFamily.coeff_apply`, `Finsupp.indicator_of_mem`, `MonomialOrder.degree_mul_of_isRegular_left`, `groupHomology.cyclesOfIsCycle₂_coe`, `rank_finsupp'`, `Rep.freeLift_hom`, `Nat.dvd_ordProj_of_dvd`, `Nat.factorization_pow`, `groupHomology.isoCycles₂_hom_comp_i`, `finTwoArrowEquiv'_sum_eq`, `Finsupp.sumFinsuppAddEquivProdFinsupp_symm_inr`, `Finsupp.DegLex.le_iff`, `groupHomology.π_comp_H1Iso_hom`, `Nat.ordProj_pos`, `MvPolynomial.monomial_sum_one`, `Finsupp.curryAddEquiv_symm_apply`, `Finsupp.liftAddHom_symm_apply`, `MonoidAlgebra.mul_apply_right`, `Nat.ordCompl_eq_self_iff_zero_or_not_dvd`, `groupHomology.isoCycles₂_inv_comp_iCycles`, `Module.Basis.ofZLatticeBasis_repr_apply`, `groupHomology.d₁₀_single_inv`, `groupHomology.mkH1OfIsTrivial_apply`, `Finsupp.Lex.wellFoundedLT`, `Finsupp.span_single_image`, `Nat.ordProj_mul`, `Nat.factorization_eq_zero_of_remainder`, `IsIsotypic.linearEquiv_finsupp`, `Finsupp.optionEquiv_symm_apply`, `SkewMonoidAlgebra.toFinsupp_eq_zero`, `Finsupp.equivFunOnFinite_symm_single`, `Finsupp.sum_add_index`, `Finsupp.degree_eq_zero_iff`, `Finsupp.toMultiset_single`, `Finsupp.mem_graph_iff`, `Finsupp.single_neg`, `Finsupp.tail_apply`, `LinearMap.toMatrixAlgEquiv_apply'`, `MvPowerSeries.coeff_subst_finite`, `MonomialOrder.div`, `Finsupp.equivFunOnFinite_symm_sum`, `Finsupp.linearCombination_surjective`, `IntermediateField.LinearDisjoint.basisOfBasisLeft_repr_apply`, `MvPolynomial.scalarRTensor_symm_apply_single`, `Finsupp.support_sup`, `MonomialOrder.lex_le_iff`, `Finsupp.lsingle_range_le_ker_lapply`, `groupHomology.d₁₀ArrowIso_hom_right`, `TensorProduct.equivFinsuppOfBasisLeft_apply`, `Module.Basis.prod_repr_inr`, `Finsupp.support_subset_iff`, `Finsupp.range_lmapDomain`, `Finsupp.neLocus_self_add_right`, `Rep.freeLift_hom_single_single`, `Finsupp.extendDomain_apply`, `AddEquiv.finsuppUnique_symm_apply_apply`, `Finsupp.add_sum_erase`, `Rep.leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single`, `Finsupp.sum_smul_index_addMonoidHom`, `groupHomology.single_one_mem_boundaries₁`, `Finsupp.subtypeDomain_sub`, `Finsupp.single_sum`, `Finsupp.linearCombination_comp_lmapDomain`, `Finsupp.support_monotone`, `Finsupp.mem_span_image_iff_linearCombination`, `Finsupp.comapDomain.addMonoidHom_apply`, `MvPowerSeries.order_eq_nat`, `Nat.factorization_choose_prime_pow`, `MvPolynomial.irreducible_sumSMulXSMulY`, `Finsupp.equivMapDomain_refl'`, `MonomialOrder.degree_sPolynomial_le`, `MvPolynomial.mem_ideal_span_monomial_image`, `ArithmeticFunction.carmichael_factorization`, `Finsupp.sum_apply`, `BilinForm.apply_eq_dotProduct_toMatrix_mulVec`, `Nat.factorization_choose`, `Module.Relations.toQuotient_map`, `MvPolynomial.IsSymmetric.antitone_supDegree`, `LaurentPolynomial.support_C_mul_T`, `groupHomology.d₂₁_single`, `Finsupp.mapDomain.linearEquiv_symm`, `Module.Basis.constr_def`, `Finsupp.domCongr_trans`, `MvPowerSeries.support_expand_subset`, `MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_degree`, `Finsupp.mapRange.zeroHom_id`, `Finsupp.mapRange.addEquiv_trans`, `groupHomology.inhomogeneousChains.d_eq`, `Finsupp.comul_comp_lsingle`, `MvPolynomial.coeff_weightedHomogeneousComponent`, `groupHomology.cycles₁IsoOfIsTrivial_inv_apply`, `Finsupp.coe_sum`, `Finsupp.Lex.addRightMono`, `MonomialOrder.coeff_mul_of_degree_add`, `groupHomology.eq_d₂₁_comp_inv_apply`, `Finsupp.faithfulSMul`, `MonomialOrder.degree_sub_leadingTerm_lt_degree`, `Module.Basis.toDual_apply_left`, `MonomialOrder.coeff_sPolynomial_sup_eq_zero`, `Finsupp.support_sup_union_support_inf`, `Finsupp.optionEquiv_apply`, `QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar`, `MvPolynomial.rTensor_apply`, `groupHomology.d₁₀_comp_coinvariantsMk_assoc`, `Finsupp.degree_mono`, `TensorProduct.sum_tmul_basis_left_eq_zero`, `MvPowerSeries.monomial_mul_monomial`, `Module.DualBases.lc_def`, `Finsupp.Lex.acc`, `Finsupp.card_support_le_one`, `Finsupp.single_eq_pi_single`, `MonoidAlgebra.mapDomainAddEquiv_apply`, `groupHomology.isoCycles₁_hom_comp_i`, `Finsupp.coe_mul`, `Module.Relations.Solution.IsPresentation.exact`, `MvPolynomial.leadingCoeff_toLex`, `Finsupp.sum_ite_self_eq'`, `Finsupp.sum_zero_index`, `Nat.factorization_eq_zero_iff`, `NumberField.canonicalEmbedding_eq_basisMatrix_mulVec`, `Finsupp.coe_mk`, `Module.Relations.solutionFinsupp_isPresentation`, `groupHomology.chainsMap_f_0_comp_chainsIso₀_apply`, `MonoidAlgebra.mul_single_apply`, `Finset.finsuppAntidiag_zero`, `AList.lookupFinsupp_apply`, `Finsupp.eraseAddHom_apply`, `Module.Basis.reindexFinsetRange_repr`, `Finsupp.mem_frange`, `Module.Basis.continuous_coe_repr`, `MonomialOrder.degree_mul`, `Finsupp.sym2Mul_apply_mk`, `Finsupp.mapDomain_apply'`, `TensorProduct.finsuppScalarLeft_apply`, `MonomialOrder.degree_monomial_le`, `DFinsupp.toFinsupp_neg`, `Module.Basis.smulTower_repr`, `Module.Basis.toDual_apply_right`, `groupHomology.single_inv_ρ_self_add_single_mem_boundaries₁`, `Finsupp.toMultiset_sup`, `MvPolynomial.coeff_mul_monomial'`, `MvPowerSeries.lexOrder_le_of_coeff_ne_zero`, `Finsupp.linearCombination_comapDomain`, `Module.DualBases.coeffs_apply`, `Nat.Prime.exists_addOrderOf_eq_pow_padic_val_nat_add_exponent`, `Nat.factorization_eq_zero_of_non_prime`, `MonomialOrder.degLex_single_lt_iff`, `List.toFinsupp_apply`, `Finsupp.toLex_monotone`, `ZSpan.repr_floor_apply`, `Finsupp.equivFunOnFinite_single`, `Finsupp.comapDomain_add_of_injective`, `Module.Basis.repr_symm_apply`, `Finsupp.coe_sub`, `Finsupp.apply_linearCombination_id`, `MonoidAlgebra.single_apply`, `Finsupp.support_inf`, `Module.Basis.tensorProduct_repr_tmul_apply`, `Finsupp.smul_single_one`, `Finsupp.Colex.single_lt_iff`, `MvPolynomial.restrictSupport_eq_span`, `Nat.prod_pow_factorization_centralBinom`, `MonomialOrder.degree_sub_LTerm_lt`, `Finsupp.sub_single_one_add`, `Representation.free_asModule_free`, `Finset.mem_finsuppAntidiag'`, `groupHomology.lsingle_comp_chainsMap_f_assoc`, `FirstOrder.Ring.mvPolynomial_zeroLocus_definable`, `Rep.linearizationTrivialIso_hom_hom`, `MvPolynomial.rank_eq`, `Basis.piTensorProduct_repr_tprod_apply`, `MonomialOrder.sPolynomial_lt_of_degree_ne_zero_of_degree_eq`, `Finsupp.cons_zero_zero`, `Finsupp.mul_prod_erase'`, `Finsupp.single_zero`, `Module.Relations.Solution.π_comp_map_apply`, `groupHomology.single_mem_cycles₂_iff`, `TensorProduct.finsuppScalarLeft_symm_apply_single`, `Module.Basis.repr_smul'`, `Finsupp.Lex.lt_iff`, `lmap_finsuppLEquivDirectSum_eq`, `Finsupp.subtypeDomain_sum`, `Finsupp.DegLex.monotone_degree`, `Finsupp.ker_lsingle`, `Module.Projective.out`, `groupHomology.boundaries₁_le_cycles₁`, `Module.Basis.repr_unitsSMul`, `MvPolynomial.support_symmDiff_support_subset_support_add`, `Representation.ind_apply`, `MvPolynomial.isEmptyRingEquiv_eq_coeff_zero`, `Finsupp.equivFunOnFinite_symm_eq_sum`, `MvPolynomial.mem_coeffs_iff`, `PowerSeries.coeff_pow`, `Finsupp.coe_mono`, `Finsupp.wellFoundedLT_of_finite`, `Nat.ordCompl_dvd`, `Module.Basis.constr_apply`, `MvPolynomial.divMonomial_add`, `Module.Finite.finsupp`, `MonoidAlgebra.mul_apply_antidiagonal`, `Finsupp.single_nonneg`, `Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply`, `Rep.diagonalSuccIsoFree_hom_hom_single`, `Finsupp.ext_iff`, `Finsupp.linearCombination_eq_fintype_linearCombination_apply`, `Nat.factorization_eq_zero_of_lt`, `AList.lookupFinsupp_surjective`, `Finsupp.Lex.single_le_iff`, `Subalgebra.LinearDisjoint.basisOfBasisLeft_repr_apply`, `TensorProduct.sum_tmul_basis_right_eq_zero`, `Finsupp.support_tsub`, `Finsupp.mapDomain.addMonoidHom_comp_mapRange`, `MvPowerSeries.hasSum_eval₂`, `AddMonoidAlgebra.single_mem_gradeBy`, `Finsupp.disjoint_supported_supported_iff`, `Finsupp.erase_single`, `MonomialOrder.degree_prod_of_regular`, `List.toFinsupp_append`, `Nat.Partition.coeff_genFun`, `mem_finsuppAffineCoords_iff_linearCombination`, `Rep.free_ext_iff`, `Nat.factorization_gcd`, `Finsupp.optionElim_apply_none`, `Submodule.LinearDisjoint.linearIndependent_left_of_flat`, `Module.Basis.repr_eq_iff'`, `linearDepOn_iff'`, `Finsupp.mapDomain_add`, `Finsupp.snd_sumFinsuppEquivProdFinsupp`, `List.toFinsupp_nil`, `Finsupp.prod_finset_sum_index`, `Finsupp.smul_single`, `Module.End.ringEquivEndFinsupp_symm_apply_apply`, `Finsupp.sum_single`, `Finsupp.supportedEquivFinsupp_symm_apply_coe_apply`, `Finsupp.subtypeDomain_zero`, `Finsupp.sumElim_inl`, `MvPolynomial.support_esymm`, `Module.Presentation.tautologicalRelations_relation`, `iSupIndep_range_lsingle`, `Rep.coinvariantsTensorIndInv_mk_tmul_indMk`, `Finsupp.sum_finset_sum_index`, `Cardinal.mk_finsupp_lift_of_infinite'`, `Finsupp.mapRange_finset_sum`, `MonoidAlgebra.single_mul_apply_of_not_exists_mul`, `Module.Basis.norm_repr_le_norm`, `MvPolynomial.scalarRTensor_apply_tmul_apply`, `MvPowerSeries.le_lexOrder_mul`, `Module.Basis.mem_span_repr_support`, `Pi.basisFun_repr`, `Algebra.leftMulMatrix_eq_repr_mul`, `Finsupp.apply_eq_of_mem_graph`, `Subalgebra.LinearDisjoint.mulLeftMap_ker_eq_bot_iff_linearIndependent_op`, `Finsupp.infinite_of_right`, `Finsupp.finsuppProdLEquiv_symm_apply_apply`, `Module.Basis.sum_repr`, `HahnSeries.SummableFamily.coeff_def`, `Finsupp.lmapDomain_disjoint_ker`, `Finsupp.supportedEquivFinsupp_apply_apply`, `ZSpan.mem_fundamentalDomain`, `Finsupp.nsmul_single_one_image`, `Finsupp.neLocus_self_sub_right`, `Finsupp.DegLex.lt_def`, `groupHomology.d₁₀ArrowIso_inv_left`, `groupHomology.H1AddEquivOfIsTrivial_symm_tmul`, `Module.Basis.toMatrix_mulVec_repr`, `Algebra.Generators.comp_σ`, `groupHomology.single_mem_cycles₁_iff`, `groupHomology.d₂₁_single_ρ_add_single_inv_mul`, `MvPolynomial.support_smul`, `MvPowerSeries.monomial_smul_eq`, `Finsupp.single_mem_supported`, `TensorProduct.sum_tmul_basis_left_injective`, `MvPowerSeries.order_monomial_of_ne_zero`, `Finsupp.graph_injective`, `Finsupp.indicator_injective`, `finsetBasisOfLinearIndependentOfCardEqFinrank_repr_apply`, `Module.End.ringHomEndFinsupp_surjective`, `Finsupp.isScalarTower`, `TensorProduct.equivFinsuppOfBasisRight_symm_apply`, `Finsupp.card_support_eq_zero`, `MvPolynomial.coeff_zero_one`, `Module.Basis.algebraMapCoeffs_repr`, `MvPolynomial.support_X`, `MonoidAlgebra.opRingEquiv_apply`, `Nat.factorization_inj`, `Finsupp.toMultiset_sum_single`, `Nat.factorization_prod`, `Module.Basis.coord_apply`, `Multiset.toFinsupp_support`, `groupHomology.eq_d₁₀_comp_inv_apply`, `Finsupp.support_sum_eq_biUnion`, `Module.Basis.mem_span_iff_repr_mem`, `Module.Basis.SmithNormalForm.repr_eq_zero_of_notMem_range`, `Module.Relations.Solution.IsPresentation.ker_π`, `KaehlerDifferential.quotKerTotalEquiv_apply`, `AddMonoidAlgebra.mul_apply_right`, `Finsupp.notMem_neLocus`, `KaehlerDifferential.kerTotal_map'`, `Finsupp.instIsLeftCancelAdd`, `Rep.leftRegularTensorTrivialIsoFree_hom_hom`, `Finsupp.sumFinsuppEquivProdFinsupp_apply`, `Finsupp.Colex.lt_iff_of_unique`, `Finsupp.weight_eq_zero_iff_eq_zero`, `Finsupp.embDomain_some_none`, `Finsupp.toMultiset_map`, `Finsupp.support_curry`, `Rep.barComplex.d_single`, `Module.Presentation.tautological_relation`, `Finsupp.mapDomain_smul`, `Finsupp.prod_ite_eq'`, `Finsupp.some_apply`, `Finsupp.domLCongr_refl`, `groupHomology.d₂₁_comp_d₁₀_assoc`, `MvPolynomial.monomial_single_add`, `LinearMap.toMatrixAlgEquiv_transpose_apply`, `Finsupp.mapRange_multiset_sum`, `Module.Basis.repr_self`, `MvPolynomial.support_X_mul`, `exteriorPower.presentation.relations_relation`, `Finsupp.restrictSupportEquiv_symm_apply_coe`, `MonoidAlgebra.domCongr_apply`, `MonomialOrder.degree_mul'`, `Finsupp.mapRange.addMonoidHom_id`, `TensorProduct.finsuppRight_apply_tmul_apply`, `Finsupp.sum_ite_self_eq`, `MvPolynomial.degreeOf_monomial_eq`, `Finsupp.linearCombination_zero`, `Nat.factorization_mul_of_coprime`, `Rep.linearization_ε_hom`, `Multiset.toFinsupp_strictMono`, `Finsupp.lcomapDomain_eq_linearProjOfIsCompl`, `Finsupp.Lex.wellFoundedLT_of_finite`, `MonomialOrder.degree_sPolynomial_lt_sup_degree`, `groupHomology.chainsMap_f_1_comp_chainsIso₁_apply`, `isPrimePow_iff_minFac_pow_factorization_eq`, `MvPolynomial.coeff_expand_zero`, `TensorProduct.finsuppRight_apply_tmul`, `Finsupp.toMultiset_inf`, `Module.subsingletonEquiv_apply`, `groupHomology.isBoundary₁_iff`, `MvPowerSeries.LinearTopology.hasBasis_nhds_zero`, `Finsupp.mapDomain_injective`, `Polynomial.degreeLT.basis_repr`, `Finsupp.coe_zero`, `Nat.ordCompl_self_pow`, `AddMonoidAlgebra.mul_single_apply_of_not_exists_add`, `Module.Basis.repr_reindex_apply`, `Finsupp.weight_apply`, `groupHomology.mapCycles₁_quotientGroupMk'_epi`, `MvPolynomial.support_C`, `Finsupp.degree_def`, `groupHomology.mapCycles₁_comp_i_assoc`, `LinearMap.toMatrix_apply`, `linearDepOn_iff'ₛ`, `MonomialOrder.degree_sub_leadingTerm_lt_iff`, `Nat.factorization_zero_right`, `NumberField.house.basis_repr_norm_le_const_mul_house`, `MonoidAlgebra.neg_apply`, `MvPolynomial.weightedHomogeneousComponent_apply`, `Finsupp.Set.indicator_singleton_eq`, `Nat.pow_factorization_choose_le`, `Finsupp.coe_orderIsoMultiset`, `AddMonoidAlgebra.mapRangeAlgHom_apply`, `MonomialOrder.degree_mul_of_right_mem_nonZeroDivisors`, `Nat.factorization_le_of_le_pow`, `Rep.coinvariantsTensorFreeToFinsupp_mk_tmul_single`, `DFinsupp.toFinsupp_zero`, `MonomialOrder.degree_sub_leadingTerm_le`, `MvPolynomial.rename_eq`, `Cardinal.mk_finsupp_of_infinite'`, `MvPolynomial.rank_eq_lift`, `Finsupp.linearIndependent_single_one`, `LinearMap.map_finsupp_linearCombination`, `Finsupp.lt_wf`, `MvPolynomial.coeff_mul`, `Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination`, `Finsupp.Lex.lt_iff_of_unique`, `Finsupp.range_restrictDom`, `LinearMap.toMatrixAlgEquiv_transpose_apply'`, `Module.Relations.Solution.π_single`, `Finsupp.lmapDomain_apply`, `linearIndepOn_iff_linearCombinationOnₛ`, `Finsupp.DegLex.single_strictAnti`, `Finset.card_finsupp`, `Finsupp.instCanLift`, `Module.presentationFinsupp_var`, `finiteDimensional_finsupp`, `SkewMonoidAlgebra.toFinsupp_sum'`, `Rep.linearization_map_hom`, `Finsupp.domLCongr_single`, `groupHomology.mem_cycles₁_iff`, `Finsupp.sum_sum_index`, `Nat.factorization_eq_of_coprime_left`, `factorization_one`, `instIsSemisimpleModuleFinsupp`, `MvPolynomial.bind₁_monomial`, `TensorProduct.coe_finsuppScalarRight'`, `LinearMap.polyCharpoly_coeff_eval`, `lsum_comp_mapRange_toSpanSingleton`, `MvPolynomial.degreeOf_lt_iff`, `HahnSeries.SummableFamily.coe_ofFinsupp`, `Finsupp.sum_of_support_subset`, `Module.Basis.repr_unop_eq_mulOpposite_repr`, `groupHomology.boundariesToCycles₁_apply`, `groupHomology.single_mem_cycles₂_iff_inv`, `groupHomology.d₁₀_single`, `Module.Relations.tensor_relation`, `linearIndepOn_iff_linearCombinationOn`, `MvPowerSeries.coeff_mul`, `Finsupp.lsingle_apply`, `Finsupp.Colex.single_strictMono`, `Representation.IndV.hom_ext_iff`, `Module.Relations.Solution.IsPresentation.π_desc_apply`, `Pi.comul_comp_finsuppLcoeFun`, `Finsupp.mem_pi`, `Finsupp.toFreeAbelianGroup_comp_toFinsupp`, `exteriorPower.basis_repr_self`, `TensorProduct.finsuppLeft'_apply`, `Finsupp.erase_sub`, `Polynomial.derivativeFinsupp_C`, `TensorProduct.finsuppRight_tmul_single`, `Submodule.mulRightMap_apply_single`, `Module.finrank_finsupp`, `Rep.indResHomEquiv_symm_apply_hom`, `groupHomology.isoCycles₂_hom_comp_i_assoc`, `Finsupp.filter_zero`, `Finsupp.card_support_eq_one`, `groupHomology.comp_d₃₂_eq`, `MvPowerSeries.lexOrder_mul_ge`, `Polynomial.derivativeFinsupp_X`, `finsuppLEquivDirectSum_symm_lof`, `Module.Flat.exists_factorization_of_isFinitelyPresented`, `Pi.lex_eq_finsupp_lex`, `groupHomology.H2π_eq_zero_iff`, `Finsupp.toMultiset_eq_iff`, `Finsupp.curryLinearEquiv_symm_apply`, `KaehlerDifferential.linearCombination_surjective`, `Finsupp.lsubtypeDomain_apply`, `HahnSeries.coeff_ofFinsuppLinearMap`, `Module.Basis.sumQuot_repr_inr`, `instUniqueSumsFinsupp`, `Finsupp.prod_zero_index`, `Finsupp.linearCombination_onFinset`, `Finsupp.lsum_symm_apply`, `MvPowerSeries.coeff_add_monomial_mul`, `Finsupp.support_sub`, `AddMonoidAlgebra.mul_apply_antidiagonal`, `Module.Basis.coord_repr_symm`, `Module.Relations.Solution.linearCombination_var_relation`, `Finsupp.lcongr_apply_apply`, `MonomialOrder.degree_sub_LTerm_le`, `Nat.factorization_le_factorization_of_dvd_right`, `Nat.ordCompl_of_not_prime`, `MonomialOrder.lex_le_iff_of_unique`, `MonomialOrder.sPolynomial_mul_monomial`, `MonomialOrder.degree_prod_of_mem_nonZeroDivisors`, `Nat.factorization_factorial_mul`, `Finsupp.instNontrivial`, `MvPowerSeries.prod_monomial`, `MonoidAlgebra.mul_single_apply_aux`, `Rep.leftRegularTensorTrivialIsoFree_inv_hom_single_single`, `ZLattice.abs_repr_le`, `MonomialOrder.degree_pow_of_pow_leadingCoeff_ne_zero`, `DirectSum.IsInternal.collectedBasis_repr_of_mem`, `Module.Basis.coe_sumCoords`, `Finsupp.equivFunOnFinite_symm_apply_apply`, `MvPolynomial.decomposition.decompose'_eq`, `Finsupp.iSup_lsingle_range`, `LinearMap.sum_repr_mul_repr_mul`, `MonomialOrder.sPolynomial_leadingTerm_mul`, `Nat.squarefree_iff_factorization_le_one`, `Finsupp.mem_supported'`, `MonoidAlgebra.mapRangeRingHom_apply`, `Finsupp.lmapDomain_supported`, `Finsupp.DegLex.wellFounded`, `Module.Basis.ofIsLocalizedModule_repr_apply`, `MonomialOrder.degree_sPolynomial`, `Rep.linearization_μ_hom`, `AddMonoidAlgebra.apply_supDegree_add_supDegree`, `Module.Relations.Solution.ofQuotient_π`, `Finsupp.single_of_single_apply`, `Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply`, `groupHomology.H1π_eq_iff`, `LinearMap.fst_prodOfFinsuppNat`, `groupHomology.d₃₂_comp_d₂₁_apply`, `Finsupp.update_eq_erase_add_single`, `MvPolynomial.monomial_dvd_monomial`, `TensorProduct.finsuppLeft_apply_tmul_apply`, `groupHomology.chainsMap_f`, `MonomialOrder.degree_X_le_single`, `groupHomology.chainsMap_f_2_comp_chainsIso₂_apply`, `LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly`, `Finsupp.image_pow_eq_finsuppProd_image`, `Representation.ofMulAction_def`, `groupHomology.cyclesMap_comp_isoCycles₁_hom`, `Finsupp.sym2_support_eq_preimage_support_mul`, `Finsupp.mapDomain_notin_range`, `Finsupp.sum_option_index`, `sigmaFinsuppLequivDFinsupp_apply`, `Finsupp.curry_apply`, `Nat.factorization_factorial_eq_zero_of_lt`, `KaehlerDifferential.kerTotal_mkQ_single_algebraMap`, `MonoidAlgebra.mul_apply_left`, `MvPolynomial.rTensorAlgHom_apply_eq`

---

← Back to Index