-
Notifications
You must be signed in to change notification settings - Fork 1
All issues
Issue creation is restricted in this repository
Issues
is:issue state:open
is:issue state:open
Search results
decompose: remove maxHeartbeats from PadicLFunctions.seriesEval_mul
lane:decomposeWorker lane: /decompose-proof (helpers; auto-merge)Worker lane: /decompose-proof (helpers; auto-merge)state:todoTicket open, unclaimedTicket open, unclaimedStatus: Open.#8534 In CBirkbeck/AINTLIB;decompose-proof: BernoulliRegular/Reflection/Local/ComponentDimension/CharacterProjectionFinrankOne.lean::completedPrincipalUnitModPEigenspace_mem_filtration_succ_of_exists_pow_ne@L112
lane:decomposeWorker lane: /decompose-proof (helpers; auto-merge)Worker lane: /decompose-proof (helpers; auto-merge)state:todoTicket open, unclaimedTicket open, unclaimedStatus: Open.#8366 In CBirkbeck/AINTLIB;decompose-proof: HasseWeil/Foundation/EC/TranslateValuation.lean::pointValuation_translateAlgEquivOfPoint_of_le_one@L1396
lane:decomposeWorker lane: /decompose-proof (helpers; auto-merge)Worker lane: /decompose-proof (helpers; auto-merge)state:todoTicket open, unclaimedTicket open, unclaimedStatus: Open.#8364 In CBirkbeck/AINTLIB;decompose-proof: HasseWeil/Foundation/EC/MulByIntUnramified.lean::ord_P_mulByInt_y_sub_const_eq_one@L1050
lane:decomposeWorker lane: /decompose-proof (helpers; auto-merge)Worker lane: /decompose-proof (helpers; auto-merge)state:todoTicket open, unclaimedTicket open, unclaimedStatus: Open.#8363 In CBirkbeck/AINTLIB;decompose-proof: DedekindResidue/MainTheorem.lean::zero_sum_le_sq@L47
lane:decomposeWorker lane: /decompose-proof (helpers; auto-merge)Worker lane: /decompose-proof (helpers; auto-merge)state:todoTicket open, unclaimedTicket open, unclaimedStatus: Open.#8361 In CBirkbeck/AINTLIB;decompose-proof: WronskianAux::wronskian_aux_four — fit default maxHeartbeats via the quotient-ring route (from #7205)
lane:decomposeWorker lane: /decompose-proof (helpers; auto-merge)Worker lane: /decompose-proof (helpers; auto-merge)state:todoTicket open, unclaimedTicket open, unclaimedStatus: Open.#8329 In CBirkbeck/AINTLIB;decompose-proof: BernoulliRegular/Reflection/WeakSplitting/UniformResidueDegree.lean::idealNormMultiplicity_prime_pow_mul_d_eq_card_sym_of_uniform@L217
lane:decomposeWorker lane: /decompose-proof (helpers; auto-merge)Worker lane: /decompose-proof (helpers; auto-merge)state:todoTicket open, unclaimedTicket open, unclaimedStatus: Open.#8291 In CBirkbeck/AINTLIB;decompose-proof: BernoulliRegular/Reflection/WeakSplitting/MultiGeometric.lean::norm_summable_and_prod_eq@L117
lane:decomposeWorker lane: /decompose-proof (helpers; auto-merge)Worker lane: /decompose-proof (helpers; auto-merge)state:todoTicket open, unclaimedTicket open, unclaimedStatus: Open.#8289 In CBirkbeck/AINTLIB;decompose-proof: BernoulliRegular/Reflection/SingularKummer/LocalizationKernel/LocalToCompletedBridge.lean::fieldUnitToCyclotomicLocalUnitPowerQuotient_equivariant_generator@L704
lane:decomposeWorker lane: /decompose-proof (helpers; auto-merge)Worker lane: /decompose-proof (helpers; auto-merge)state:todoTicket open, unclaimedTicket open, unclaimedStatus: Open.#8287 In CBirkbeck/AINTLIB;decompose-proof: BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/PrincipalUnitFactor/ConjNormSemiPrimaryAndUnitFactorData.lean::dvd_exponent_of_neg_one_pow_mul_zeta_pow_isSemiPrimary@L323
lane:decomposeWorker lane: /decompose-proof (helpers; auto-merge)Worker lane: /decompose-proof (helpers; auto-merge)state:todoTicket open, unclaimedTicket open, unclaimedStatus: Open.#8278 In CBirkbeck/AINTLIB;decompose-proof: BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/KummerFurtwaengler/StickelbergerIdealOrbit.lean::pthSymbolAtPrime_galoisAction_exists_unit@L314
lane:decomposeWorker lane: /decompose-proof (helpers; auto-merge)Worker lane: /decompose-proof (helpers; auto-merge)state:todoTicket open, unclaimedTicket open, unclaimedStatus: Open.#8275 In CBirkbeck/AINTLIB;decompose-proof: BernoulliRegular/Reflection/ResidueSymbol/Furtwaengler/IrelandRosen/Theorem1/CanonicalPrimeSourceData.lean::residueCharInt_eq_teichUnitFullOfRootsOfUnityBijective_pow_d@L363
lane:decomposeWorker lane: /decompose-proof (helpers; auto-merge)Worker lane: /decompose-proof (helpers; auto-merge)state:todoTicket open, unclaimedTicket open, unclaimedStatus: Open.#8274 In CBirkbeck/AINTLIB;