commRing 📖 | CompOp | 608 mathmath: exists_sq_eq_prime_iff_of_mod_four_eq_one, NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply', legendreSym.eq_neg_one_iff, addOrderOf_coe, intCast_eq_intCast_iff_dvd_sub, Submodule.toAddSubgroup_toZModSubmodule, isUnit_iff_coprime, DirichletCharacter.changeLevel_injective, LucasLehmer.X.fst_natCast, DihedralGroup.r_one_zpow, isCyclic_units_iff_of_odd, wittPolynomial_zmod_self, EisensteinSeries.gammaSet_div_gcd_to_gammaSet10_bijection, pow_card_sub_one, χ₈'_int_eq_if_mod_eight, QuaternionGroup.a_one_pow_n, unitsMap_surjective, Int.quotientSpanEquivZMod_comp_Quotient_mk, modularCyclotomicCharacter.id, Odd.intCast_zmod_two, QuaternionGroup.orderOf_a_one, LFunction_modOne_eq, CongruenceSubgroup.Gamma_mem', LFunction_stdAddChar_eq_expZeta, DirichletCharacter.Odd.eval_neg, val_eq_one, DirichletCharacter.LSeries_eulerProduct_tprod, rootsOfUnity_eq_top, AddSubgroupClass.coe_zmod_smul, WittVector.toZModPow_compat, tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries, WittVector.verschiebung_zmod, AddMonoidHom.toZModLinearMap_injective, orderOf_one_add_mul_prime, LucasLehmer.X.ofNat_snd, QuaternionGroup.a_mul_xa, IsPrimitiveRoot.minpoly_dvd_pow_mod, PadicInt.zmod_congr_of_sub_mem_span, intCast_cast_neg, dft_even_iff, invDFT_apply, charpoly_pow_card, DirichletCharacter.LSeries_modOne_eq, IsCyclic.val_mulAutMulEquiv_apply, LucasLehmer.X.zero_fst, DirichletCharacter.changeLevel_def, exists_sq_eq_prime_iff_of_mod_four_eq_three, isCyclic_units_two_mul_iff_of_odd, DirichletCharacter.LSeriesSummable_of_one_lt_re, Int.quotientSpanNatEquivZMod_comp_Quotient_mk, cast_one, cyclotomicCharacter.toZModPow, DirichletCharacter.conductor_le_conductor_mem_conductorSet, ringEquivCongr_trans, LucasLehmer.X.neg_snd, exists_sq_eq_neg_one_iff, natCast_natAbs_valMinAbs, AddCommGroup.equiv_directSum_zmod_of_finite', DihedralGroup.r_pow, unitsMap_self, intCast_cast_mul, DirichletCharacter.changeLevel_trans, valMinAbs_neg_of_ne_half, DirichletCharacter.LSeries_twist_vonMangoldt_eq, intCast_cast_add, autEquivZmod_symm_apply_natCast, cast_intCast', CliffordAlgebra.toProd_comp_ofProd, quadraticChar_two, DirichletCharacter.LFunction_eq_LSeries, val_unit', val_natCast_of_lt, DirichletCharacter.norm_LSeries_product_ge_one, stdAddChar_coe, trace_pow_card, smulMemClass, CliffordAlgebra.toProd_ι_tmul_one, natCast_eq_one_iff_odd, instIsReducedZModOfFactSquarefreeNat, cast_add_eq_ite, DirichletCharacter.deriv_LFunction_eq_deriv_LSeries, natCast_self, DirichletCharacter.LFunction_changeLevel, isCyclic_units_one, DirichletCharacter.IsPrimitive.completedLFunction_one_sub, not_isUnit_of_mem_primeFactors, intCast_eq_iff, Nat.eq_sq_add_sq_iff_eq_sq_mul, isCyclic_units_iff, natCast_zmod_surjective, minOrder_of_prime, ModN.basis_apply_eq_mkQ, add_self_eq_zero_iff_eq_zero, eq_zero_iff_even, modularCyclotomicCharacter.spec, Polynomial.natDegree_of_dvd_cyclotomic_of_irreducible, LFunction_eq_LSeries, χ₄_int_mod_four, DirichletCharacter.primitiveCharacter_one, AddAction.orbitZMultiplesEquiv_symm_apply', DirichletCharacter.norm_le_one, DirichletCharacter.mul_delta, Finset.sum_indicator_mod, LucasLehmer.X.ofNat_fst, AddAutEquivUnits_symm_apply, ringHom_rightInverse, DirichletCharacter.eval_modulus_sub, Real.not_summable_indicator_one_div_natCast, CongruenceSubgroup.Gamma1_mem', minOrder, ArithmeticFunction.vonMangoldt.support_residueClass_prime_div, exists_sq_eq_two_iff, val_pow_le, inv_neg_one, χ₈'_nat_eq_if_mod_eight, cast_sub', pow_totient, DirichletCharacter.unit_norm_eq_one, PadicInt.ext_of_toZModPow, DirichletCharacter.Odd.to_fun, χ₈'_int_eq_χ₄_mul_χ₈, IsPrimitiveRoot.autToPow_eq_modularCyclotomicCharacter, DirichletCharacter.sum_characters_eq, CliffordAlgebra.map_mul_map_of_isOrtho_of_mem_evenOdd, not_isCyclic_units_of_mul_coprime, CommGroup.equiv_prod_multiplicative_zmod_of_finite, Nat.card_units_zmod_lt_sub_one, natCast_self', AddChar.zmod_add, WittVector.fromPadicInt_comp_toPadicInt, natCast_rightInverse, CliffordAlgebra.evenOdd.gradedMonoid, EisensteinSeries.gammaSetDivGcdSigmaEquiv_symm_eq, DirichletCharacter.toUnitHom_inj, IsPrimitiveRoot.coe_autToPow_apply, zmod_smul_mem, zmod_val_inv_nsmul_nsmul, AddSubgroup.toZModSubmodule_toAddSubgroup, DirichletCharacter.level_one', DirichletCharacter.LSeriesSummable_mul, isSquare_neg_one_iff_forall_mem_primeFactors_mod_four_ne_three, DirichletCharacter.conductor_one, LucasLehmer.sZMod_eq_sMod, val_one'', instIsSimpleAddGroup, dft_comp_unitMul, val_add, IsCyclotomicExtension.Rat.inertiaDegIn_of_not_dvd, natCast_pow_eq_zero_of_le, DirichletCharacter.LSeries_changeLevel, DirichletCharacter.mulEquiv_units, toAddCircle_inj, instIsDomainOfNatNat, Odd.natCast_zmod_two, inv_one, LucasLehmer.residue_eq_zero_iff_sMod_eq_zero, DihedralGroup.oddCommuteEquiv_symm_apply, EisensteinSeries.gammaSet_one_mem_iff, DirichletCharacter.changeLevel_one, val_inv_mul, AddCommGroup.equiv_free_prod_directSum_zmod, val_neg_of_ne_zero, valMinAbs_natCast_of_le_half, cast_pow', val_mul, valMinAbs_natCast_of_half_lt, valMinAbs_zero, val_cast_of_lt, IsPrimitiveRoot.autToPow_injective, CliffordAlgebra.range_ι_le_evenOdd_one, DirichletCharacter.Even.toUnitHom_eval_neg_one, ArithmeticFunction.pow_carmichael, card_units_eq_totient, DihedralGroup.oddCommuteEquiv_apply, inv_coe_unit, IsCyclic.val_inv_mulAutMulEquiv_apply, DirichletCharacter.changeLevel_toUnitHom, unitsMap_comp, instSubsingletonUnits, cast_injective_of_le, exists_prime_addEquiv_ZMod, val_sub, DirichletCharacter.level_one, CliffordAlgebra.one_le_evenOdd_zero, DirichletCharacter.LSeries.mul_mu_eq_one, PadicInt.toZModPow_ofIntSeq_of_pow_dvd_sub, QuaternionGroup.a_mul_a, WittVector.frobeniusPoly_zmod, natAbs_valMinAbs_eq_natAbs_valMinAbs, AddAction.zmultiplesQuotientStabilizerEquiv_symm_apply, val_one', coe_int_inv_mul_eq_one, AddCommGroup.equiv_directSum_zmod_of_finite, autEquivZmod_symm_apply_intCast, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow', eq_neg_of_valMinAbs_eq_neg_valMinAbs, ringEquivCongr_refl_apply, χ₈'_eq_χ₄_mul_χ₈, Nat.range_mul_add, coe_valMinAbs, AddChar.zmodChar_apply', castHom_apply, neg_val, eisSummand_of_gammaSet_eq_divIntMap, algebraOfModule.proof, isPrimitive_stdAddChar, legendreSym.at_two, nonsquare_of_jacobiSym_eq_neg_one, TruncatedWittVector.commutes_symm', intCast_abs_mod_two, forall, isSquare_neg_one_iff, val_one_eq_one_mod, QuaternionGroup.xa_mul_a, lift_castAddHom, mul_val_inv, cast_natCast', cast_one', WittVector.fromPadicInt_comp_toPadicInt_ext, cast_add', lift_comp_coe, cast_zmod_eq_zero_iff_of_le, DirichletCharacter.summable_neg_log_one_sub_mul_prime_cpow, CoxeterSystem.lengthParity_comp_simple, ringEquivCongr_symm, ringEquivCongr_ringEquivCongr_apply, invDFT_def', natCast_eq_natCast_iff', QuaternionGroup.one_def, CliffordAlgebra.GradedAlgebra.ι_apply, natCast_eq_iff, AddAutEquivUnits_apply, cast_mul', jacobiSym.at_neg_two, legendreSym.eq_one_iff, IsPrimitiveRoot.minpoly_dvd_mod_p, natCast_eq_zero_iff, gaussSum_mulShift_of_isPrimitive, completedLFunction_eq, χ₈_int_mod_eight, TruncatedWittVector.charP_zmod, DihedralGroup.orderOf_r_one, FiniteField.two_pow_card, Int.quotientSpanEquivZMod_comp_castRingHom, toAddCircle_natCast, quadraticChar_neg_two, sq_add_sq, dft_apply, castHom_self, cast_cast_zmod_of_le, bijective_rootsOfUnityAddChar, IsCyclotomicExtension.Rat.inertiaDeg_eq, valMinAbs_eq_zero, natAbs_valMinAbs_neg, IsCyclotomicExtension.Rat.galEquivZMod_apply_of_pow_eq, DirichletCharacter.isPrimitive_one_level_one, IsPrimitiveRoot.separable_minpoly_mod, val_zero, DihedralGroup.r_zpow, eq_zero_iff_gcd_ne_one, intCast_cast_sub, isQuadratic_χ₈', LucasLehmer.X.add_snd, invDFT_apply', AddSubgroup.toZModSubmodule_symm, LucasLehmer.sZMod_eq_s, IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_not_dvd, CliffordAlgebra.ι_mul_ι_mem_evenOdd_zero, DirichletCharacter.LSeriesSummable_twist_vonMangoldt, isQuadratic_χ₈, DirichletCharacter.isPrimitive_one_level_zero, DirichletCharacter.modOne_eq_one, DirichletCharacter.convolution_twist_vonMangoldt, EisensteinSeries.vecMul_SL2_mem_gammaSet, PadicInt.zmod_cast_comp_toZModPow, LucasLehmer.X.one_fst, val_neg_one, Subgroup.quotientEquivSigmaZMod_apply, surjective_rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar, χ₄_nat_one_mod_four, val_coe_unit_coprime, pow_zmod_val_inv_pow, jacobiSym.neg, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_pow, DihedralGroup.r_mul_r, isCyclic_units_of_prime_pow, modularCyclotomicCharacter.unique, ringHom_map_cast, exists, not_summable_indicator_mod_of_antitone_of_neg, dft_comp_neg, AddChar.zmodChar_apply, ringHom_surjective, IsCyclotomicExtension.Rat.galEquivZMod_restrictNormal_apply, cast_id', LucasLehmer.X.mul_fst, val_neg', gauss_lemma, lift_comp_castAddHom, exponent, orderOf_one_add_four_mul, intCast_eq_intCast_iff', intCast_zmod_eq_zero_iff_dvd, DirichletCharacter.LSeriesSummable_iff, cast_sub, Nat.prime_iff_fac_equiv_neg_one, CommGroup.equiv_free_prod_prod_multiplicative_zmod, PadicInt.toZModPow_eq_iff_ext, cast_natCast, cast_neg_one, χ₈_nat_mod_eight, instSubsingletonAlgebra, coe_int_isUnit_iff_isCoprime, DihedralGroup.sr_mul_sr, AddSubgroup.coe_toZModSubmodule, natCast_zmod_val, QuaternionGroup.a_one_pow, DirichletCharacter.IsPrimitive.fourierTransform_eq_inv_mul_gaussSum, cast_zero, isUnit_prime_iff_not_dvd, intCast_eq_zero_iff_even, DirichletCharacter.changeLevel_factorsThrough, LucasLehmer.X.snd_intCast, Polynomial.dickson_one_one_zmod_p, coe_int_mul_val_inv, χ₄_int_three_mod_four, DirichletCharacter.absicssaOfAbsConv_eq_one, dft_dft, neg_eq_self_iff, intCast_eq_intCast_iff, cast_intCast, ringEquivCongr_refl, legendreSym.eq_zero_iff, DirichletCharacter.eq_one_iff_conductor_eq_one, χ₄_nat_three_mod_four, DirichletCharacter.sum_characters_eq_zero, intCast_rightInverse, lift_coe, isSquare_neg_one_of_eq_sq_add_sq_of_coprime, QuaternionGroup.xa_mul_xa, DirichletCharacter.mul_convolution_distrib, intCast_eq_one_iff_odd, PadicInt.ker_toZModPow, χ₄_apply, RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply, CoxeterSystem.lengthParity_simple, castHom_comp, DirichletCharacter.norm_LFunction_product_ge_one, CliffordAlgebra.prodEquiv_symm_apply, natCast_eq_zero_iff_even, charP, val_add_val_of_le, instSubsingletonModule, orderOf_one_add_prime, χ₄_int_one_mod_four, LucasLehmer.X.add_fst, Nat.prime_iff_card_units, IsPrimitiveRoot.squarefree_minpoly_mod, CliffordAlgebra.even_toSubmodule, unitsMap_val, addOrderOf_coe', isCyclic_units_four, LSeriesSummable_of_one_lt_re, DirichletCharacter.LSeries_eulerProduct_hasProd, MulAction.zpowersQuotientStabilizerEquiv_symm_apply, CliffordAlgebra.prodEquiv_apply, χ₄_eq_neg_one_pow, cast_descFactorial, intCast_mod, toAddCircle_intCast, MulAction.orbitZPowersEquiv_symm_apply', tsum_dirichletSummand, Ico_map_valMinAbs_natAbs_eq_Ico_map_id, CongruenceSubgroup.Gamma1_mem, jacobiSym.at_two, map_smul, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow', toAddCircle_apply, ker_intCastRingHom, val_intCast, natCast_smul_units, DirichletCharacter.LSeries_eulerProduct_exp_log, legendreSym.eq_one_iff', IsCyclotomicExtension.Rat.inertiaDegIn_eq, val_natCast, ker_intCastAddHom, instFiniteZModUnits, LucasLehmer.X.mul_snd, WittVector.toPadicInt_comp_fromPadicInt_ext, orderOf_one_add_mul_prime_pow, erdos_ginzburg_ziv_multiset, legendreSym.at_neg_one, isUnit_prime_of_not_dvd, CliffordAlgebra.ofProd_comp_toProd, val_add_of_le, pow_pow_zmod_val_inv, neg_eq_self_mod_two, quadraticChar_odd_prime, isSquare_neg_one_iff', WittVector.toPadicInt_comp_fromPadicInt, CliffordAlgebra.evenOdd_mul_le, LucasLehmer.X.neg_fst, cyclotomicCharacter.toZModPow_toFun, lift_injective, mul_inv_eq_gcd, castHom_bijective, TruncatedWittVector.zmodEquivTrunc_apply, SL_reduction_mod_hom_val, DirichletCharacter.changeLevel_eq_one_iff, val_mul_le, gauss_lemma_aux, summable_indicator_mod_iff_summable, Even.intCast_zmod_two, LucasLehmer.X.fst_intCast, cast_id, toAddCircle_injective, nonsquare_iff_jacobiSym_eq_neg_one, DirichletCharacter.FactorsThrough.existsUnique, Even.natCast_zmod_two, DihedralGroup.sr_mul_r, LucasLehmer.X.one_snd, IsCyclic.mulAutMulEquiv_symm_apply_symm_apply, CongruenceSubgroup.Gamma1_to_Gamma0_mem, DirichletCharacter.apply_eq_toArithmeticFunction_apply, modularCyclotomicCharacter.comp, subsingleton_ringEquiv, orderOf_lt, ArithmeticFunction.carmichael_eq_exponent', not_isCyclic_units_eight, PadicInt.zmod_congr_of_sub_mem_span_aux, QuaternionGroup.xa_sq, cyclotomicCharacter.spec, DirichletCharacter.not_LSeriesSummable_at_one, one_eq_zero_iff, val_one, CliffordAlgebra.toProd_one_tmul_ι, DirichletCharacter.changeLevel_self_toUnitHom, val_mul', instIsAddCyclic, abs_valMinAbs_eq_abs_valMinAbs, valMinAbs_natCast_eq_self, rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar_val, natCast_mod, val_two_eq_two_mod, toCircle_intCast, toCircle_natCast, ringChar_zmod_n, orderOf_five, χ₈'_apply, val_add_of_lt, ArithmeticFunction.carmichael_eq_exponent, inv_zero, coe_mul_inv_eq_one, lucas_primality_iff, invDFT_def, Polynomial.natDegree_of_mem_normalizedFactors_cyclotomic, legendreSym.eq_neg_one_iff', injective_toCircle, legendreSym.at_neg_two, χ₄_int_eq_if_mod_four, isReduced_zmod, intCast_zmod_cast, AddChar.zmod_zero, IsPrimitiveRoot.autToPow_spec, isUnit_cast_of_dvd, isSquare_of_jacobiSym_eq_one, TruncatedWittVector.commutes, addOrderOf_one, castHom_injective, isSquare_neg_one_of_eq_sq_add_sq_of_isCoprime, val_pow, IsCyclic.mulAutMulEquiv_symm_apply_apply, coe_unitOfCoprime, DihedralGroup.r_one_pow_n, DirichletCharacter.factorsThrough_iff_ker_unitsMap, natCast_eq_natCast_iff, cast_pow, DihedralGroup.one_def, AddChar.zmodChar_primitive_of_primitive_root, modularCyclotomicCharacter'.spec', CoxeterSystem.lengthParity_eq_ofAdd_length, cast_neg, toCircle_apply, DirichletCharacter.delta_mul, χ₄_nat_mod_four, natAbs_mod_two, CliffordAlgebra.ι_mem_evenOdd_one, Subgroup.transferTransversal_apply'', cast_sub_one, IsPrimitiveRoot.zmodEquivZPowers_apply_coe_nat, coe_int_mul_inv_eq_one, DirichletCharacter.isMultiplicative_toArithmeticFunction, DirichletCharacter.convolution_mul_moebius, charZero, isCyclic_units_two_pow_iff, coe_unitOfIsCoprime, toAddCircle_eq_zero, IsCyclotomicExtension.Rat.inertiaDeg_of_not_dvd, natAbs_valMinAbs_add_le, quadraticChar_neg_one, AddMonoidHom.coe_toZModLinearMap, DihedralGroup.r_mul_sr, isCyclic_units_zero, instIsLocalHomZModRingHomOfIsLocalRingOfNontrivial, subsingleton_ringHom, DirichletCharacter.Odd.toUnitHom_eval_neg_one, DirichletCharacter.factorsThrough_one_iff, DirichletCharacter.Even.to_fun, CliffordAlgebra.ofProd_ι_mk, val_mul_iff_lt, CliffordAlgebra.GradedAlgebra.lift_ι_eq, AddSubgroup.mem_toZModSubmodule, QuaternionGroup.a_zero, val_cast_eq_val_of_lt, χ₈_nat_eq_if_mod_eight, DirichletCharacter.changeLevel_primitiveCharacter, DirichletCharacter.map_zero', TruncatedWittVector.commutes', prod_Ico_one_prime, jacobiSym.at_neg_one, coe_intCast, MvPolynomial.C_dvd_iff_zmod, erdos_ginzburg_ziv, LucasLehmer.X.zero_snd, DirichletCharacter.modZero_eq_delta, ModN.instModuleFinite, DirichletCharacter.fourierTransform_eq_gaussSum_mulShift, IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_mod_eq, IsCyclotomicExtension.Rat.inertiaDeg_eq_of_not_dvd, dft_eq_fourier, dft_odd_iff, reverse_lucas_primality, ringEquivCongr_val, val_eq_zero, isCyclic_units_prime, neg_val', EisensteinSeries.eisensteinSeries_slash_apply, AddChar.zmod_intCast, instIsScalarTower, ringEquivCongr_intCast, natCast_toNat, euler_criterion, eq_unit_mul_divisor, CliffordAlgebra.GradedAlgebra.ι_sq_scalar, DirichletCharacter.LSeries_eulerProduct, val_mul_of_lt, exists_sq_eq_neg_two_iff, CongruenceSubgroup.Gamma_mem, injective_stdAddChar, DirichletCharacter.changeLevel_self, val_cast_zmod_lt, AddChar.zmodAddEquiv_apply, isCyclic_units_four_mul_iff, isQuadratic_χ₄, CliffordAlgebra.evenOdd_isCompl, PadicInt.cast_toZModPow, eisenstein_lemma_aux, smul_mem, EisensteinSeries.gammaSetDivGcdEquiv_eq, completedLFunction_modOne_eq, IsPrimitiveRoot.zmodEquivZPowers_apply_coe_int, AddChar.zmod_injective, WittVector.zmodEquivTrunc_compat, DihedralGroup.r_one_pow, DihedralGroup.inv_r, castHom_surjective, dft_def, DirichletCharacter.conductor_one_dvd, DirichletCharacter.changeLevel_eq_cast_of_dvd, coe_int_val_inv_mul, cauchy_davenport, χ₈_apply, valMinAbs_spec, intCast_surjective, modularCyclotomicCharacter'.unique', Polynomial.normalizedFactors_cyclotomic_card, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, instIsAddKleinFourProdZModOfNatNat, rootsOfUnityAddChar_val, toCircle_eq_circleExp, Int.quotientSpanNatEquivZMod_comp_castRingHom, eq_zero_of_gcd_ne_one, stdAddChar_apply, IsCyclotomicExtension.autEquivPow_symm_apply, EisensteinSeries.mem_gammaSet_one, cyclotomicCharacter.toFun_spec, val_add_le, TruncatedWittVector.commutes_symm, DirichletCharacter.FactorsThrough.eq_changeLevel, IsPrimitiveRoot.zmodEquivZPowers_symm_apply_zpow, cast_mul, IsDedekindDomain.selmerGroup.valuation_ker_eq, χ₄_nat_eq_if_mod_four, IsCyclotomicExtension.autEquivPow_apply, DihedralGroup.r_zero, dft_apply_zero, LucasLehmer.X.snd_natCast, χ₈_int_eq_if_mod_eight, instHasEnoughRootsOfUnityHSubNatOfNat, IsCyclotomicExtension.Rat.galEquivZMod_smul_of_pow_eq, nsmul_zmod_val_inv_nsmul, unitsMap_def, cast_add, summable_indicator_mod_iff, WittVector.frobenius_zmodp, DirichletCharacter.Even.eval_neg, CongruenceSubgroup.Gamma0_mem, eq_one_iff_odd
|