| 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 | 231 mathmath: instCanonicallyOrderedAddOfAddLeftMono, toDFinsupp_add, MvPolynomial.support_mul, Colex.addLeftStrictMono, List.toFinsupp_eq_sum_mapIdx_single, MvPolynomial.coeff_divMonomial, MonomialOrder.degree_add_of_ne, Multiset.toFinsupp_add, sumFinsuppLEquivProdFinsupp_apply, groupHomology.dââ_single, domCongr_refl, neLocus_add_left, sumFinsuppAddEquivProdFinsupp_symm_inl, prod_add_index_of_disjoint, instIsRightCancelAdd, sigmaFinsuppAddEquivDFinsupp_apply, List.toFinsupp_cons_eq_single_add_embDomain, MvPolynomial.mul_def, mapRange.addEquiv_refl, groupHomology.mem_cyclesâ_iff, groupHomology.single_isCycleâ_iff_inv, DFinsupp.toFinsupp_add, subtypeDomain_add, support_single_add_single, sum_single_add_single, update_eq_add_single, MonomialOrder.degree_sub_le, sigmaFinsuppAddEquivPiFinsupp_apply, neLocus_self_add_left, add_sub_single_one, Lex.addLeftMono, prod_add_index, toMultiset_toFinsupp, mapRange.addEquiv_apply, MonomialOrder.degree_reduce_lt, Multiset.toFinsupp_sum_eq, sumFinsuppAddEquivProdFinsupp_symm_apply, sigmaFinsuppAddEquivDFinsupp_symm_apply, AddEquiv.finsuppUnique_symm, MonomialOrder.toSyn_strictMono, MonomialOrder.div_single, groupHomology.dââ_single_inv_mul_Ď_add_single, support_add_single, mapRange.addEquiv_toEquiv, Nat.factorization_mul, MonomialOrder.degree_add_le, some_add, factorization_mul, MvPowerSeries.lexOrder_mul, Colex.addRightMono, update_eq_single_add, add_eq_zero_iff, MonomialOrder.le_degree, sigmaFinsuppEquivDFinsupp_add, Colex.addRightStrictMono, embSigma_add, sub_add_single_one_cancel, erase_add, Multiset.toFinsupp_union, add_apply, sumFinsuppLEquivProdFinsupp_symm_apply, support_add_eq, prod_add_index', MonomialOrder.lex_lt_iff_of_unique, SkewMonoidAlgebra.toFinsuppAddEquiv_apply, FreeAbelianGroup.equivFinsupp_symm_apply, AddCommGroup.equiv_free_prod_directSum_zmod, MonomialOrder.degLex_le_iff, Multiset.toFinsupp_inter, MonomialOrder.degree_le_iff, domCongr_apply, Multiset.toFinsupp_apply, sum_add_index', AddEquiv.finsuppUnique_apply, MonomialOrder.degree_mul_of_isRegular_right, MvPolynomial.coeff_monomial_mul, Finset.mapRange_finsuppAntidiag_eq, MonomialOrder.degree_sum_le, instTwoUniqueSumsFinsupp, MonomialOrder.degree_mul_of_mul_leadingCoeff_ne_zero, filter_add, snd_sumFinsuppAddEquivProdFinsupp, MonomialOrder.degree_mul_lt_iff_left_lt_of_ne_zero, coe_curryAddEquiv, MonomialOrder.degree_smul_le, mapRange.addEquiv_symm, MonomialOrder.degree_mul_le, neLocus_add_right, sum_add_index_of_disjoint, MonomialOrder.le_add_right, MonomialOrder.degree_mul_of_left_mem_nonZeroDivisors, MvPolynomial.monomial_add_single, MonomialOrder.degree_pow_le, prod_hom_add_index, domCongr_symm, addCommute_of_disjoint, update_eq_single_add_erase, degree_preimage_add, Relation.cutExpand_le_invImage_lex, MonomialOrder.toSyn_monotone, MonomialOrder.degLex_single_le_iff, MvPolynomial.support_mul_X, SkewMonoidAlgebra.toFinsuppAddEquiv_symm_apply, List.toFinsupp_concat_eq_toFinsupp_add_single, mapRange_add', sumFinsuppAddEquivProdFinsupp_apply, Finset.mapRange_finsuppAntidiag_subset, groupHomology.inhomogeneousChains.d_single, groupHomology.isBoundaryâ_iff, toMultiset_add, Multiset.toFinsupp_singleton, Multiset.toFinsupp_symm_apply, FreeAbelianGroup.equivFinsupp_apply, groupHomology.single_isCycleâ_iff, List.support_sum_eq, MvPolynomial.coeff_mul_X, instIsCancelAdd, SkewMonoidAlgebra.ofFinsupp_add, coe_add, MvPowerSeries.coeff_add_mul_monomial, MvPolynomial.restrictSupport_nsmul, coe_orderIsoMultiset_symm, SkewMonoidAlgebra.toFinsupp_add, groupHomology.single_Ď_self_add_single_inv_mem_boundariesâ, support_single_add_single_subset, fst_sumFinsuppAddEquivProdFinsupp, MonomialOrder.sPolynomial_monomial_mul, support_single_add, exteriorPower.presentation_relation, Lex.addRightStrictMono, erase_add_single, MvPolynomial.monomial_mul, MonomialOrder.toSyn_eq_zero_iff, update_eq_sub_add_single, sigmaFinsuppLequivDFinsupp_symm_apply, Multiset.toFinsupp_zero, single_add_erase, Multiset.toFinsupp_toMultiset, MonomialOrder.degree_prod_le, MonomialOrder.div_set, single_add, embDomain_add, degree_preimage_nsmul, Lex.addLeftStrictMono, MonomialOrder.degLex_lt_iff, sum_hom_add_index, mapRange.addEquiv_toAddMonoidHom, Nat.factorization_eq_primeFactorsList_multiset, addLeftReflectLE, MvPolynomial.esymmAlgHomMonomial_add, List.support_sum_subset, Multiset.toFinsupp_eq_iff, filter_pos_add_filter_neg, support_add, AddEquiv.finsuppUnique_symm_apply_support_val, domLCongr_apply, MvPolynomial.restrictSupport_add, Colex.addLeftMono, single_add_single_eq_single_add_single, MvPolynomial.support_divMonomial, mapRange_add, MonomialOrder.lex_lt_iff, addCommute_iff_inter, MvPolynomial.coeff_mul_monomial, finsuppAddEquivDFinsupp_apply, finsuppAddEquivDFinsupp_symm_apply, MvPolynomial.coeff_X_mul, orderedSub, MonomialOrder.degree_mul_of_isRegular_left, sumFinsuppAddEquivProdFinsupp_symm_inr, curryAddEquiv_symm_apply, sum_add_index, MonomialOrder.div, MonomialOrder.lex_le_iff, neLocus_self_add_right, AddEquiv.finsuppUnique_symm_apply_apply, MonomialOrder.degree_sPolynomial_le, groupHomology.dââ_single, domCongr_trans, mapRange.addEquiv_trans, Lex.addRightMono, MonomialOrder.coeff_mul_of_degree_add, MonomialOrder.degree_sub_leadingTerm_lt_degree, MvPowerSeries.monomial_mul_monomial, MonomialOrder.degree_mul, MonomialOrder.degree_monomial_le, groupHomology.single_inv_Ď_self_add_single_mem_boundariesâ, MonomialOrder.degLex_single_lt_iff, comapDomain_add_of_injective, MonomialOrder.degree_sub_LTerm_lt, sub_single_one_add, MonomialOrder.sPolynomial_lt_of_degree_ne_zero_of_degree_eq, groupHomology.single_mem_cyclesâ_iff, MvPolynomial.divMonomial_add, List.toFinsupp_append, Nat.Partition.coeff_genFun, mapDomain_add, Module.Presentation.tautologicalRelations_relation, MvPowerSeries.le_lexOrder_mul, nsmul_single_one_image, groupHomology.dââ_single_Ď_add_single_inv_mul, Multiset.toFinsupp_support, MvPowerSeries.coeff_mul_of_add_lexOrder, instIsLeftCancelAdd, Rep.barComplex.d_single, Module.Presentation.tautological_relation, MvPolynomial.monomial_single_add, MvPolynomial.support_X_mul, exteriorPower.presentation.relations_relation, MonomialOrder.degree_mul', Nat.factorization_mul_of_coprime, Multiset.toFinsupp_strictMono, MonomialOrder.degree_sPolynomial_lt_sup_degree, groupHomology.isBoundaryâ_iff, MonomialOrder.degree_sub_leadingTerm_lt_iff, MonomialOrder.degree_mul_of_right_mem_nonZeroDivisors, MonomialOrder.degree_sub_leadingTerm_le, groupHomology.single_mem_cyclesâ_iff_inv, 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, MonomialOrder.sPolynomial_leadingTerm_mul, MonomialOrder.degree_sPolynomial, update_eq_erase_add_single, MonomialOrder.degree_X_le_single, sigmaFinsuppLequivDFinsupp_apply
|
instAddCommGroup đ | CompOp | 212 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, Rep.leftRegularHom_hom, groupHomology.eq_dââ_comp_inv, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_left, Module.FaithfullyFlat.finsupp, groupHomology.cyclesMap_comp_isoCyclesâ_hom, groupHomology.comp_dââ_eq, groupHomology.mapCyclesâ_comp_assoc, groupHomology.toCycles_comp_isoCyclesâ_hom_assoc, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_right, groupHomology.dââ_single_one_thd, groupHomology.isoCyclesâ_inv_comp_iCycles_apply, KaehlerDifferential.quotKerTotalEquiv_symm_comp_D, groupHomology.chainsâToCoinvariantsKer_surjective, Rep.coinvariantsTensorFreeLEquiv_symm_apply, Rep.standardComplex.d_eq, Module.presentationFinsupp_G, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_single, groupHomology.dââ_comp_dââ_assoc, Rep.coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, 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, 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, Rep.indResAdjunction_counit_app_hom_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, Rep.finsuppTensorRight_hom_hom, KaehlerDifferential.derivationQuotKerTotal_apply, groupHomology.dââ_comp_coinvariantsMk, groupHomology.dââ_comp_dââ_apply, groupHomology.mapCyclesâ_comp_apply, Rep.coindFunctorIso_inv_app_hom_hom_apply_coe, groupHomology.H2Ď_eq_iff, groupHomology.H1AddEquivOfIsTrivial_single, groupHomology.range_dââ_eq_coinvariantsKer, groupHomology.isoCyclesâ_hom_comp_i_apply, groupHomology.eq_dââ_comp_inv_assoc, Rep.ofMulActionSubsingletonIsoTrivial_inv_hom, groupHomology.cyclesMap_comp_isoCyclesâ_hom_assoc, groupHomology.inhomogeneousChains.d_single, Rep.diagonalOneIsoLeftRegular_inv_hom, 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, Rep.diagonalSuccIsoTensorTrivial_hom_hom_single, 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, Rep.ofMulActionSubsingletonIsoTrivial_hom_hom, Module.length_finsupp, Rep.linearizationTrivialIso_inv_hom, 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, Rep.finsuppTensorRight_inv_hom, groupHomology.mapCyclesâ_hom, groupHomology.isoCyclesâ_inv_comp_iCycles_apply, groupHomology.isoCyclesâ_inv_comp_iCycles_assoc, KaehlerDifferential.derivationQuotKerTotal_lift_comp_linearCombination, groupHomology.cyclesMkâ_eq, groupHomology.chainsMap_f_1_comp_chainsIsoâ, Rep.coindVEquiv_apply_hom, 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.finsuppTensorLeft_inv_hom, groupHomology.instEpiModuleCatH2Ď, Rep.leftRegularTensorTrivialIsoFree_inv_hom, 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, Rep.linearization_δ_hom, groupHomology.mapCyclesâ_id_comp_apply, groupHomology.H2Ď_comp_map_apply, Rep.FiniteCyclicGroup.homResolutionIso_hom_f_hom_apply, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply, Rep.finsuppTensorLeft_hom_hom, groupHomology.inhomogeneousChains.d_comp_d, Rep.indMap_hom, 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.diagonalOneIsoLeftRegular_hom_hom, Rep.coinvariantsTensorIndHom_mk_tmul_indVMk, groupHomology.mapCyclesâ_hom, 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, groupHomology.mapCyclesâ_comp_i_apply, Rep.freeLift_hom, 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, Rep.leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single, 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, Rep.linearizationTrivialIso_hom_hom, 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, Rep.leftRegularTensorTrivialIsoFree_hom_hom, groupHomology.dââ_comp_dââ_assoc, Rep.linearization_Îľ_hom, lcomapDomain_eq_linearProjOfIsCompl, groupHomology.chainsMap_f_1_comp_chainsIsoâ_apply, groupHomology.mapCyclesâ_quotientGroupMk'_epi, groupHomology.mapCyclesâ_comp_i_assoc, Module.presentationFinsupp_var, finiteDimensional_finsupp, Rep.linearization_map_hom, instIsSemisimpleModuleFinsupp, groupHomology.dââ_single, Representation.IndV.hom_ext_iff, Rep.indResHomEquiv_symm_apply_hom, groupHomology.isoCyclesâ_hom_comp_i_assoc, groupHomology.comp_dââ_eq, groupHomology.H2Ď_eq_zero_iff, Rep.leftRegularTensorTrivialIsoFree_inv_hom_single_single, Rep.linearization_Îź_hom, 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 | 861 mathmath: TensorProduct.finsuppRight_apply, snd_sumFinsuppLEquivProdFinsupp, LinearMap.exists_finsupp_nat_of_fin_fun_injective, fst_sumFinsuppLEquivProdFinsupp, groupHomology.Ď_comp_H2Iso_hom_assoc, support_finset_sum, Module.Free.finsupp, Rep.coe_linearization_obj_Ď, HahnSeries.instNoZeroDivisorsFinsuppNat, groupHomology.mapCyclesâ_comp_assoc, Orthonormal.inner_left_finsupp, mapRange.linearEquiv_refl, Module.Basis.end_repr_apply, Algebra.Presentation.differentials.commââ_single, mem_supported_support, MvPolynomial.rTensor_apply_tmul_apply, floorDiv_def, restrictDom_apply, groupHomology.boundariesâ_le_cyclesâ, instIsOrderedCancelAddMonoidLexFinsupp, QuadraticMap.sum_polar_sub_repr_sq, MvPolynomial.scalarRTensor_apply_monomial_tmul, Module.basisUnique_repr_eq_zero_iff, finsuppTensorFinsupp_apply, Representation.ofMulActionSelfAsModuleEquiv_symm_apply, Rep.diagonalSuccIsoFree_inv_hom_single, PolynomialModule.smul_def, IsBaseChange.finsuppPow, lmapDomain_id, NumberField.Units.fun_eq_repr, 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, IsAdjoinRootMonic.coeff_apply, Module.Relations.Solution.surjective_Ď_iff_span_eq_top, supportedEquivFinsupp_symm_single, Rep.coindToInd_of_support_subset_orbit, Representation.finsupp_apply, LinearMap.toMatrix_apply', mapRange.linearEquiv_toAddEquiv, groupHomology.mapCyclesâ_comp_apply, Rep.leftRegularHom_hom, Matrix.repr_toLin, MvPowerSeries.coeff_pow, KaehlerDifferential.mvPolynomialBasis_repr_D_X, multiset_sum_sum_index, linearCombination_id_surjective, TensorProduct.sum_tmul_basis_right_injective, isOrderedAddMonoid, rank_finsupp, LinearIndependent.linearCombination_repr, exteriorPower.basis_repr_ne, Algebra.Presentation.differentials.commââ, rank_finsupp_self, Representation.ofCoinvariantsTprodLeftRegular_mk_tmul_single, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_left, Module.Basis.mk_repr, Module.Flat.finsupp, MvPolynomial.monomial_finsupp_sum_index, Module.Relations.Solution.injective_fromQuotient_iff_ker_Ď_eq_span, linearEquivFunOnFinite_symm_coe, Module.Basis.repr_isUnitSMul, Span.repr_def, groupHomology.mem_cyclesâ_iff, coe_ceilDiv_def, groupHomology.cyclesMap_comp_isoCyclesâ_hom, linearIndependent_iff_injective_finsuppLinearCombination, MvPolynomial.scalarRTensor_apply_X_tmul_apply, groupHomology.mapCyclesâ_comp_assoc, Module.Basis.prod_repr_inl, groupHomology.toCycles_comp_isoCyclesâ_hom_assoc, Module.Relations.Solution.surjective_fromQuotient_iff_surjective_Ď, linearCombination_zero_apply, mem_supported, Module.Basis.repr_self_apply, mem_span_iff_linearCombination, IsLocalFrameOn.coeff_apply_of_mem, setBasisOfLinearIndependentOfCardEqFinrank_repr_apply, Algebra.Presentation.differentials.homâ_single, Rep.diagonalSuccIsoTensorTrivial_inv_hom_single_right, LinearMap.sum_repr_mul_repr_mulââ, Representation.ofMulAction_apply, Colex.isOrderedCancelAddMonoid, 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, finsuppTensorFinsupp'_symm_single_eq_tmul_single_one, Rep.finsuppToCoinvariantsTensorFree_single, Module.Relations.Solution.IsPresentation.linearEquiv_symm_var, Rep.coinvariantsTensorFreeLEquiv_symm_apply, linearIndependent_iff_ker, SkewMonoidAlgebra.ofFinsupp_sum, Pi.counit_comp_finsuppLcoeFun, curryLinearEquiv_symm_apply_apply, llift_apply, linearCombination_smul, groupHomology.cyclesâ_eq_top_of_isTrivial, AddCommMonCat.free_map, Ideal.finsuppTotal_apply, TensorProduct.equivFinsuppOfBasisLeft_apply_tmul_apply, lmapDomain_linearCombination, range_mapRange_linearMap, Module.Basis.repr_algebraMap, Multiset.support_sum_subset, Algebra.Generators.cotangentSpaceBasis_repr_one_tmul, iInf_ker_lapply_le_bot, Rep.coindFunctorIso_hom_app_hom_hom_apply_hom_hom_apply, 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, LinearEquiv.finsuppUnique_symm_apply, span_le_supported_biUnion_support, LinearMap.BilinForm.apply_eq_dotProduct_toMatrix_mulVec, KaehlerDifferential.kerTotal_eq, span_image_eq_map_linearCombination, 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', 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, Module.Basis.ofEquivFun_repr_apply, supported_univ, Module.Basis.sumQuot_repr_left, groupHomology.mapCyclesâ_comp, Representation.ofMulAction_self_smul_eq_mul, Module.Basis.reindexRange_repr', Module.Basis.reindexRange_repr, sigmaFinsuppLEquivPiFinsupp_symm_apply, TensorProduct.equivFinsuppOfBasisLeft_apply_tmul, PiTensorProduct.ofFinsuppEquiv'_tprod_single, TensorProduct.equivFinsuppOfBasisLeft_symm, Submodule.mulLeftMap_apply, TensorProduct.finsuppScalarRight_apply, Module.Relations.Solution.ofQuotient_var, groupHomology.mapCyclesâ_comp_i, TensorProduct.finsuppScalarRight_apply_tmul, Polynomial.derivativeFinsupp_apply_toFun, 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, lcoeFun_comp_lsingle, Finset.sum_apply', isOrderedCancelAddMonoid, lcoeFun_apply, basisOfLinearIndependentOfCardEqFinrank_repr_apply, PiTensorProduct.ofFinsuppEquiv_tprod_single, Module.Relations.range_map, Module.Basis.SmithNormalForm.repr_apply_embedding_eq_repr_smul, groupHomology.single_one_fst_sub_single_one_snd_mem_boundariesâ, floorDiv_apply, Representation.coinvariantsTprodLeftRegularLEquiv_apply, finsuppTensorFinsuppLid_symm_single_smul, ker_mapRange, 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, Module.Basis.addSubgroupOfClosure_repr_apply, sumFinsuppLEquivProdFinsupp_symm_apply, Module.Basis.repr_range, basis_toMatrix_basisFun_mul, instFinitePresentationFinsupp, 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, linearCombination_linear_comp, groupHomology.mapCyclesâ_comp_i, Module.Basis.repr_eq_iff, mem_submodule_iff, Module.Basis.sumQuot_repr_inl, groupHomology.boundariesOfIsBoundaryâ_coe, IsBaseChange.of_basis, Algebra.Generators.cotangentSpaceBasis_repr_tmul, comul_comp_lapply, Algebra.TensorProduct.equivFinsuppOfBasis_apply, sumFinsuppLEquivProdFinsupp_symm_inl, Module.Basis.repr_linearCombination, ceilDiv_apply, Algebra.TensorProduct.equivFinsuppOfBasis_symm_apply, MvPolynomial.rTensor_apply_X_tmul, PiLp.basisFun_repr, Algebra.Generators.H1Cotangent.δAux_toAlgHom, linearCombination_single_index, groupHomology.single_one_fst_sub_single_one_fst_mem_boundariesâ, lift_apply, LinearIndependent.linearCombinationEquiv_apply_coe, Module.Relations.Solution.range_Ď, TensorProduct.equivFinsuppOfBasisRight_apply_tmul_apply, subtypeDomain_finsupp_sum, groupHomology.mapCyclesâ_id_comp_apply, LinearIndependent.linearCombination_comp_repr, Polynomial.derivativeFinsupp_apply_apply, Algebra.SubmersivePresentation.sectionCotangent_eq_iff, 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, sum_sum_index', Rep.indResAdjunction_counit_app_hom_hom, Module.Basis.equivFunL_symm_apply_repr, PowerBasis.repr_gen_pow_isIntegral, Rep.coindToInd_apply, groupHomology.mapCyclesâ_comp_i_apply, Polynomial.derivativeFinsupp_derivative, 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, counit_comp_lsingle, TensorProduct.finsuppScalarRight_smul, groupHomology.coe_mapCyclesâ, finsuppTensorFinsupp_single, groupHomology.H1Ď_comp_map_apply, Nat.ceilRoot_def, Module.Basis.repr_reindex, support_sum, Module.subsingletonEquiv_symm_apply, IsLocalizedModule.map_linearCombination, rank_finsupp_self', Module.Basis.algebraMapCoeffs_repr_apply_toFun, 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, Module.Basis.repr_symm_single, Representation.finsuppToCoinvariants_single_mk, groupHomology.H2Ď_comp_map_assoc, apply_eq_dotProduct_toMatrixâ_mulVec, TensorProduct.finsuppLeft_apply, MvPolynomial.irreducible_sumSMulX, support_ceilDiv_subset, finsuppTensorFinsuppRid_symm_single_smul, finsetBasisOfTopLeSpanOfCardEqFinrank_repr_apply, Module.Basis.restrictScalars_repr_apply, Orthonormal.inner_finsupp_eq_sum_right, Representation.finsupp_single, span_eq_range_linearCombination, Module.Basis.equivFunL_apply, isCompl_range_lmapDomain_span, Algebra.Generators.cotangentRestrict_bijective_of_isCompl, MvPolynomial.combinatorial_nullstellensatz_exists_linearCombination, Module.Relations.map_single, MvPolynomial.rTensorAlgHom_toLinearMap, Rep.finsuppTensorRight_hom_hom, MvPolynomial.coeff_sumSMulX, 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, LinearMap.toMatrix_transpose_apply, Pi.basis_repr, 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, Module.Basis.toDual_eq_repr, Module.Basis.sum_repr_mul_repr, linearCombination_apply, Nat.factorization_ceilRoot, Subalgebra.LinearDisjoint.mulRightMap_ker_eq_bot_iff_linearIndependent, NumberField.integralBasis_repr_apply, groupHomology.H2Ď_eq_iff, Submodule.mulRightMap_eq_mulMap_comp, Module.Basis.linearMap_repr_apply, groupHomology.H1AddEquivOfIsTrivial_single, MultilinearMap.freeFinsuppEquiv_def, groupHomology.isoCyclesâ_hom_comp_i_apply, linearCombination_embDomain, Representation.ofMulActionSelfAsModuleEquiv_apply, KaehlerDifferential.kerTotal_map, PiTensorProduct.ofFinsuppEquiv_apply, MvPolynomial.support_esymm', TensorProduct.finsuppScalarRight_symm_apply_single, groupHomology.cyclesMap_comp_isoCyclesâ_hom_assoc, Module.Basis.mem_span_image, LinearMap.CompatibleSMul.finsupp_cod, NumberField.mixedEmbedding.stdBasis_apply_isComplex_fst, Module.Basis.localizationLocalization_repr_algebraMap, groupHomology.inhomogeneousChains.d_single, Module.Basis.dualBasis_apply, apply_eq_star_dotProduct_toMatrixâ_mulVec, Complex.coe_basisOneI_repr, linearCombination_single, Module.Presentation.CokernelData.Ď_lift, Module.Basis.reindexFinsetRange_repr_self, Orthonormal.inner_right_finsupp, LinearMap.toMatrix_transpose_apply', Module.Basis.repr_symm_single_one, groupHomology.isBoundaryâ_iff, coe_basis, mapRange.linearEquiv_toLinearMap, 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, restrictDom_comp_subtype, lsum_apply, Basis.multilinearMap_apply_apply, Rep.standardComplex.d_of, Module.Basis.coe_finTwoProd_repr, linearCombination_unique, groupHomology.toCycles_comp_isoCyclesâ_hom, coe_lsum, groupHomology.cyclesMap_comp_isoCyclesâ_hom_apply, linearCombination_mapDomain, Span.finsupp_linearCombination_repr, groupHomology.mapCyclesâ_id_comp, lapply_comp_lsingle_same, instIsCocomm, IsAdjoinRootMonic.coeff_apply_lt, DirectSum.IsInternal.collectedBasis_repr_of_mem_ne, Module.Basis.toMatrix_apply, KaehlerDifferential.mvPolynomialBasis_repr_apply, LinearMap.exists_finsupp_nat_of_prod_injective, sigmaFinsuppLEquivPiFinsupp_apply, Rep.diagonalSuccIsoTensorTrivial_hom_hom_single, finsuppTensorFinsuppRid_single_tmul_single, LinearIndependent.linearCombinationEquiv_symm_apply, Module.DualBases.basis_repr_apply, LieAlgebra.LoopAlgebra.toFinsupp_single_tmul, Algebra.toMatrix_lmul', Module.Relations.Solution.isPresentation_iff, Polynomial.derivativeFinsupp_map, disjoint_supported_supported, llift_symm_apply, TensorProduct.finsuppScalarLeft_apply_tmul_apply, groupHomology.isoCyclesâ_hom_comp_i_apply, Module.Basis.symmetricAlgebra_repr_apply, supportedEquivFinsupp_symm_apply_coe_support_val, ZLattice.exists_forall_abs_repr_le_norm, Matrix.toLin_apply, mapDomain_finset_sum, MultilinearMap.freeFinsuppEquiv_apply, linearCombination_range, Submodule.mulRightMap_apply, finsuppLEquivDirectSum_single, 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, mapRange.linearMap_comp, support_floorDiv_subset, linearCombination_restrict, Algebra.Presentation.differentials.commââ, Module.Basis.sumQuot_repr_inr_of_mem, coe_basisSingleOne, coe_lmapDomain, indicator_eq_sum_attach_single, lapply_comp_lsingle_of_ne, groupHomology.cyclesOfIsCycleâ_coe, Module.Basis.repr_injective, LinearIndependent.repr_range, Module.Basis.repr_apply_eq, MvPolynomial.monomial_sum_index, linearCombination_comp, LinearMap.polyCharpolyAux_map_aeval, Pi.counit_coe_finsupp, groupHomology.dââ_apply_mem_cyclesâ, NumberField.inverse_basisMatrix_mulVec_eq_repr, range_linearCombination, supported_empty, 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, linearIndependent_single_iff, MultilinearMap.freeFinsuppEquiv_single, Module.Basis.end_repr_symm_apply, InnerProductSpace.toMatrix_rankOne, MvPolynomial.rTensor_symm_apply_single, Representation.free_single_single, lcongr_symm_single, Module.Basis.apply_eq_iff, Module.Flat.iff_forall_exists_factorization, sigmaFinsuppLequivDFinsupp_symm_apply, Module.Relations.Solution.Ď_comp_map, domLCongr_symm, Rep.finsuppTensorRight_inv_hom, setBasisOfTopLeSpanOfCardEqFinrank_repr_apply, LinearMap.polyCharpolyAux_coeff_eval, MonomialOrder.degree_prod_le, 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, 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, lcongr_single, Module.Flat.exists_factorization_of_apply_eq_zero_of_free, Matrix.toLinearMapâ_apply, linearEquivFunOnFinite_apply, ZLattice.abs_repr_lt_of_norm_lt, groupHomology.cyclesMkâ_eq, LieAlgebra.LoopAlgebra.residuePairing_apply_apply, MvPolynomial.rTensor_apply_monomial_tmul, Algebra.Generators.repr_CotangentSpaceMap, Module.Basis.dualBasis_repr, groupHomology.H1Ď_eq_zero_iff, groupHomology.isoCyclesâ_inv_comp_iCycles_assoc, sumFinsuppLEquivProdFinsupp_symm_inr, groupHomology.Ď_comp_H1Iso_hom_assoc, Pi.comul_coe_finsupp, supported_mono, groupHomology.H2Ď_comp_map, NumberField.mixedEmbedding.stdBasis_apply_isReal, HahnSeries.coeff_toMvPowerSeries_symm, Module.Basis.linearCombination_repr, union_support_maximal_linearIndependent_eq_range_basis, Module.FinitePresentation.out, Nat.factorization_floorRoot, Module.Basis.linearCombination_coord, Representation.FiniteCyclicGroup.coinvariantsKer_leftRegular_eq_ker, coe_floorDiv, Module.Basis.tensorAlgebra_repr_apply, Nat.floorRoot_def, Module.projective_def', groupHomology.H1Ď_comp_map_assoc, Representation.coinvariantsTprodLeftRegularLEquiv_symm_apply, Module.Basis.equivFun_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, Rep.finsuppTensorLeft_inv_hom, LinearMap.snd_prodOfFinsuppNat, LinearEquiv.finsuppUnique_apply, linearCombination_fin_zero, Module.Relations.Solution.Ď_relation, exteriorPower.basis_repr_apply, linearEquivFunOnFinite_symm_single, Module.Basis.toMatrix_update, PiLp.basis_toMatrix_basisFun_mul, single_multiset_sum, groupHomology.single_one_snd_sub_single_one_snd_mem_boundariesâ, linearCombination_equivMapDomain, mapRange.linearEquiv_apply, Multiset.support_sum_eq, groupHomology.instEpiModuleCatH2Ď, Module.Basis.baseChange_repr_tmul, ZSpan.repr_fract_apply, finsuppLEquivDirectSum_apply, Rep.leftRegularTensorTrivialIsoFree_inv_hom, Algebra.TensorProduct.basis_repr_symm_apply, LinearMap.polyCharpoly_map_eq_charpoly, Submodule.mulLeftMap_apply_single, single_mem_span_single, KaehlerDifferential.quotKerTotalEquiv_symm_apply, finsuppTensorFinsuppLid_apply_apply, LinearIndependent.repr_ker, groupHomology.H1Ď_comp_map, groupHomology.chainsMap_f_hom, groupHomology.dââ_apply_mem_cyclesâ, mapRange.linearMap_toAddMonoidHom, QuaternionAlgebra.coe_basisOneIJK_repr, Ideal.range_finsuppTotal, Lex.isOrderedCancelAddMonoid, groupHomology.boundariesOfIsBoundaryâ_coe, groupHomology.cyclesMkâ_eq, finsuppLequivDFinsupp_apply_apply, liftAddHom_singleAddHom, MvPolynomial.esymm_eq_sum_monomial, groupHomology.mapCyclesâ_comp_i_assoc, toMultiset_sum, domLCongr_apply, Rep.linearization_δ_hom, curryLinearEquiv_apply, QuadraticMap.apply_linearCombination', Finset.support_sum_eq, groupHomology.mapCyclesâ_id_comp_apply, finsuppTensorFinsupp_symm_single, linearCombination_linearCombination, Module.Relations.Solution.IsPresentation.desc_comp_Ď, lift_symm_apply, groupHomology.H2Ď_comp_map_apply, NumberField.mixedEmbedding.latticeBasis_repr_apply, Module.Basis.ext_elem_iff, KaehlerDifferential.mvPolynomialBasis_repr_D, HahnSeries.coeff_toMvPowerSeries, Rep.FiniteCyclicGroup.homResolutionIso_inv_f_hom_apply_hom_hom_apply, finsuppTensorFinsuppRid_apply_apply, Module.Basis.repr_sum_self, RootPairing.Base.toWeightBasis_repr_root, Rep.finsuppTensorLeft_hom_hom, linearCombination_option, Polynomial.derivativeFinsupp_one, Algebra.leftMulMatrix_mulVec_repr, 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, Algebra.Generators.cotangentRestrict_mk, supportedEquivFinsupp_apply_support_val, finsuppLequivDFinsupp_symm_apply, lsum_comp_lsingle, Algebra.Generators.cotangentRestrict_bijective_of_basis_kaehlerDifferential, TensorProduct.finsuppRight_symm_apply_single, DegLex.instIsOrderedCancelAddMonoidDegLexNat, Module.Basis.linearMap_repr_symm_apply, KaehlerDifferential.mvPolynomialBasis_repr_comp_D, finsuppTensorFinsuppLid_single_tmul_single, Rep.indMap_hom, groupHomology.isoCyclesâ_hom_comp_i_assoc, isArtinian_finsupp, span_range_eq_top_iff_surjective_finsuppLinearCombination, prod_sum_index, mapDomain_sum, Representation.leftRegular_norm_apply, 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, MvPolynomial.support_esymm'', TensorProduct.finsuppLeft_apply_tmul, PiTensorProduct.ofFinsuppEquiv'_apply_apply, LinearMap.toMatrix_toSpanSingleton, linearDepOn_iffâ, Representation.coinvariantsFinsuppLEquiv_symm_apply, Module.finrank_finsupp_self, Polynomial.support_derivativeFinsupp_subset_range, TensorProduct.equivFinsuppOfBasisRight_symm, exteriorPower.basis_repr, groupHomology.Ď_comp_H2Iso_hom_apply, indicator_eq_sum_single, Module.Relations.Solution.span_relation_le_ker_Ď, MonomialOrder.degree_prod, IsBaseChange.basis_repr_comp, mapRange.linearEquiv_trans, OrthonormalBasis.coe_toBasis_repr_apply, mapDomain.toLinearMap_linearEquiv, Rep.coinvariantsTensorIndHom_mk_tmul_indVMk, ZLattice.normBound_spec, QuadraticMap.apply_linearCombination, groupHomology.mapCyclesâ_hom, groupHomology.isoCyclesâ_inv_comp_iCycles, AdjoinRoot.powerBasisAux'_repr_apply_to_fun, IsAdjoinRootMonic.coeff_apply_coe, Module.Basis.mapCoeffs_repr, Module.Basis.traceDual_repr_apply, groupHomology.cyclesMap_comp_isoCyclesâ_hom_assoc, linearIndependent_single, 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, moduleIsTorsionFree, Module.Basis.ofZLatticeComap_repr_apply, Module.projective_def, coe_univ_sum_single, HahnSeries.toMvPowerSeries_apply, Module.End.ringEquivEndFinsupp_apply_apply_support, groupHomology.mapCyclesâ_comp_i_apply, Module.annihilator_finsupp, 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', Rep.freeLift_hom, groupHomology.isoCyclesâ_hom_comp_i, 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, LinearMap.toMatrixAlgEquiv_apply', MonomialOrder.div, 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, Rep.leftRegularTensorTrivialIsoFree_hom_hom_single_tmul_single, groupHomology.single_one_mem_boundariesâ, single_sum, linearCombination_comp_lmapDomain, mem_span_image_iff_linearCombination, MvPolynomial.irreducible_sumSMulXSMulY, sum_apply, BilinForm.apply_eq_dotProduct_toMatrix_mulVec, Module.Relations.toQuotient_map, mapDomain.linearEquiv_symm, Module.Basis.constr_def, comul_comp_lsingle, groupHomology.cyclesâIsoOfIsTrivial_inv_apply, coe_sum, Module.Basis.toDual_apply_left, QuadraticMap.sum_repr_sq_add_sum_repr_mul_polar, MvPolynomial.rTensor_apply, Module.DualBases.lc_def, groupHomology.isoCyclesâ_hom_comp_i, Module.Relations.Solution.IsPresentation.exact, NumberField.canonicalEmbedding_eq_basisMatrix_mulVec, Module.Basis.reindexFinsetRange_repr, Module.Basis.continuous_coe_repr, TensorProduct.finsuppScalarLeft_apply, Module.Basis.smulTower_repr, Module.Basis.toDual_apply_right, groupHomology.single_inv_Ď_self_add_single_mem_boundariesâ, linearCombination_comapDomain, ZSpan.repr_floor_apply, Module.Basis.repr_symm_apply, apply_linearCombination_id, Module.Basis.tensorProduct_repr_tmul_apply, Representation.free_asModule_free, Basis.piTensorProduct_repr_tprod_apply, Module.Relations.Solution.Ď_comp_map_apply, groupHomology.single_mem_cyclesâ_iff, TensorProduct.finsuppScalarLeft_symm_apply_single, Module.Basis.repr_smul', 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, Module.Basis.constr_apply, Module.Finite.finsupp, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_inv_f_hom_apply, linearCombination_eq_fintype_linearCombination_apply, Subalgebra.LinearDisjoint.basisOfBasisLeft_repr_apply, disjoint_supported_supported_iff, MonomialOrder.degree_prod_of_regular, mem_finsuppAffineCoords_iff_linearCombination, 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, mapRange_finset_sum, Module.Basis.norm_repr_le_norm, 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, 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, TensorProduct.equivFinsuppOfBasisRight_symm_apply, Module.Basis.algebraMapCoeffs_repr, toMultiset_sum_single, Nat.factorization_prod, Module.Basis.coord_apply, 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, KaehlerDifferential.kerTotal_map', Rep.leftRegularTensorTrivialIsoFree_hom_hom, Rep.barComplex.d_single, domLCongr_refl, LinearMap.toMatrixAlgEquiv_transpose_apply, mapRange_multiset_sum, Module.Basis.repr_self, TensorProduct.finsuppRight_apply_tmul_apply, linearCombination_zero, TensorProduct.finsuppRight_apply_tmul, Module.subsingletonEquiv_apply, groupHomology.isBoundaryâ_iff, Polynomial.degreeLT.basis_repr, Module.Basis.repr_reindex_apply, groupHomology.mapCyclesâ_quotientGroupMk'_epi, groupHomology.mapCyclesâ_comp_i_assoc, LinearMap.toMatrix_apply, linearDepOn_iff'â, NumberField.house.basis_repr_norm_le_const_mul_house, Rep.coinvariantsTensorFreeToFinsupp_mk_tmul_single, linearIndependent_single_one, LinearMap.map_finsupp_linearCombination, Rep.FiniteCyclicGroup.leftRegular.range_applyAsHom_sub_eq_ker_linearCombination, range_restrictDom, LinearMap.toMatrixAlgEquiv_transpose_apply', Module.Relations.Solution.Ď_single, lmapDomain_apply, linearIndepOn_iff_linearCombinationOnâ, SkewMonoidAlgebra.toFinsupp_sum', domLCongr_single, groupHomology.mem_cyclesâ_iff, sum_sum_index, TensorProduct.coe_finsuppScalarRight', LinearMap.polyCharpoly_coeff_eval, lsum_comp_mapRange_toSpanSingleton, Module.Basis.repr_unop_eq_mulOpposite_repr, groupHomology.boundariesToCyclesâ_apply, groupHomology.single_mem_cyclesâ_iff_inv, linearIndepOn_iff_linearCombinationOn, 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, Rep.indResHomEquiv_symm_apply_hom, groupHomology.isoCyclesâ_hom_comp_i_assoc, Polynomial.derivativeFinsupp_X, finsuppLEquivDirectSum_symm_lof, Module.Flat.exists_factorization_of_isFinitelyPresented, 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, MvPowerSeries.prod_monomial, Rep.leftRegularTensorTrivialIsoFree_inv_hom_single_single, ZLattice.abs_repr_le, DirectSum.IsInternal.collectedBasis_repr_of_mem, Module.Basis.coe_sumCoords, iSup_lsingle_range, LinearMap.sum_repr_mul_repr_mul, mem_supported', lmapDomain_supported, Module.Basis.ofIsLocalizedModule_repr_apply, Rep.linearization_Îź_hom, Module.Relations.Solution.ofQuotient_Ď, Rep.FiniteCyclicGroup.coinvariantsTensorResolutionIso_hom_f_hom_apply, groupHomology.H1Ď_eq_iff, LinearMap.fst_prodOfFinsuppNat, TensorProduct.finsuppLeft_apply_tmul_apply, LinearMap.polyCharpolyAux_map_eq_toMatrix_charpoly, Representation.ofMulAction_def, groupHomology.cyclesMap_comp_isoCyclesâ_hom, sigmaFinsuppLequivDFinsupp_apply, MvPolynomial.rTensorAlgHom_apply_eq
|
instAddGroup đ | CompOp | 1 mathmath: mem_finsuppAffineCoords_iff_linearCombination
|
instAddMonoid đ | CompOp | 11 mathmath: antidiagonal_single, MvPowerSeries.coeff_inv, MvPowerSeries.coeff_inv_aux, sum_antidiagonal_swap, antidiagonal_zero, instIsAddTorsionFree, MvPowerSeries.coeff_invOfUnit, distribMulActionHom_ext'_iff, prod_antidiagonal_swap, MvPolynomial.coeff_mul, MvPowerSeries.coeff_mul
|
instAddZeroClass đ | CompOp | 134 mathmath: sum_toMultiset, finite_of_degree_le, mulHom_ext'_iff, degree_eq_sum, MvPowerSeries.weightedOrder_monomial, MvPolynomial.degrees_monomial, mapDomain.addMonoidHom_comp, toMultiset_strictMono, MvPolynomial.weightedDegree_eq_zero_iff, singleAddHom_apply, FreeAbelianGroup.toFinsupp_toFreeAbelianGroup, weight_single_one_apply, mapDomain_comapDomain_nat_add_one, sigmaFinsuppAddEquivDFinsupp_apply, prod_toMultiset, toMultiset_zero, le_weight_of_ne_zero', MvPolynomial.le_weightedTotalDegree, toMultiset_toFinsupp, MvPolynomial.pow_idealOfVars, MvPolynomial.idealOfVars_eq_restrictSupportIdeal, coeFnAddHom_apply, MvPolynomial.totalDegree_eq, mapRange.addMonoidHom_apply, MvPolynomial.mem_pow_idealOfVars_iff, MvPolynomial.degrees_def, sigmaFinsuppAddEquivDFinsupp_symm_apply, Module.End.ringHomEndFinsupp_apply_apply, liftAddHom_comp_single, card_toMultiset, Sym.coe_equivNatSum_symm_apply, MvPowerSeries.weightedOrder_monomial_of_ne_zero, toMultiset_apply, sigmaFinsuppEquivDFinsupp_add, weight_single, toFreeAbelianGroup_comp_singleAddHom, MvPolynomial.monomialOneHom_apply, MvPolynomial.coeff_homogeneousComponent, FreeAbelianGroup.equivFinsupp_symm_apply, comp_liftAddHom, MvPolynomial.pow_idealOfVars_eq_span, mapRange.addMonoidHom_toZeroHom, MvPolynomial.weightedHomogeneousSubmodule_eq_finsupp_supported, MvPowerSeries.coeff_homogeneousComponent, degree_apply, FreeAbelianGroup.toFinsupp_comp_toFreeAbelianGroup, toFreeAbelianGroup_single, finite_of_nat_weight_le, le_degree, MvPolynomial.degree_degLexDegree, le_weight, mem_toMultiset, coe_curryAddEquiv, MvPolynomial.monomial_mem_pow_idealOfVars_iff, MvPowerSeries.le_weightedOrder_subst, count_toMultiset, FreeAbelianGroup.toFinsupp_of, weight_single_index, degree_preimage_add, liftAddHom_apply, DegLex.lt_iff, MvPowerSeries.coeff_weightedHomogeneousComponent, MvPowerSeries.order_le, degLex_def, mapRange.addMonoidHom_comp, toMultiset_add, Multiset.toFinsupp_symm_apply, FreeAbelianGroup.equivFinsupp_apply, MvPowerSeries.exists_coeff_ne_zero_and_order, MvPolynomial.homogeneousComponent_apply, addHom_ext'_iff, toFreeAbelianGroup_toFinsupp, MvPowerSeries.weightedOrder_eq_nat, MvPowerSeries.totalDegree_trunc', sigmaFinsuppLequivDFinsupp_symm_apply, MvPolynomial.monomial_mem_homogeneousSubmodule_pow_degree, Multiset.toFinsupp_toMultiset, degree_preimage_nsmul, MvPowerSeries.exists_coeff_ne_zero_and_weightedOrder, add_closure_setOf_eq_single, mapRange.addEquiv_toAddMonoidHom, MvPowerSeries.weightedOrder_le, LinearMap.snd_prodOfFinsuppNat, toFinset_toMultiset, degree_single, applyAddHom_apply, MvPolynomial.weightedDecomposition.decompose'_eq, le_weight_of_ne_zero, Multiset.toFinsupp_eq_iff, mapDomain.addMonoidHom_apply, MvPolynomial.homogeneousSubmodule_eq_finsupp_supported, liftAddHom_singleAddHom, toMultiset_sum, range_single_one, MvPowerSeries.order_monomial, MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_weight, liftAddHom_apply_single, mapDomain.addMonoidHom_id, embDomain.addMonoidHom_apply, weight_sub_single_add, MvPolynomial.degrees_monomial_eq, liftAddHom_symm_apply_apply, DegLex.le_iff, curryAddEquiv_symm_apply, liftAddHom_symm_apply, degree_eq_zero_iff, toMultiset_single, comapDomain.addMonoidHom_apply, MvPowerSeries.order_eq_nat, MvPowerSeries.ne_zero_iff_exists_coeff_ne_zero_and_degree, MvPolynomial.coeff_weightedHomogeneousComponent, degree_mono, eraseAddHom_apply, toMultiset_sup, DegLex.monotone_degree, mapDomain.addMonoidHom_comp_mapRange, nsmul_single_one_image, DegLex.lt_def, MvPowerSeries.order_monomial_of_ne_zero, toMultiset_sum_single, weight_eq_zero_iff_eq_zero, toMultiset_map, Rep.barComplex.d_single, mapRange.addMonoidHom_id, toMultiset_inf, weight_apply, degree_def, MvPolynomial.weightedHomogeneousComponent_apply, coe_orderIsoMultiset, toFreeAbelianGroup_comp_toFinsupp, toMultiset_eq_iff, MvPolynomial.decomposition.decompose'_eq, image_pow_eq_finsuppProd_image, sigmaFinsuppLequivDFinsupp_apply
|
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 | 17 mathmath: coe_neg, neLocus_neg, neLocus_neg_neg, mapRange_neg, subtypeDomain_neg, filter_neg, mapRange_neg', sum_neg_index, erase_neg, SkewMonoidAlgebra.toFinsupp_neg, SkewMonoidAlgebra.ofFinsupp_neg, prod_neg_index, toDFinsupp_neg, neg_apply, support_neg, single_neg, DFinsupp.toFinsupp_neg
|
instSub đ | CompOp | 40 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â, sum_sub_index, mapRange_sub', DFinsupp.toFinsupp_sub, single_sub, groupHomology.single_one_fst_sub_single_one_snd_mem_boundariesâ, 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, Module.Presentation.tautologicalRelations_relation, neLocus_self_sub_right, Module.Presentation.tautological_relation, exteriorPower.presentation.relations_relation, groupHomology.isBoundaryâ_iff, 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
|