Documentation Verification Report

Defs

📁 Source: Mathlib/Algebra/Ring/Int/Defs.lean

Statistics

Metric	Count
Definitions `instCommRing`, `instCommSemiring`, `instDistrib`, `instRing`, `instSemiring`	5
Theorems `cast_mul`, `cast_mul_eq_zsmul_cast`, `cast_pow`, `instCharZero`, `instIsCancelMulZero`, `instIsDomain`, `instMulDivCancelClass`	7
Total	12

Int

Definitions

Name	Category	Theorems
`instCommRing` 📖	CompOp	628 math math: `IsPrimitiveRoot.subOneIntegralPowerBasis_gen_prime`, `CongruenceSubgroup.Gamma_zero_bot`, `NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply'`, `Num.cast_to_int`, `instPosSMulStrictMonoIntOfIsOrderedAddMonoid`, `WittVector.bind₁_frobeniusPoly_wittPolynomial`, `sign_intCast`, `ModularForm.mul_slash_SL2`, `IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime`, `RootPairing.GeckConstruction.h_def`, `ModularGroup.SLOnGLPos_smul_apply`, `AlgebraicGeometry.AffineSpace.map_toSpecMvPoly_assoc`, `IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime_pow`, `ComplexShape.ε_succ`, `HNNExtension.toSubgroup_neg_one`, `NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply`, `quotientSpanEquivZMod_comp_Quotient_mk`, `IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow`, `Ideal.absNorm_span_insert`, `NumberField.isCoprime_differentIdeal_of_isCoprime_discr`, `CongruenceSubgroup.Gamma_mem'`, `IsPrimitiveRoot.totient_le_degree_minpoly`, `ComplexShape.χ_prev`, `RootPairing.Base.injective_pairingIn`, `FreeAbelianGroup.toFinsupp_toFreeAbelianGroup`, `ComplexShape.EulerCharSigns.χ_next`, `AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply`, `WittVector.ghostComponent_apply`, `NumberField.RingOfIntegers.instIsIntegralClosureIntWithVal`, `NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply'`, `IsPrimitiveRoot.minpoly_dvd_pow_mod`, `Equiv.Perm.sign_of_cycleType`, `CongruenceSubgroup.instFiniteIndexGamma`, `Finsupp.sum_zsmul`, `ComplexShape.eulerCharSignsDownNat_χ`, `ArithmeticFunction.intCoe_one`, `LieAlgebra.isSolvable_iff_int`, `CongruenceSubgroup.exists_Gamma_le_conj'`, `IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_apply`, `RootPairing.Base.cartanMatrix_map_abs`, `AddSubgroup.exists_finsupp_of_mem_closure_range`, `ModularForm.SL_slash`, `CongruenceSubgroup.conjGL_coe`, `CongruenceSubgroup.mem_Gamma_one`, `quotientSpanNatEquivZMod_comp_Quotient_mk`, `IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two_pow`, `IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers`, `RootPairing.EmbeddedG2.pairingIn_threeShortAddLong_right`, `Matrix.detp_neg_one_one`, `Real.isIntegral_two_mul_sin_rat_mul_pi`, `ArithmeticFunction.moebius_eq_or`, `Equiv.Perm.signAux_swap`, `IsDedekindDomain.HeightOneSpectrum.intValuation_le_one`, `IsCyclotomicExtension.Rat.ramificationIdxIn_eq`, `instIsCancelMulZero`, `WeierstrassCurve.valuation_Δ_aux_eq_of_isIntegral`, `ArithmeticFunction.moebius_ne_zero_iff_eq_or`, `WittVector.mul_polyOfInterest_aux2`, `FractionalIdeal.absNorm_eq'`, `ModularGroup.one_lt_normSq_T_zpow_smul`, `instLieModuleInt`, `CongruenceSubgroup.strictPeriods_Gamma0`, `FractionalIdeal.count_finsuppProd`, `Algebra.discr_eq_discr`, `IsPrimitiveRoot.subOneIntegralPowerBasis_gen`, `Rat.isFractionRingDen`, `IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one'`, `RingOfIntegers.exponent_eq_sInf`, `quadraticChar_isQuadratic`, `CongruenceSubgroup.Gamma_normal`, `ArithmeticFunction.LSeries_zeta_mul_Lseries_moebius`, `Matrix.SpecialLinearGroup.map_intCast_injective`, `negOnePow_eq_neg_one_iff`, `RootPairing.Base.pairingIn_le_zero_of_ne`, `ModularGroup.coe_apply_complex`, `jacobiTheta_T_sq_smul`, `instMulDivCancelClass`, `RootPairing.Base.cartanMatrix_nondegenerate`, `ModularForm.levelOne_neg_weight_rank_zero`, `Ideal.absNorm_eq_pow_inertiaDeg'`, `Subgroup.IsArithmetic.is_commensurable`, `Finset.prod_indicator_biUnion_finset_sub_indicator`, `ModularGroup.sl_moeb`, `ZNum.gcd_to_nat`, `IsPrimitiveRoot.is_roots_of_minpoly`, `LaurentSeries.ofPowerSeries_powerSeriesPart`, `ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq`, `LaurentSeries.single_order_mul_powerSeriesPart`, `Matrix.SpecialLinearGroup.coe_int_neg`, `NumberField.RingOfIntegers.withValEquiv_symm_apply`, `EisensteinSeries.E2_slash_action`, `FixedDetMatrices.reps_zero_empty`, `ArithmeticFunction.moebius_sq`, `normUnit_eq`, `IsPrimitiveRoot.norm_toInteger_sub_one_of_eq_two`, `ModularGroup.coe_T_zpow_smul_eq`, `NumberField.FinitePlace.prod_eq_inv_abs_norm_int`, `CongruenceSubgroup.exists_Gamma_le_conj`, `Real.isIntegral_two_mul_cos_rat_mul_pi`, `ArithmeticFunction.moebius_apply_one`, `Fin.sign_cycleRange`, `Equiv.Perm.sign_eq_prod_prod_Ioi`, `isEllSequence_id`, `EisensteinSeries.G2_slash_action`, `ArithmeticFunction.not_LSeriesSummable_moebius_at_one`, `Subgroup.instIsArithmeticRangeSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGL`, `LaurentPolynomial.invOf_T`, `RootPairing.EmbeddedG2.toIsValuedIn`, `IsPrimitiveRoot.integralPowerBasisOfPrimePow_gen`, `IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime_pow`, `RootPairing.finrank_corootSpanIn_int`, `ComplexShape.ε₁_ε₂`, `RootPairing.pairingIn_pairingIn_mem_set_of_length_eq`, `RootPairing.zero_le_pairingIn_of_root_sub_mem`, `ArithmeticFunction.moebius_mul_coe_zeta`, `HNNExtension.toSubgroupEquiv_neg_one`, `IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_pow_ne_two`, `ArithmeticFunction.moebius_apply_prime_pow`, `ModularGroup.tendsto_abs_re_smul`, `CongruenceSubgroup.Gamma1_mem'`, `Equiv.Perm.sign_of_cycleType_eq_replicate`, `Subgroup.instIsArithmeticMapSpecialLinearGroupFinOfNatNatIntGeneralLinearGroupRealMapGLOfFiniteIndex`, `AddSubgroup.index_eq_natAbs_det`, `IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime`, `ArithmeticFunction.moebius_eq_zero_of_not_squarefree`, `ZNum.cmp_to_int`, `IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply`, `GradedTensorProduct.tmul_coe_mul_coe_tmul`, `ModularGroup.exists_max_im`, `ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on_of_nonzero`, `RootPairing.Base.exists_mem_span_pairingIn_ne_zero_and_pairwise_ne`, `ComplexShape.TensorSigns.ε'_succ`, `Rat.associated_num_den`, `ComplexShape.ε_down_ℕ`, `Subgroup.IsArithmetic.isCusp_iff_isCusp_SL2Z`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime_pow`, `CongruenceSubgroup.instFiniteIndexGamma1`, `isCusp_SL2Z_iff'`, `RootPairing.pairingIn_pairingIn_mem_set_of_length_eq_of_ne`, `Equiv.Perm.decomposeFin.symm_sign`, `ModularGroup.denom_apply`, `IsPrimitiveRoot.minpoly_eq_pow_coprime`, `CliffordAlgebra.map_mul_map_of_isOrtho_of_mem_evenOdd`, `ZNum.mod_to_int`, `ModularGroup.im_T_smul`, `RootPairing.finrank_rootSpanIn_int`, `LaurentSeries.val_le_one_iff_eq_coe`, `IsPrimitiveRoot.subOneIntegralPowerBasis'_gen_prime`, `FixedDetMatrices.T_S_rel_smul`, `ArithmeticFunction.moebius_apply_of_squarefree`, `ModEq.listSum_map_zero`, `Finsupp.toFreeAbelianGroup_comp_singleAddHom`, `RootPairing.pairingIn_eq_zero_of_add_notMem_of_sub_notMem`, `CongruenceSubgroup.Gamma_one_top`, `IsCyclotomicExtension.Rat.inertiaDegIn_of_not_dvd`, `WithZeroMulInt.toNNReal_lt_one_iff`, `Finsupp.prod_zpow`, `IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime`, `Algebra.coe_norm_int`, `LaurentPolynomial.T_zero`, `IsIntegral.ratCast_iff`, `RootPairing.isG2_iff`, `IsPrimitiveRoot.adjoinEquivRingOfIntegers_apply`, `Matrix.num_zero`, `FreeAbelianGroup.equivFinsupp_symm_apply`, `AddCommGroup.equiv_free_prod_directSum_zmod`, `ModEq.listSum_zero`, `RootPairing.IsG2.toIsValuedIn`, `LaurentPolynomial.degree_C`, `LieModule.isNilpotent_iff_int`, `EisensteinSeries.G2_S_transform`, `Complex.isIntegral_exp_rat_mul_pi_mul_I`, `Matrix.det_eq_detp_sub_detp`, `ModularGroup.SL_to_GL_tower`, `ModularFormClass.one_mem_strictPeriods_SL2Z`, `divisorsAntidiag_natCast`, `WeierstrassCurve.IsMinimal.val_Δ_maximal`, `ModularGroup.T_mul_apply_one`, `IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime_pow`, `IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_two`, `jacobiTheta_S_smul`, `ModularForm.levelOne_weight_zero_rank_one`, `ModularGroup.re_T_smul`, `CongruenceSubgroup.strictWidthInfty_Gamma0`, `IsPrimitiveRoot.integralPowerBasis'_gen`, `UnitsInt.univ`, `IsDedekindDomain.HeightOneSpectrum.valuation_div_le_one_iff`, `Rep.toAdditive_symm_apply`, `FreeAbelianGroup.toFinsupp_comp_toFreeAbelianGroup`, `Equiv.Perm.sign_eq_prod_prod_Iio`, `IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd`, `Real.isAlgebraic_tan_rat_mul_pi`, `IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two'`, `HNNExtension.NormalWord.unitsSMul_cancels_iff`, `CongruenceSubgroup.Gamma_cong_eq_self`, `Complex.isAlgebraic_sin_rat_mul_pi`, `Finsupp.toFreeAbelianGroup_single`, `WittVector.mul_polyOfInterest_aux4`, `DirichletCharacter.LSeries.mul_mu_eq_one`, `ModularGroup.coe_T_inv`, `ZNum.le_to_int`, `Real.isAlgebraic_cos_rat_mul_pi`, `Rep.ofMulDistribMulAction_ρ_apply_apply`, `ModularGroup.T_inv_mul_apply_one`, `Rat.valuation_le_one_iff_den`, `IsPrimitiveRoot.subOneIntegralPowerBasis'_gen`, `Matrix.SpecialLinearGroup.isClosedEmbedding_mapGLInt`, `RootPairing.coxeterWeightIn_eq_zero_iff`, `IsPrimitiveRoot.power_basis_int'_dim`, `RootPairing.EmbeddedG2.pairingIn_twoShortAddLong_left`, `Subgroup.IsArithmetic.isFiniteRelIndexSL`, `LaurentSeries.powerSeriesPart_coeff`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure`, `RootPairing.IsNotG2.toIsValuedIn`, `UpperHalfPlane.exists_SL2_smul_eq_of_apply_zero_one_ne_zero`, `UpperHalfPlane.modular_S_smul`, `cast_det`, `WeierstrassCurve.isGoodReduction_iff`, `ModularGroup.re_T_inv_smul`, `EisensteinSeries.D2_inv`, `NumberField.house.exists_ne_zero_int_vec_house_le`, `CongruenceSubgroup.isArithmetic_conj_SL2Z`, `fract_int`, `HNNExtension.NormalWord.unitsSMulGroup_snd`, `EisensteinSeries.q_expansion_riemannZeta`, `ArithmeticFunction.moebius_apply_prime`, `ArithmeticFunction.intCoe_mul`, `ModularGroup.denom_S`, `RingOfIntegers.not_dvd_exponent_iff`, `WittVector.bind₁_wittMulN_wittPolynomial`, `IsPrimitiveRoot.integralPowerBasisOfPrimePow_dim`, `FixedDetMatrices.reduce_mem_reps`, `ModularGroup.normSq_S_smul_lt_one`, `RootPairing.EmbeddedG2.pairingIn_threeShortAddTwoLong_right`, `ModularGroup.T_pow_mul_apply_one`, `Subgroup.mem_closure_range_iff`, `WithZeroMulInt.toNNReal_le_one_iff`, `ComplexShape.ε₂_ε₁`, `NumberField.discr_eq_discr`, `AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly_assoc`, `ModularGroup.exists_row_one_eq_and_min_re`, `Fin.sign_cycleIcc_of_le`, `IsPrimitiveRoot.minpoly_dvd_expand`, `FunctionField.InftyValuation.map_one'`, `IsCyclotomicExtension.ring_of_integers'`, `WittVector.mul_polyOfInterest_vars`, `RootPairing.IsG2.span_eq_rootSpan_int`, `negOnePow_one`, `IsPrimitiveRoot.minpoly_dvd_mod_p`, `Equiv.Perm.ofSign_disjoint`, `isDivSequence_id`, `groupCohomology.norm_ofAlgebraAutOnUnits_eq`, `AddSubgroup.mem_closure_range_iff`, `Equiv.Perm.sign_of_pow_two_eq_one`, `RootPairing.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed`, `ModularGroup.re_T_zpow_smul`, `FreeAbelianGroup.toFinsupp_of`, `Num.cast_ofZNum`, `Rep.toAdditive_apply`, `quotientSpanEquivZMod_comp_castRingHom`, `IsCyclotomicExtension.ringOfIntegers`, `Ideal.relNorm_int`, `AlgebraicGeometry.AffineSpace.map_toSpecMvPoly`, `IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one`, `RootPairing.chainBotCoeff_add_chainTopCoeff_eq_pairingIn_chainTopIdx`, `CuspForm.coe_translate`, `SpecialLinearGroup.SL2Z_generators`, `IsCyclotomicExtension.Rat.inertiaDeg_eq`, `Submodule.natAbs_det_equiv`, `ModularGroup.im_lt_im_S_smul`, `NumberField.Units.dirichletUnitTheorem.seq_norm_le`, `IsPrimitiveRoot.separable_minpoly_mod`, `Complex.isIntegral_two_mul_sin_rat_mul_pi`, `IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem`, `IsDedekindDomain.HeightOneSpectrum.valuation_of_unit_eq`, `negOnePow_odd`, `absNorm_under_mem`, `ZMod.isQuadratic_χ₈'`, `IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_not_dvd`, `Subgroup.isArithmetic_iff_finiteIndex`, `ZMod.isQuadratic_χ₈`, `RootPairing.IsG2.pairingIn_mem_zero_one_three`, `wittStructureInt_prop`, `negOnePow_def`, `IsPrimitiveRoot.norm_toInteger_sub_one_eq_one`, `ModularGroup.im_T_zpow_smul`, `FractionalIdeal.absNorm_eq`, `EisensteinSeries.isBoundedAtImInfty_eisensteinSeries_SIF`, `RootPairing.EmbeddedG2.pairingIn_long_short`, `EisensteinSeries.vecMul_SL2_mem_gammaSet`, `IsPrimitiveRoot.isIntegral`, `NumberField.RingOfIntegers.mk_zero`, `IsCyclotomicExtension.Rat.inertiaDeg_span_zeta_sub_one'`, `isCusp_SL2Z_iff`, `RootPairing.coxeterWeightIn_mem_set_of_isCrystallographic`, `IsDedekindDomain.HeightOneSpectrum.intValuation.map_one'`, `RootPairing.EmbeddedG2.pairingIn_threeShortAddLong_left`, `ModularForm.slash_action_eq'_iff`, `surjective_cosetToCuspOrbit`, `LieAlgebra.IsSolvable.solvable_int`, `Num.ofZNum_toNat`, `ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq`, `CongruenceSubgroup.strictWidthInfty_Gamma1`, `ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq_on`, `FreeAbelianGroup.equivFinsupp_apply`, `EisensteinSeries.eisensteinSeries_SIF_apply`, `ArithmeticFunction.sum_eq_iff_sum_mul_moebius_eq`, `Equiv.Perm.signAux3_mul_and_swap`, `NumberField.RingOfIntegers.withValEquiv_apply`, `RootPairing.forall_pairingIn_eq_swap_or`, `LaurentSeries.hasseDeriv_coeff`, `CongruenceSubgroup.finiteIndex_conjGL`, `Complex.isIntegral_exp_neg_rat_mul_pi_mul_I`, `Matrix.num_ofNat`, `RootPairing.EmbeddedG2.pairingIn_short_long`, `ModularGroup.exists_one_half_le_im_smul`, `CongruenceSubgroup.instFiniteIndexGamma0`, `DivisibleHull.qsmul_def`, `groupCohomology.cocyclesOfIsMulCocycle₂_coe`, `instStarOrderedRing`, `IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd`, `negOnePow_two_mul_add_one`, `WittVector.frobeniusPolyAux_eq`, `Matrix.superFactorial_dvd_vandermonde_det`, `SignType.intCast_cast`, `NumberField.discr_mem_differentIdeal`, `groupCohomology.coboundariesOfIsMulCoboundary₁_coe`, `UpperHalfPlane.petersson_slash_SL`, `NumberField.absNorm_differentIdeal`, `Matrix.num_natCast`, `NumberField.RingOfIntegers.isIntegral_coe`, `units_eq_one_or`, `CongruenceSubgroup.ModularGroup_T_pow_mem_Gamma`, `ModularForm.SL_slash_def`, `LaurentSeries.hasseDeriv_single_add`, `RootPairing.GeckConstruction.diagonal_elim_mem_span_h_iff`, `IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_symm_apply`, `WeierstrassCurve.isMinimal_iff`, `IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff`, `exists_signed_sum'`, `cast_list_sum`, `Polynomial.IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast`, `NumberField.RingOfIntegers.mk_one`, `Rat.isFractionRingNum`, `Set.unit_valuation_eq_one`, `Matrix.detp_smul_adjp`, `IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two`, `CongruenceSubgroup.strictPeriods_Gamma1`, `RootPairing.pairingIn_pairingIn_mem_set_of_isCrystal_of_isRed'`, `AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply`, `Finsupp.toFreeAbelianGroup_toFinsupp`, `NumberField.RingOfIntegers.instIsIntegralClosureInt`, `RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply`, `absNorm_under_dvd_absNorm`, `groupCohomology.cocyclesOfIsMulCocycle₁_coe`, `WittVector.mul_polyOfInterest_aux1`, `CartanMatrix.F₄_det`, `IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two`, `bind₁_rename_expand_wittPolynomial`, `CongruenceSubgroup.strictWidthInfty_Gamma`, `LieIdeal.coe_derivedSeries_eq_int`, `ArithmeticFunction.moebius_sq_eq_one_of_squarefree`, `IsPrimitiveRoot.squarefree_minpoly_mod`, `transcendental_liouvilleNumber`, `LSeries_one_mul_Lseries_moebius`, `UpperHalfPlane.ModularGroup_T_zpow_mem_verticalStrip`, `HNNExtension.toSubgroupEquiv_neg_apply`, `ZNum.abs_to_nat`, `EisensteinSeries.q_expansion_bernoulli`, `ArithmeticFunction.abs_moebius_eq_one_of_squarefree`, `RootPairing.pairingIn_rat`, `IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_not_dvd`, `EisensteinSeries.D2_one`, `CongruenceSubgroup.Gamma1_in_Gamma0`, `RootPairing.EmbeddedG2.pairingIn_twoShortAddLong_right`, `CongruenceSubgroup.Gamma1_mem`, `IsPrimitiveRoot.card_quotient_toInteger_sub_one`, `IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime_pow`, `ModularGroup.im_smul_eq_div_normSq`, `HNNExtension.NormalWord.unitsSMul_neg`, `ZNum.to_of_int`, `IsCyclotomicExtension.Rat.inertiaDegIn_eq`, `RootPairing.Base.exists_root_eq_sum_int`, `Polynomial.cyclotomic_eq_prod_X_pow_sub_one_pow_moebius`, `witt_structure_prop`, `Matrix.detp_smul_add_adjp`, `CongruenceSubgroup.mem_conjGL`, `RootPairing.pairingIn_le_zero_of_root_add_mem`, `WittVector.bind₁_verschiebungPoly_wittPolynomial`, `Matrix.SpecialLinearGroup.map_intCast_inj`, `Ideal.natAbs_det_equiv`, `ArithmeticFunction.LSeriesSummable_moebius_iff`, `ArithmeticFunction.sum_moebius_mul_log_eq`, `Real.isAlgebraic_sin_rat_mul_pi`, `ComplexShape.eulerCharSignsUpNat_χ`, `WithZeroMulInt.toNNReal_eq_one_iff`, `RootPairing.EmbeddedG2.pairingIn_threeShortAddTwoLong_left`, `EisensteinSeries.tendsto_double_sum_S_act`, `CongruenceSubgroup.strictPeriods_Gamma`, `ModularGroup.tendsto_lcRow0`, `cosetToCuspOrbit_apply_mk`, `Matrix.isAddUnit_detp_smul_mul_adjp`, `Matrix.detp_mul`, `Matrix.num_one`, `Complex.isIntegral_two_mul_cos_rat_mul_pi`, `GradedTensorProduct.comm_coe_tmul_coe`, `instTrivialStar`, `LieModule.coe_lowerCentralSeries_eq_int`, `SL_reduction_mod_hom_val`, `SlashInvariantForm.slash_S_apply`, `Ioc_filter_dvd_eq`, `Polynomial.toLaurent_one`, `WittVector.wittMul_zero`, `LaurentPolynomial.degree_C_ite`, `LaurentPolynomial.smeval_one`, `WittVector.polyOfInterest_vars_eq`, `LaurentPolynomial.single_zero_one_eq_one`, `ModularGroup.coe_one`, `ZNum.of_to_int`, `CongruenceSubgroup.Gamma1_to_Gamma0_mem`, `Subgroup.strictPeriods_SL2Z`, `CongruenceSubgroup.mem_conjGL'`, `WittVector.wittNeg_zero`, `IsCyclotomicExtension.Rat.cyclotomicRing_isIntegralClosure_of_prime`, `NumberField.RingOfIntegers.isIntegral`, `IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_pow_ne_two`, `ComplexShape.χ_next`, `RootPairing.chainBotCoeff_if_one_zero`, `RootPairing.chainTopCoeff_if_one_zero`, `ZNum.div_to_int`, `NumberField.hermiteTheorem.natDegree_le_rankOfDiscrBdd`, `IsPrimitiveRoot.IsCyclotomicExtension.ringOfIntegersOfPrimePow`, `TensorProduct.tmul_of_gradedMul_of_tmul`, `ModularGroup.exists_one_half_le_im_smul_and_norm_denom_le`, `IsPrimitiveRoot.integralPowerBasis_dim`, `ModularGroup.T_S_rel`, `HNNExtension.NormalWord.unitsSMulEquiv_symm_apply`, `IsCyclotomicExtension.Rat.ramificationIdx_of_not_dvd`, `EisensteinSeries.vecMulSL_gcd`, `WittVector.bind₁_onePoly_wittPolynomial`, `ZNum.lt_to_int`, `RootPairing.Base.IsPos.exists_mem_support_pos_pairingIn`, `divisorsAntidiag_neg`, `WittVector.wittOne_zero_eq_one`, `LieModule.IsNilpotent.nilpotent_int`, `Matrix.num_intCast`, `IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen`, `IsCyclotomicExtension.Rat.ramificationIdx_eq_of_not_dvd`, `SlashInvariantForm.vAdd_width_periodic`, `ModularGroup.exists_smul_mem_fd`, `AlgebraicGeometry.AffineSpace.over_over`, `RootPairing.chainTopCoeff_sub_chainBotCoeff`, `ModularFormClass.bdd_at_infty_slash`, `AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp`, `NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply`, `divisorsAntidiag_ofNat`, `HNNExtension.ReducedWord.map_fst_eq_and_of_prod_eq`, `AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly`, `NumberField.RingOfIntegers.instIsIntegralInt`, `ModularGroup.coe_T`, `Num.to_nat_to_int`, `FractionalIdeal.absNorm_div_norm_eq_absNorm_div_norm`, `Num.ofZNum'_toNat`, `CuspFormClass.zero_at_infty_slash`, `CongruenceSubgroup.conj_cong_is_cong`, `Matrix.mul_adjp_apply_ne`, `Matrix.det_neg_eq_smul`, `ModularForm.is_invariant_one'`, `Ideal.absNorm_eq_pow_inertiaDeg`, `EisensteinSeries.eisensteinSeriesSIF_apply`, `ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_on`, `IsPrimitiveRoot.coe_toInteger`, `FunctionField.inftyValuation.C`, `ModularGroup.im_T_inv_smul`, `sign_finRotate`, `NumberField.Embeddings.finite_of_norm_le`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one`, `Equiv.Perm.IsCycle.sign`, `IsPrimitiveRoot.integralPowerBasis_gen`, `IsCyclotomicExtension.Rat.ramificationIdx_eq`, `Nat.modEq_eleven_digits_sum`, `UpperHalfPlane.modular_T_zpow_smul`, `IsCyclotomicExtension.Rat.associated_norm_zeta_sub_one`, `ZNum.cast_to_int`, `IsPrimitiveRoot.pow_isRoot_minpoly`, `Equiv.Perm.IsSwap.sign_eq`, `EisensteinSeries.eisensteinSeries_tendstoLocallyUniformlyOn`, `TensorProduct.gradedCommAux_lof_tmul`, `CongruenceSubgroup.IsCongruenceSubgroup.finiteIndex`, `RootPairing.isNotG2_iff`, `PowerSeries.coe_one`, `units_ne_iff_eq_neg`, `Matrix.SpecialLinearGroup.coe_matrix_coe`, `ArithmeticFunction.coe_zeta_mul_moebius`, `Set.integer_valuation_le_one`, `Finset.prod_indicator_biUnion_sub_indicator`, `Complex.isAlgebraic_tan_rat_mul_pi`, `Nat.ofDigits_neg_one`, `instIsDomain`, `DirichletCharacter.convolution_mul_moebius`, `ModularForm.is_invariant_const`, `Subgroup.IsArithmetic.finiteIndex_comap`, `WittVector.mul_polyOfInterest_aux5`, `Matrix.num_eq_zero_iff`, `AddSubgroup.relIndex_eq_natAbs_det`, `ModularForm.SL_slash_apply`, `IsCyclotomicExtension.Rat.inertiaDeg_of_not_dvd`, `Matrix.SpecialLinearGroup.discreteSpecialLinearGroupIntRange`, `ZNum.dvd_to_int`, `EisensteinSeries.eisSummand_SL2_apply`, `Nat.moebius_eq`, `CartanMatrix.G₂_det`, `EisensteinSeries.eisensteinSeries_SIF_MDifferentiable`, `IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one`, `ArithmeticFunction.abs_moebius_le_one`, `RootPairing.IsG2.exists_pairingIn_neg_three`, `ideal_span_absNorm_eq_self`, `IsAddTorsionFree.to_noZeroSMulDivisors_int`, `Equiv.Perm.sign_prod_list_swap`, `ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on'`, `IsCyclotomicExtension.Rat.ramificationIdxIn_of_not_dvd`, `ModularGroup.coe_T_zpow`, `instCharZero`, `WittVector.mul_polyOfInterest_aux3`, `WittVector.verschiebungPoly_zero`, `MvPolynomial.C_dvd_iff_zmod`, `WittVector.wittOne_pos_eq_zero`, `isIntegral_two_mul_cos_rat_mul_pi`, `IsPrimitiveRoot.minpoly_eq_pow`, `exists_signed_sum`, `Complex.isAlgebraic_cos_rat_mul_pi`, `Algebra.coe_trace_int`, `absNorm_under_eq_sInf`, `Ideal.absNorm_span_singleton`, `IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton`, `RootPairing.EmbeddedG2.pairingIn_shortAddLong_left`, `IsCyclotomicExtension.Rat.inertiaDeg_eq_of_not_dvd`, `WeierstrassCurve.IsGoodReduction.goodReduction`, `IsPrimitiveRoot.minpoly_dvd_cyclotomic`, `Equiv.Perm.sign_of_cycleType'`, `RootPairing.pairingIn_pairingIn_mem_set_of_isCrystallographic`, `NumberField.RingOfIntegers.minpoly_coe`, `ModularGroup.coe_S`, `EisensteinSeries.eisensteinSeries_slash_apply`, `IsCyclotomicExtension.Rat.ramificationIdxIn_of_prime`, `cast_mem_ideal_iff`, `Liouville.transcendental`, `RootPairing.GeckConstruction.h_eq_diagonal`, `Polynomial.cyclotomic_eq_minpoly`, `ArithmeticFunction.intCoe_apply`, `ArithmeticFunction.prod_eq_iff_prod_pow_moebius_eq_of_nonzero`, `Equiv.Perm.ofSign_disjUnion`, `TensorProduct.gradedComm_of_tmul_of`, `IsCyclotomicExtension.Rat.inertiaDeg_eq_of_prime`, `PowerSeries.rescale_neg_one_invOneSubPow`, `CongruenceSubgroup.Gamma_mem`, `EisensteinSeries.eisensteinSeriesSIF_mdifferentiable`, `IsDedekindDomain.HeightOneSpectrum.valuation_le_one`, `ModularGroup.S_mul_S_eq`, `Ideal.natAbs_det_basis_change`, `negOnePow_succ`, `C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum`, `ModularGroup.coeHom_apply`, `RootPairing.EmbeddedG2.pairingIn_shortAddLong_right`, `ZMod.isQuadratic_χ₄`, `ZNum.to_int_inj`, `Subgroup.strictWidthInfty_SL2Z`, `Ideal.ringChar_quot`, `ZNum.mul_to_int`, `Matrix.mul_adjp_add_detp`, `TotalComplexShape.ε₂_ε₁`, `WittVector.wittSub_zero`, `IsPrimitiveRoot.norm_toInteger_sub_one_of_prime_ne_two'`, `ArithmeticFunction.IsMultiplicative.prodPrimeFactors_one_sub_of_squarefree`, `ModularGroup.SL_neg_smul`, `WittVector.wittZero_eq_zero`, `liesOver_span_absNorm`, `IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime`, `Complex.isIntegral_int_I`, `Ico_filter_dvd_eq`, `instWellFoundedGTWithZeroMultiplicativeIntLeOne`, `Equiv.Perm.sign_swap'`, `StarAddMonoid.toStarModuleInt`, `ModularForm.is_invariant_one`, `Equiv.Perm.sign_swap`, `EisensteinSeries.tsum_symmetricIco_tsum_eq_S_act`, `IsPrimitiveRoot.subOneIntegralPowerBasisOfPrimePow_gen_prime`, `NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply`, `IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one`, `RootPairing.chainBotCoeff_sub_chainTopCoeff`, `EisensteinSeries.D2_mul`, `Nat.absNorm_under_prime`, `ArithmeticFunction.sum_eq_iff_sum_smul_moebius_eq_on`, `quotientSpanNatEquivZMod_comp_castRingHom`, `Matrix.isAddUnit_detp_mul_detp`, `divisorsAntidiag_neg_natCast`, `Subgroup.exists_finsupp_of_mem_closure_range`, `WittVector.wittAdd_zero`, `LaurentPolynomial.degree_C_le`, `UpperHalfPlane.modular_T_smul`, `ZNum.of_to_int'`, `IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem`, `LaurentSeries.hasseDeriv_single`, `HNNExtension.ReducedWord.exists_normalWord_prod_eq`, `Rat.ringOfIntegersWithValEquiv_apply`, `IsPrimitiveRoot.norm_toInteger_pow_sub_one_of_prime_ne_two`, `ModularForm.SL_smul_slash`, `Finsupp.toFreeAbelianGroup_comp_toFinsupp`, `castRingHom_int`, `ModEq.listSum_map`, `map_neg_divisorsAntidiag`, `IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers`, `SlashInvariantForm.T_zpow_width_invariant`, `ArithmeticFunction.moebius_apply_isPrimePow_not_prime`, `EisensteinSeries.isBoundedAtImInfty_eisensteinSeriesSIF`, `RootPairing.Base.chainTopCoeff_eq_of_ne`, `IsPrimitiveRoot.minpoly_dvd_x_pow_sub_one`, `Submodule.natAbs_det_basis_change`, `ArithmeticFunction.abscissaOfAbsConv_moebius`, `CongruenceSubgroup.Gamma0_mem`, `Ideal.absNorm_dvd_norm_of_mem`, `EisensteinSeries.G2_T_transform`, `FixedDetMatrices.S_smul_four`, `RootPairing.baseOf_pairwise_pairing_le_zero`, `Nat.eleven_dvd_iff`, `ArithmeticFunction.abs_moebius`, `RootPairing.IsNotG2.pairingIn_mem_zero_one_two`, `isEllDivSequence_id`
`instCommSemiring` 📖	CompOp	270 math math: `NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply'`, `WittVector.bind₁_frobeniusPoly_wittPolynomial`, `WittVector.remainder_vars`, `AlgebraicGeometry.AffineSpace.map_toSpecMvPoly_assoc`, `quadraticChar_card_sqrts`, `ZMod.χ₈'_int_eq_if_mod_eight`, `MvPolynomial.eval₂Hom_X`, `MvPolynomial.hom_C`, `NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply`, `IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime_pow`, `WittVector.aeval_verschiebung_poly'`, `quadraticChar_card_card`, `Differential.implicitDeriv_C`, `Padic.norm_intCast_eq_one_iff`, `Differential.algHom_deriv`, `jacobiSum_mem_algebraAdjoin_of_pow_eq_one`, `one_le_pow_mul_abs_eval_div`, `AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_symm_apply`, `NumberField.Ideal.inertiaDeg_primesOverSpanEquivMonicFactorsMod_symm_apply'`, `IsCyclotomicExtension.Rat.ncard_primesOver_of_prime_pow`, `ChevalleyThm.chevalley_polynomialC`, `MulChar.apply_mem_algebraAdjoin_of_pow_eq_one`, `IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_apply`, `Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply`, `BoxIntegral.unitPartition.mem_smul_span_iff`, `isCoprime_iff_nat_coprime`, `Zsqrtd.exists_coprime_of_gcd_pos`, `CommRingCat.free_obj_coe`, `Nat.prime_iff_prime_int`, `WittVector.mul_polyOfInterest_aux2`, `quadraticChar_two`, `CommRingCat.free_map_coe`, `MulChar.apply_mem_algebraAdjoin`, `IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one'`, `isCoprime_iff_gcd_eq_one`, `normalize_of_nonneg`, `normUnit_eq`, `ModN.basis_apply_eq_mkQ`, `prime_two`, `ZMod.χ₄_int_mod_four`, `DifferentialAlgebra.deriv_algebraMap`, `LindemannWeierstrass.exp_polynomial_approx`, `IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime_pow`, `Rat.isCoprime_num_den`, `IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_pow_ne_two`, `quadraticChar_dichotomy`, `IsCyclotomicExtension.Rat.ramificationIdx_eq_of_prime`, `IsPrimitiveRoot.adjoinEquivRingOfIntegers_symm_apply`, `ZMod.χ₈'_nat_eq_if_mod_eight`, `RingHom.toIntAlgHom_apply`, `CharP.ker_intAlgebraMap_eq_span`, `instIsGaloisGroupIntRingOfIntegersOfRat`, `Submodule.torsion_int`, `ZMod.χ₈'_int_eq_χ₄_mul_χ₈`, `prime_three`, `IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton_of_prime`, `NonUnitalSubring.unitization_apply`, `CommRingCat.coproductCocone_inl`, `quadraticChar_sum_zero`, `WittVector.mulN_coeff`, `IsPrimitiveRoot.adjoinEquivRingOfIntegers_apply`, `algebraMap.coe_deriv`, `quadraticChar_eq_zero_iff`, `quadraticChar_zero`, `Differential.coeff_mapCoeffs`, `NumberField.RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors`, `PadicInt.coe_adicCompletionIntegersEquiv_symm_apply`, `Algebra.Presentation.coeffs_subset_core`, `Algebra.Presentation.coeffs_relation_subset_core`, `WittVector.wittZSMul_vars`, `IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two'`, `CommRingCat.coproductCocone_inr`, `WittVector.mul_polyOfInterest_aux4`, `WittVector.frobeniusPoly_zmod`, `Representation.norm_ofMulDistribMulAction_eq`, `ZMod.χ₈'_eq_χ₄_mul_χ₈`, `legendreSym.at_two`, `MvPolynomial.eval₂_cast_comp`, `NumberField.Ideal.liesOver_primesOverSpanEquivMonicFactorsMod_symm`, `RingOfIntegers.not_dvd_exponent_iff`, `mem_subalgebraOfSubring`, `quadraticChar_exists_neg_one'`, `WittVector.bind₁_wittMulN_wittPolynomial`, `normalize_coe_nat`, `EisensteinSeries.finGcdMap_div`, `AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly_assoc`, `IsPrimitiveRoot.minpoly_dvd_expand`, `WittVector.IsPoly.poly`, `WittVector.mul_polyOfInterest_vars`, `jacobiSym.at_neg_two`, `Differential.mapCoeffs_monomial`, `ZMod.χ₈_int_mod_eight`, `FiniteField.two_pow_card`, `PadicInt.coe_adicCompletionIntegersEquiv_apply`, `Ideal.relNorm_int`, `AlgebraicGeometry.AffineSpace.map_toSpecMvPoly`, `quadraticChar_neg_two`, `exists_jacobiSum_eq_neg_one_add`, `Differential.mapCoeffs_C`, `WittVector.wittAdd_vars`, `NumberField.integralBasis_repr_apply`, `groupHomology.H1AddEquivOfIsTrivial_single`, `absNorm_under_mem`, `Polynomial.hermite_eq_deriv_gaussian'`, `wittStructureInt_prop`, `CommRingCat.coproductCocone_pt`, `negOnePow_def`, `subalgebraOfSubring_toSubsemiring`, `Polynomial.deriv_gaussian_eq_hermite_mul_gaussian`, `ZMod.χ₄_nat_one_mod_four`, `jacobiSym.neg`, `Subbimodule.coe_toSubbimoduleInt`, `prime_ofNat_iff`, `IsCyclotomicExtension.Rat.ncard_primesOver_of_prime`, `IsCyclotomicExtension.Rat.liesOver_span_zeta_sub_one`, `Rat.isFractionRing`, `wittStructureInt_vars`, `Subbimodule.coe_toSubbimoduleNat`, `ZMod.χ₈_nat_mod_eight`, `WittVector.frobeniusPolyAux_eq`, `Polynomial.hermite_eq_deriv_gaussian`, `Differential.mapCoeffs_X`, `ZMod.coe_int_isUnit_iff_isCoprime`, `WittVector.coeff_frobeniusFun`, `cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt`, `Nat.isCoprime_iff_coprime`, `ZMod.χ₄_int_three_mod_four`, `WittVector.constantCoeff_wittMul`, `groupHomology.H1AddEquivOfIsTrivial_symm_apply`, `PadicInt.norm_intCast_eq_one_iff`, `IsPrimitiveRoot.adjoinEquivRingOfIntegersOfPrimePow_symm_apply`, `normalize_of_nonpos`, `groupHomology.H1ToTensorOfIsTrivial_H1π_single`, `ZMod.χ₄_nat_three_mod_four`, `IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two`, `Differential.algHom_deriv'`, `AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_apply`, `Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply`, `coe_gcd`, `ZMod.χ₄_apply`, `RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply`, `absNorm_under_dvd_absNorm`, `WittVector.mul_polyOfInterest_aux1`, `WittVector.wittSub_vars`, `Rat.isLocalizationIsInteger_iff`, `exists_prime_and_dvd`, `ZMod.χ₄_int_one_mod_four`, `MvPolynomial.counit_surjective`, `quadraticChar_eq_one_of_char_two`, `WittVector.wittPow_vars`, `ZMod.χ₄_eq_neg_one_pow`, `abs_eq_normalize`, `natAbs_gcd`, `WittVector.constantCoeff_wittAdd`, `jacobiSym.at_two`, `quadraticChar_sq_one`, `CommRingCat.coproductCoconeIsColimit_desc`, `witt_structure_prop`, `WittVector.constantCoeff_wittNSMul`, `WittVector.bind₁_verschiebungPoly_wittPolynomial`, `groupHomology.H1AddEquivOfIsTrivial_apply`, `WittVector.coeff_select`, `legendreSym.at_neg_one`, `Rat.int_algebraMap_injective`, `quadraticChar_odd_prime`, `NonUnitalSubring.unitization_range`, `NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply_eq_span`, `Differential.deriv_aeval_eq`, `Surreal.dyadicMap_apply`, `RingOfIntegers.exponent_eq_one_iff`, `WittVector.polyOfInterest_vars`, `WittVector.wittMul_zero`, `WittVector.polyOfInterest_vars_eq`, `Differential.logDeriv_eq_zero`, `WittVector.wittNeg_zero`, `quadraticChar_sq_one'`, `WittVector.map_frobeniusPoly`, `WittVector.constantCoeff_wittZSMul`, `Rat.int_algebraMap_surjective`, `IsCyclotomicExtension.Rat.map_eq_span_zeta_sub_one_pow`, `IsCyclotomicExtension.Rat.ramificationIdx_of_not_dvd`, `WittVector.bind₁_onePoly_wittPolynomial`, `FractionalIdeal.abs_det_basis_change`, `WittVector.wittOne_zero_eq_one`, `IsCyclotomicExtension.Rat.ramificationIdx_eq_of_not_dvd`, `Ideal.span_singleton_absNorm`, `uzpow_intCast`, `AlgebraicGeometry.AffineSpace.over_over`, `IsCyclotomicExtension.Rat.adjoin_singleton_eq_top`, `ZMod.χ₈'_apply`, `coe_lcm`, `AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv_comp`, `NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply`, `quadraticChar_apply`, `AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly`, `Differential.implicitDeriv_X`, `RingHom.toIntAlgHom_coe`, `legendreSym.at_neg_two`, `ZMod.χ₄_int_eq_if_mod_four`, `IsPrimitiveRoot.self_sub_one_pow_dvd_order`, `natAbs_lcm`, `algebraMap_int_eq`, `IsCyclotomicExtension.Rat.ramificationIdx_eq`, `quadraticChar_neg_one_iff_not_isSquare`, `Differential.algEquiv_deriv'`, `quadraticChar_eq_pow_of_char_ne_two`, `WittVector.wittNSMul_vars`, `quadraticChar_eq_pow_of_char_ne_two'`, `cyclotomic_comp_X_add_one_isEisensteinAt`, `ZMod.χ₄_nat_mod_four`, `Representation.ofMulDistribMulAction_apply_apply`, `prime_iff_natAbs_prime`, `instIsLocalizationIntPosRat`, `WittVector.mul_polyOfInterest_aux5`, `int_algebra_subsingleton`, `MvPolynomial.counit_C`, `quadraticChar_neg_one`, `IsPrimitiveRoot.arg`, `WittVector.aeval_verschiebungPoly`, `fermatLastTheoremWith'_nat_int_tfae`, `Fermat42.coprime_of_minimal`, `ZMod.χ₈_nat_eq_if_mod_eight`, `WittVector.mul_polyOfInterest_aux3`, `jacobiSym.at_neg_one`, `WittVector.verschiebungPoly_zero`, `MvPolynomial.C_dvd_iff_zmod`, `Polynomial.shiftedLegendre_eval_symm`, `WittVector.wittOne_pos_eq_zero`, `wittStructureInt_rename`, `WittVector.constantCoeff_wittNeg`, `map_wittStructureInt`, `ModN.instModuleFinite`, `NumberField.instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype`, `absNorm_under_eq_sInf`, `IsCyclotomicExtension.Rat.isIntegralClosure_adjoin_singleton`, `mem_nonUnitalSubalgebraOfNonUnitalSubring`, `cast_mem_ideal_iff`, `quadraticChar_eq_neg_one_iff_not_one`, `Tactic.NormNum.int_not_isCoprime_helper`, `WittVector.coeff_frobenius`, `groupHomology.H1AddEquivOfIsTrivial_symm_tmul`, `WittVector.wittNeg_vars`, `Ideal.ringChar_quot`, `WittVector.wittSub_zero`, `WittVector.wittZero_eq_zero`, `liesOver_span_absNorm`, `RingHom.toIntAlgHom_injective`, `Algebra.Presentation.instFiniteTypeIntCoreOfFinite`, `Surreal.dyadicMap_apply_pow`, `Algebra.adjoin_int`, `ZMod.χ₈_apply`, `constantCoeff_wittStructureInt_zero`, `CommRingCat.coproductCocone_ι`, `WittVector.wittPolyProd_vars`, `Differential.algEquiv_deriv`, `NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply`, `IsCyclotomicExtension.Rat.ramificationIdx_span_zeta_sub_one`, `Nat.absNorm_under_prime`, `Nat.Coprime.isCoprime`, `nonneg_iff_normalize_eq_self`, `WittVector.wittAdd_zero`, `quadraticChar_one_iff_isSquare`, `quadraticChar_exists_neg_one`, `EisensteinSeries.mem_gammaSet_one`, `WittVector.wittPolyProdRemainder_vars`, `ZMod.χ₄_nat_eq_if_mod_four`, `ZMod.χ₈_int_eq_if_mod_eight`, `WittVector.wittMul_vars`, `WittVector.constantCoeff_wittSub`, `MvPolynomial.counit_X`
`instDistrib` 📖	CompOp	—
`instRing` 📖	CompOp	808 math math: `HomotopyCategory.spectralObjectMappingCone_δ'_app`, `Num.cast_to_int`, `CategoryTheory.InjectiveResolution.Hom.hom'_f`, `DerivedCategory.instIsLocalizationCochainComplexIntQQuasiIsoUp`, `CategoryTheory.ShortComplex.ShortExact.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoX₃CochainComplexMapSingleFunctorOfNatX₁`, `ComplexShape.embeddingUpIntDownInt_f`, `CochainComplex.triangleOfDegreewiseSplit_obj₁`, `CochainComplex.mappingConeCompTriangleh_comm₁_assoc`, `CochainComplex.HomComplex.Cochain.rightShiftAddEquiv_symm_apply`, `Polynomial.ascPochhammer_smeval_neg_eq_descPochhammer`, `CochainComplex.HomComplex.Cochain.fromSingleMk_neg`, `CochainComplex.mappingCone.δ_inl`, `CochainComplex.mappingCone.inl_v_descCochain_v_assoc`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_neg`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_add`, `DerivedCategory.right_fac`, `CochainComplex.HomComplex.Cocycle.leftShiftAddEquiv_symm_apply`, `CochainComplex.mappingCone.inr_f_d_assoc`, `NumberField.Units.logEmbedding_fundSystem`, `CochainComplex.HomComplex.Cochain.δ_single`, `CochainComplex.mappingConeCompTriangle_obj₂`, `CochainComplex.HomComplex.Cocycle.equivHom_symm_apply`, `CochainComplex.isStrictlyGE_shift`, `floor_int`, `Nat.Ioc_filter_modEq_cast`, `CochainComplex.mappingCone.id`, `NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne`, `CochainComplex.shiftFunctorZero_eq`, `Rat.padicValuation_cast`, `CategoryTheory.InjectiveResolution.ι'_f_zero`, `CochainComplex.mappingCone.liftCochain_v_snd_v_assoc`, `Polynomial.cyclotomic.irreducible`, `CochainComplex.mappingCone.inr_f_fst_v`, `CochainComplex.isStrictlyLE_iff`, `CochainComplex.HomComplex.Cochain.leftShift_smul`, `ZMod.intCast_cast_neg`, `CochainComplex.HomComplex.Cochain.fromSingleEquiv_fromSingleMk`, `CochainComplex.mappingCone.triangle_mor₁`, `ArithmeticFunction.intCoe_one`, `HomologicalComplex₂.shiftFunctor₂XXIso_refl`, `CochainComplex.mappingCone.liftCochain_v_snd_v`, `CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₂`, `ComplexShape.instIsTruncLENatIntEmbeddingUpIntLE`, `ArithmeticFunction.intCoe_int`, `CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₃`, `CochainComplex.instIsStrictlyLEObjHomologicalComplexIntUpSingle`, `DerivedCategory.instCommShiftHomologicalComplexIntUpHomFunctorQuotientCompQhIso`, `Module.Basis.ofZLatticeBasis_apply`, `CategoryTheory.DifferentialObject.d_squared_apply`, `padicValuation_lt_one_iff`, `CochainComplex.HomComplex.Cocycle.equivHomShift_symm_postcomp`, `ComplexShape.instIsRelIffNatIntEmbeddingUpIntLE`, `CochainComplex.instLinearIntFunctorSingleFunctors`, `CochainComplex.mapBifunctorShift₂Iso_hom_naturality₂_assoc`, `ZMod.intCast_cast_mul`, `Module.Basis.ofZLatticeComap_apply`, `CochainComplex.mappingCone.d_snd_v`, `CochainComplex.HomComplex.Cochain.rightUnshift_neg`, `ZMod.intCast_cast_add`, `CochainComplex.HomComplex.Cochain.δ_fromSingleMk`, `Rat.isInt_intFloor`, `CochainComplex.HomComplex.Cochain.map_v`, `Nat.ceil_int`, `CategoryTheory.Functor.commShiftIso_map₂CochainComplex_flip_hom_app`, `CochainComplex.ConnectData.map_comp_map`, `AbsoluteValue.abs_isEuclidean`, `CochainComplex.HomComplex.leftHomologyData_K_coe`, `CochainComplex.mappingConeCompTriangle_mor₃`, `CochainComplex.HomComplex.Cochain.shift_add`, `CochainComplex.HomComplex.Cochain.comp_id`, `Ring.choose_eq_smul`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_add`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_sub`, `CategoryTheory.ProjectiveResolution.cochainComplex_d`, `padicValuation_eq_one_iff`, `CochainComplex.HomComplex.Cochain.toSingleMk_neg`, `CochainComplex.HomComplex.Cochain.ofHom_v_comp_d`, `CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂_assoc`, `CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁_assoc`, `CochainComplex.shiftShortComplexFunctorIso_add'_hom_app`, `CochainComplex.HomComplex.Cochain.map_zero`, `ModuleCat.forget₂_addCommGrp_essSurj`, `CochainComplex.cm5b.fac`, `DerivedCategory.singleFunctorsPostcompQIso_inv_hom`, `CochainComplex.instIsCompatibleWithShiftHomologicalComplexIntUpQuasiIso`, `CochainComplex.HomComplex.Cochain.toSingleMk_v`, `CochainComplex.HomComplex.leftHomologyData'_i`, `CochainComplex.IsKInjective.rightOrthogonal`, `CochainComplex.ConnectData.cochainComplex_X`, `ZMod.cast_add_eq_ite`, `CochainComplex.IsKInjective.Qh_map_bijective`, `ComplexShape.Embedding.embeddingUpInt_areComplementary`, `CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv_apply`, `CochainComplex.HomComplex.Cochain.shift_neg`, `HomotopyCategory.instIsHomologicalIntUpHomologyFunctor`, `Finset.prod_indicator_biUnion_finset_sub_indicator`, `ZNum.gcd_to_nat`, `DerivedCategory.subsingleton_hom_of_isStrictlyLE_of_isStrictlyGE`, `Profinite.NobelingProof.GoodProducts.linearIndependent_comp_of_eval`, `CochainComplex.ι_mapBifunctorShift₂Iso_hom_f_assoc`, `CochainComplex.homotopyUnop_hom_eq`, `CochainComplex.HomComplex.Cochain.toSingleMk_add`, `CochainComplex.mappingCone.inr_f_d`, `Mathlib.Meta.NormNum.IsInt.raw_refl`, `ModN.basis_apply_eq_mkQ`, `CochainComplex.HomComplex.δ_v`, `CochainComplex.instIsStrictlyGEObjHomologicalComplexIntUpSingle`, `CochainComplex.HomComplex.Cochain.comp_v`, `ZLattice.comap_toAddSubgroup`, `ArithmeticFunction.coe_coe`, `CochainComplex.HomComplex.Cochain.comp_zero_cochain_v`, `HomologicalComplex.dgoToHomologicalComplex_obj_d`, `CochainComplex.mappingCone.inr_f_descShortComplex_f_assoc`, `CochainComplex.HomComplex.Cochain.neg_v`, `CochainComplex.HomComplex.Cocycle.equivHomShift'_symm_apply`, `ZLattice.module_finite`, `CochainComplex.HomComplex.Cochain.sub_v`, `CochainComplex.mappingCone.liftCochain_v_descCochain_v`, `CochainComplex.mappingCone.lift_f_fst_v`, `CochainComplex.mappingCone.inl_v_triangle_mor₃_f`, `PeriodPair.latticeBasis_zero`, `CochainComplex.XIsoOfEq_shift`, `CochainComplex.HomComplex.Cochain.rightUnshift_comp`, `CochainComplex.HomComplex.Cochain.rightUnshift_units_smul`, `ComplexShape.eulerCharSignsUpInt_χ`, `HomologicalComplex.dgoEquivHomologicalComplex_unitIso`, `CochainComplex.mappingCone.inr_triangleδ`, `AddAction.orbitZMultiplesEquiv_symm_apply`, `RootPairing.finrank_corootSpanIn_int`, `CochainComplex.HomComplex.Cochain.ofHoms_comp`, `ModuleCat.forget₂_addCommGroup_full`, `CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_eq`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_sub`, `ArithmeticFunction.moebius_mul_coe_zeta`, `CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₁`, `CochainComplex.HomComplex.leftHomologyData_π_hom_apply`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_sub`, `CochainComplex.instIsStrictlyLEExtendNatIntEmbeddingDownNatOfNat`, `ZLattice.rank`, `ZSpan.quotientEquiv_apply_mk`, `CochainComplex.mappingCone.id_X`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_mk_hom`, `CochainComplex.HomComplex.Cochain.single_zero`, `CochainComplex.mappingCone.inr_descShortComplex_assoc`, `Rat.isNat_intCeil_ofIsNNRat`, `ZNum.cmp_to_int`, `CochainComplex.mappingConeCompHomotopyEquiv_comm₂_assoc`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_sub`, `Profinite.NobelingProof.succ_exact`, `CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id`, `CochainComplex.HomComplex.leftHomologyData_i_hom_apply`, `HomotopyCategory.instAdditiveIntUpShiftFunctor`, `CochainComplex.HomComplex.Cochain.fromSingleMk_postcomp`, `Submodule.torsion_int`, `CochainComplex.mappingCone.d_snd_v'_assoc`, `instIsLocalizationHomologicalComplexIntUpHomotopyCategoryQuotientHomotopyEquivalences`, `CochainComplex.HomComplex.Cochain.shift_zero`, `CategoryTheory.Functor.instCommShiftHomotopyCategoryIntUpDerivedCategoryHomMapDerivedCategoryFactorsh`, `ZNum.mod_to_int`, `CochainComplex.shiftFunctorZero_inv_app_f`, `ceil_int`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_zero`, `CochainComplex.HomComplex.Cochain.leftShift_comp`, `CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_symm_apply`, `RootPairing.finrank_rootSpanIn_int`, `NumberField.Units.span_basisOfIsMaxRank`, `CochainComplex.triangleOfDegreewiseSplit_obj₂`, `CochainComplex.HomComplex.Cochain.zero_cochain_comp_v`, `CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id_assoc`, `CochainComplex.g_shortComplexTruncLEX₃ToTruncGE`, `CochainComplex.homologyFunctor_shift`, `DerivedCategory.instIsTriangulatedHomotopyCategoryIntUpQh`, `CochainComplex.HomComplex.Cochain.toSingleMk_v_eq_zero`, `CochainComplex.isKInjective_shift_iff`, `Submodule.span_int_eq`, `CochainComplex.isStrictlyGE_iff`, `ZLattice.covolume_div_covolume_eq_relIndex`, `Polynomial.hermite_succ`, `Polynomial.sub_one_pow_totient_lt_natAbs_cyclotomic_eval`, `CochainComplex.HomComplex.Cochain.leftShift_rightShift_eq_negOnePow_rightShift_leftShift`, `NonUnitalSubring.unitization_apply`, `HomologicalComplex.dgoEquivHomologicalComplexUnitIso_hom_app_f`, `CochainComplex.mappingCone.lift_f_fst_v_assoc`, `ZLattice.comap_equiv_apply`, `Polynomial.hermite_eq_iterate`, `Polynomial.sub_one_lt_natAbs_cyclotomic_eval`, `DerivedCategory.to_singleFunctor_obj_eq_zero_of_injective`, `DerivedCategory.right_fac_of_isStrictlyLE_of_isStrictlyGE`, `Module.Basis.addSubgroupOfClosure_repr_apply`, `CochainComplex.HomComplex.Cochain.leftShift_rightShift`, `ComplexShape.embeddingUpNat_f`, `CochainComplex.HomComplex.Cochain.ofHom_neg`, `descPochhammer_eval_cast`, `CochainComplex.isSplitEpi_to_singleFunctor_obj_of_projective`, `CochainComplex.HomComplex.Cochain.zero_v`, `DerivedCategory.instLinearCochainComplexIntQ`, `Polynomial.int_cyclotomic_rw`, `HomologicalComplex.dgoEquivHomologicalComplex_functor`, `ComplexShape.instIsTruncGENatIntEmbeddingUpIntGE`, `CochainComplex.isZero_of_isStrictlyLE`, `card_box`, `LaurentSeries.derivative_iterate_coeff`, `Rat.isNat_intCeil`, `divisorsAntidiag_natCast`, `Nat.floor_int`, `CochainComplex.instAdditiveIntFunctorSingleFunctors`, `CochainComplex.shiftFunctor_obj_X`, `CochainComplex.mappingConeCompHomotopyEquiv_comm₁`, `Submodule.finiteQuotient_iff`, `Ioo_eq_finset_map`, `HomotopyCategory.mappingCone_triangleh_distinguished`, `CochainComplex.mappingCone.rotateHomotopyEquiv_comm₂`, `AddSubgroup.toIntSubmodule_symm`, `CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂`, `meromorphicOrderAt_id`, `CochainComplex.HomComplex.Cochain.map_add`, `CochainComplex.homologySequenceδ_quotient_mapTriangle_obj_assoc`, `CategoryTheory.ProjectiveResolution.extMk_hom`, `CochainComplex.mappingCone.triangleRotateShortComplex_X₂`, `CochainComplex.HomComplex.Cochain.fromSingleMk_v`, `Polynomial.descPochhammer_smeval_eq_descFactorial`, `CochainComplex.HomComplex.Cochain.fromSingleMk_add`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_neg`, `CochainComplex.HomComplex.Cochain.shift_smul`, `CochainComplex.HomComplex.Cochain.leftShiftAddEquiv_apply`, `CochainComplex.HomComplex.Cochain.ofHomotopy_refl`, `CategoryTheory.ProjectiveResolution.Hom.hom'_f_assoc`, `HomologicalComplex.dgoToHomologicalComplex_obj_X`, `CochainComplex.mappingCone.ext_from_iff`, `CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe`, `CochainComplex.shiftShortComplexFunctor'_hom_app_τ₁`, `Polynomial.X_pow_sub_X_sub_one_irreducible`, `DerivedCategory.instIsIsoMapCochainComplexIntQ`, `ModEq.listProd_map`, `ZNum.le_to_int`, `CochainComplex.HomComplex.Cocycle.toSingleMk_zero`, `CochainComplex.HomComplex.Cochain.rightShiftAddEquiv_apply`, `CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv`, `CochainComplex.HomComplex.Cochain.leftUnshift_v`, `CochainComplex.mappingConeCompHomotopyEquiv_comm₁_assoc`, `AddAction.zmultiplesQuotientStabilizerEquiv_symm_apply`, `CochainComplex.ConnectData.map_f`, `CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₂`, `CharacterModule.intSpanEquivQuotAddOrderOf_apply`, `CochainComplex.mappingCone.triangleRotateShortComplex_X₃`, `CochainComplex.HomComplex.Cochain.rightShift_leftShift`, `instQFactorsThroughHomotopyIntUp`, `CochainComplex.HomComplex.Cochain.ofHom_v`, `CochainComplex.HomComplex.Cochain.ofHom_sub`, `CochainComplex.instLinearHomologicalComplexIntUpShiftFunctor`, `fract_int`, `DerivedCategory.instAdditiveHomotopyCategoryIntUpQh`, `PosNum.cast_to_int`, `CochainComplex.HomComplex.Cochain.leftUnshift_smul`, `CochainComplex.mappingCone.inr_f_snd_v`, `CochainComplex.instIsKInjectiveObjIntShiftFunctor`, `CochainComplex.mappingConeCompTriangle_mor₃_naturality`, `CategoryTheory.Functor.instCommShiftCochainComplexIntDerivedCategoryHomMapDerivedCategoryFactors`, `Rat.isInt_intCeil`, `CochainComplex.HomComplex.Cochain.shiftLinearMap_apply`, `Submodule.span_singleton_toAddSubgroup_eq_zmultiples`, `CategoryTheory.ProjectiveResolution.π'_f_zero_assoc`, `DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhQuasiIso`, `Mathlib.Tactic.Ring.natCast_int`, `HomologicalComplex₂.shiftFunctor₁XXIso_refl`, `CochainComplex.mappingCone.triangleRotateShortComplex_X₁`, `DerivedCategory.left_fac_of_isStrictlyLE_of_isStrictlyGE`, `CochainComplex.shiftFunctor_map_f'`, `CochainComplex.mappingCone.ext_to_iff`, `CochainComplex.ConnectData.restrictionLEIso_inv_f`, `CategoryTheory.ProjectiveResolution.Hom.hom'_comp_π'`, `CochainComplex.HomComplex.Cochain.rightShift_zero`, `CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₃`, `CategoryTheory.ProjectiveResolution.Hom.hom'_f`, `Ring.descPochhammer_smeval_add`, `CochainComplex.singleFunctor_obj_d`, `Profinite.NobelingProof.factors_prod_eq_basis_of_ne`, `CochainComplex.quasiIso_shift_iff`, `CochainComplex.HomComplex.Cochain.rightUnshift_v`, `HomotopyCategory.composableArrowsFunctor_obj`, `ComplexShape.instIsRelIffNatIntEmbeddingDownNat`, `CochainComplex.shiftShortComplexFunctor'_hom_app_τ₂`, `CochainComplex.shiftFunctorAdd'_inv_app_f'`, `CochainComplex.exactAt_of_isLE`, `DerivedCategory.instHasLeftCalculusOfFractionsHomotopyCategoryIntUpQuasiIso`, `CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_inv_f_f`, `ModEq.listProd_map_one`, `ZMod.intCast_comp_cast`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_zero`, `descPochhammer_eq_ascPochhammer`, `ZLattice.module_free`, `CochainComplex.mappingCone.map_inr`, `Num.cast_ofZNum`, `CategoryTheory.Functor.mapCochainComplexShiftIso_inv_app_f`, `CochainComplex.shiftFunctorAdd'_eq`, `CochainComplex.shiftFunctorAdd'_inv_app_f`, `HomotopyCategory.instLinearIntUpShiftFunctor`, `CochainComplex.mappingCone.liftCochain_v_fst_v`, `CochainComplex.mapBifunctorShift₂Iso_hom_naturality₂`, `CochainComplex.HomComplex.Cochain.fromSingleMk_zero`, `CochainComplex.mappingCone.decomp_from`, `CochainComplex.mappingCone.inl_v_triangle_mor₃_f_assoc`, `Submodule.toAddSubgroup_toIntSubmodule`, `HomotopyCategory.Pretriangulated.distinguished_cocone_triangle`, `Submodule.natAbs_det_equiv`, `CochainComplex.mappingConeCompTriangle_mor₁`, `CochainComplex.mappingCone.inr_triangleδ_assoc`, `CochainComplex.cm5b.instIsStrictlyGEBiprodIntMappingConeIdIOfHAddOfNat`, `CochainComplex.HomComplex.Cochain.leftShift_zero`, `CochainComplex.mappingCone.inl_v_snd_v_assoc`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_zero`, `CategoryTheory.ProjectiveResolution.Hom.hom'_comp_π'_assoc`, `Icc_eq_finset_map`, `Submodule.span_int_eq_addSubgroup_closure`, `CochainComplex.instLinearIntShiftFunctor`, `ZSpan.isAddFundamentalDomain'`, `CochainComplex.triangleOfDegreewiseSplit_mor₂`, `Submodule.fg_iff_addSubgroup_fg`, `ZMod.intCast_cast_sub`, `HomologicalComplex.dgoEquivHomologicalComplex_counitIso`, `HomotopyCategory.instLinearIntUpSingleFunctor`, `CochainComplex.HomComplex.Cochain.ofHoms_v_comp_d`, `CochainComplex.mappingCone.inr_f_triangle_mor₃_f`, `DerivedCategory.isLE_Q_obj_iff`, `CochainComplex.cm5b.fac_assoc`, `ComplexShape.eulerCharSignsDownInt_χ`, `HomotopyCategory.instAdditiveIntUpSingleFunctor`, `PosNum.to_int_eq_succ_pred`, `CochainComplex.mapBifunctorHomologicalComplexShift₂Iso_hom_f_f`, `CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv`, `CochainComplex.triangleOfDegreewiseSplit_obj₃`, `CochainComplex.shiftFunctorZero'_hom_app_f`, `HomotopyCategory.Pretriangulated.contractible_distinguished`, `instModuleFinite_of_discrete_submodule`, `ComplexShape.instIsRelIffNatIntEmbeddingUpIntGE`, `ComplexShape.instIsRelIffIntEmbeddingDownIntUpInt`, `padicValuation_self`, `CochainComplex.mappingCone.triangle_mor₂`, `CochainComplex.HomComplex.Cocycle.leftUnshift_coe`, `CochainComplex.HomComplex.Cochain.equivHomotopy_apply_of_eq`, `Ioc_eq_finset_map`, `CochainComplex.MappingConeCompHomotopyEquiv.hom_inv_id`, `PeriodPair.order_weierstrassP`, `CochainComplex.mappingCone.d_snd_v_assoc`, `CochainComplex.instAdditiveIntShiftFunctor`, `CategoryTheory.HasExt.hasSmallLocalizedShiftedHom_of_isLE_of_isGE`, `CochainComplex.shiftFunctor_map_f`, `CochainComplex.quasiIsoAt_shift_iff`, `CochainComplex.mappingCone.d_snd_v'`, `CochainComplex.HomComplex.Cocycle.equivHomShift_symm_apply`, `CochainComplex.instIsKProjectiveObjIntShiftFunctor`, `Rat.isNat_intFloor`, `CategoryTheory.HasExt.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoOfIsGEOfIsLEOfNat`, `Num.ofZNum_toNat`, `CochainComplex.HomComplex.Cochain.rightShift_smul`, `CochainComplex.HomComplex.Cochain.map_comp`, `Nat.Ico_filter_modEq_cast`, `Polynomial.cyclotomic_dvd_of_mahlerMeasure_eq_one`, `CochainComplex.homotopyOp_hom_eq`, `CochainComplex.mappingCone.inr_f_descCochain_v_assoc`, `CochainComplex.HomComplex.Cochain.map_sub`, `CochainComplex.HomComplex.Cocycle.homOf_f`, `CochainComplex.IsKProjective.Qh_map_bijective`, `CochainComplex.mappingCone.d_fst_v_assoc`, `CochainComplex.homOfDegreewiseSplit_f`, `CochainComplex.shiftFunctorAdd_inv_app_f`, `ComplexShape.boundaryGE_embeddingUpIntGE_iff`, `DerivedCategory.isGE_Q_obj_iff`, `CochainComplex.mappingCone.map_id`, `CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₁`, `CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₂`, `CategoryTheory.Functor.commShiftIso_map₂CochainComplex_inv_app`, `CochainComplex.mappingConeCompTriangle_obj₃`, `IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomic`, `MulAction.orbitZPowersEquiv_symm_apply`, `DerivedCategory.instEssSurjHomotopyCategoryIntUpQh`, `CategoryTheory.ProjectiveResolution.π'_f_zero`, `Submodule.span_int_eq_addSubgroupClosure`, `CochainComplex.mappingCone.inl_v_fst_v`, `DivisibleHull.qsmul_def`, `Rat.IsRat.isInt_round`, `CochainComplex.isLE_iff`, `CochainComplex.ConnectData.cochainComplex_d`, `PeriodPair.latticeBasis_one`, `ZLattice.covolume_eq_det_mul_measureReal`, `HomotopyCategory.instIsTriangulatedIntUpSubcategoryAcyclic`, `descPochhammer_int_eq_ascFactorial`, `HomologicalComplex.homologicalComplexToDGO_map_f`, `CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_inv_app_f`, `SignType.intCast_cast`, `CochainComplex.exists_iso_single`, `CochainComplex.HomComplex.Cocycle.rightShiftAddEquiv_symm_apply`, `CochainComplex.HomComplex.Cochain.shift_units_smul`, `HomotopyCategory.instIsTriangulatedIntUp`, `CochainComplex.ConnectData.restrictionLEIso_hom_f`, `CochainComplex.exactAt_of_isGE`, `CochainComplex.shiftFunctorAdd_eq`, `DerivedCategory.instFaithfulFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh`, `CochainComplex.HomComplex.Cochain.leftShiftLinearEquiv_symm_apply`, `CochainComplex.mappingCone.inr_f_descCochain_v`, `CochainComplex.ι_mapBifunctorShift₂Iso_hom_f`, `CochainComplex.cm5b.instQuasiIsoIntP`, `CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₃`, `cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt`, `ZLattice.exists_forall_abs_repr_le_norm`, `CategoryTheory.DifferentialObject.objEqToHom_d`, `CochainComplex.mappingCone.triangleMapOfHomotopy_comm₂_assoc`, `CategoryTheory.DifferentialObject.eqToHom_f'`, `CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_inv_hom₁`, `CochainComplex.mappingCone.isZero_X_iff`, `uIcc_eq_finset_map`, `Ideal.span_singleton_toAddSubgroup_eq_zmultiples`, `Profinite.NobelingProof.GoodProducts.square_commutes`, `Subgroup.transferTransversal_apply'`, `DerivedCategory.instIsGEObjCochainComplexIntQOfIsGE`, `CochainComplex.mappingConeCompHomotopyEquiv_comm₂`, `CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom_assoc`, `existsUnique_mem_box`, `exists_signed_sum'`, `CochainComplex.HomComplex.δ_zero_cochain_v`, `CochainComplex.HomComplex.Cochain.units_smul_v`, `CochainComplex.HomComplex.Cochain.δ_toSingleMk`, `CochainComplex.cm5b.instMonoFIntI`, `CochainComplex.HomComplex.CohomologyClass.toHom_bijective`, `ZMod.intCast_rightInverse`, `CochainComplex.HomComplex.Cochain.fromSingleMk_precomp`, `Polynomial.factorial_mul_shiftedLegendre_eq`, `Rat.isInt_round`, `CochainComplex.HomComplex.Cochain.leftUnshift_add`, `CochainComplex.isGE_iff`, `CochainComplex.HomComplex.Cocycle.fromSingleMk_zero`, `CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃_assoc`, `HomotopyCategory.instIsCompatibleWithShiftHomologicalComplexIntUpHomotopic`, `CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom`, `CochainComplex.mappingCone.inr_f_fst_v_assoc`, `CategoryTheory.ProjectiveResolution.instProjectiveXIntCochainComplex`, `CategoryTheory.DifferentialObject.objEqToHom_refl`, `CategoryTheory.InjectiveResolution.ι'_f_zero_assoc`, `Mathlib.Meta.NormNum.isInt_jacobiSymNat`, `CochainComplex.mappingCone.inl_v_d_assoc`, `CochainComplex.shiftFunctorZero'_inv_app_f`, `CochainComplex.mappingCone.cocycleOfDegreewiseSplit_triangleRotateShortComplexSplitting_v`, `CochainComplex.HomComplex.Cochain.rightShift_units_smul`, `CochainComplex.isZero_of_isStrictlyGE`, `CategoryTheory.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoObjCochainComplexCompSingleFunctorOfNatOfHasExt`, `HomologicalComplex.dgoToHomologicalComplex_map_f`, `DerivedCategory.exists_iso_Q_obj_of_isGE_of_isLE`, `PeriodPair.latticeEquiv_symm_apply`, `HomotopyCategory.instIsTriangulatedIntUpMapHomotopyCategory`, `LaurentPolynomial.toLaurent_support`, `CochainComplex.HomComplex.Cochain.rightUnshift_smul`, `cast_list_prod`, `HomotopyCategory.composableArrowsFunctor_map`, `CochainComplex.HomComplex.Cocycle.equivHomShift'_apply`, `CochainComplex.instQuasiIsoIntMapHomologicalComplexUpShiftFunctor`, `DerivedCategory.instEssSurjArrowHomotopyCategoryIntUpMapArrowQh`, `CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom'_assoc`, `CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃_assoc`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_add`, `MulAction.zpowersQuotientStabilizerEquiv_symm_apply`, `AddCommGrpCat.injective_as_module_iff`, `CochainComplex.HomComplex.Cochain.smul_v`, `CochainComplex.isSplitMono_from_singleFunctor_obj_of_injective`, `CochainComplex.mappingCone.triangleRotateShortComplexSplitting_r`, `HomotopyCategory.quasiIso_eq_subcategoryAcyclic_W`, `ZNum.abs_to_nat`, `CategoryTheory.InjectiveResolution.Hom.hom'_f_assoc`, `CochainComplex.HomComplex.Cochain.δ_shift`, `CochainComplex.shiftShortComplexFunctor'_hom_app_τ₃`, `CochainComplex.HomComplex.Cochain.fromSingleMk_sub`, `CochainComplex.mappingCone.inl_v_descShortComplex_f_assoc`, `CochainComplex.IsKProjective.leftOrthogonal`, `DerivedCategory.from_singleFunctor_obj_eq_zero_of_projective`, `DerivedCategory.exists_iso_Q_obj_of_isGE`, `CategoryTheory.Functor.commShiftIso_map₂CochainComplex_flip_inv_app`, `CochainComplex.cm5b.instInjectiveXIntI`, `CochainComplex.cm5b.instMonoIntI`, `CategoryTheory.ProjectiveResolution.extAddEquivCohomologyClass_apply`, `ComplexShape.instIsRelIffNatIntEmbeddingUpNat`, `Rat.isNat_intFloor_ofIsNNRat`, `Polynomial.map_cyclotomic_int`, `ZNum.to_of_int`, `Mathlib.Meta.NormNum.isInt_negOfNat`, `CochainComplex.isKProjective_iff_leftOrthogonal`, `CategoryTheory.InjectiveResolution.extMk_hom`, `CategoryTheory.InjectiveResolution.cochainComplex_d_assoc`, `ZSpan.quotientEquiv.symm_apply`, `CochainComplex.shortComplexTruncLE_shortExact`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_zero`, `CochainComplex.cm5b.i_f_comp`, `CochainComplex.HomComplex.Cochain.δ_rightUnshift`, `CochainComplex.mappingCone.inr_snd`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_neg`, `CochainComplex.mappingCone.decomp_to`, `CochainComplex.HomComplex.leftHomologyData_H_coe`, `CochainComplex.HomComplex.leftHomologyData'_K_coe`, `Rat.isNat_round`, `CochainComplex.HomComplex.Cochain.leftUnshift_units_smul`, `CochainComplex.mappingCone.inl_fst`, `CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv_apply`, `CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₃`, `CochainComplex.HomComplex.Cocycle.shift_coe`, `meromorphicOrderAt_pow`, `Matrix.num_one`, `ComplexShape.embeddingUpIntLE_f`, `NonUnitalSubring.unitization_range`, `CochainComplex.mappingCone.liftCochain_v_fst_v_assoc`, `HomologicalComplex.dgoEquivHomologicalComplexCounitIso_hom_app_f`, `HomotopyCategory.mem_subcategoryAcyclic_iff`, `CochainComplex.isStrictlyLE_shift`, `CochainComplex.ConnectData.restrictionGEIso_inv_f`, `ZSpan.instDiscreteTopologySubtypeMemAddSubgroupToAddSubgroupIntSpanRangeCoeBasisRealOfFinite`, `CochainComplex.instFullIntSingleFunctor`, `CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₁`, `CochainComplex.HomComplex.Cochain.δ_rightShift`, `DerivedCategory.right_fac_of_isStrictlyLE`, `CochainComplex.ConnectData.map_id`, `Padic.comap_mulValuation_eq_int_padicValuation`, `CochainComplex.HomComplex.Cochain.leftShift_v`, `CochainComplex.mappingCone.d_fst_v'_assoc`, `CochainComplex.HomComplex.Cochain.rightUnshift_add`, `CochainComplex.HomComplex.Cochain.toSingleMk_zero`, `CochainComplex.homologySequenceδ_quotient_mapTriangle_obj`, `CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_hom_f_f`, `ComplexShape.embeddingDownNat_f`, `HomotopyCategory.homologyFunctor_shiftMap_assoc`, `CochainComplex.mappingCone.inl_v_d`, `CochainComplex.isZero_of_isGE`, `CochainComplex.shiftFunctor_obj_X'`, `HomotopyCategory.distinguished_iff_iso_trianglehOfDegreewiseSplit`, `CochainComplex.HomComplex.Cochain.shift_v`, `ComplexShape.σ_def`, `CochainComplex.shiftFunctorZero_hom_app_f`, `CochainComplex.mappingCone.inr_f_snd_v_assoc`, `CochainComplex.triangleOfDegreewiseSplit_mor₃`, `CochainComplex.shift_f_comp_mappingConeHomOfDegreewiseSplitIso_inv_assoc`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_extMk`, `CochainComplex.HomComplex.Cochain.shiftAddHom_apply`, `ZNum.of_to_int`, `CategoryTheory.InjectiveResolution.instQuasiIsoIntι'`, `CochainComplex.mappingCone.trianglehMapOfHomotopy_hom₂`, `CochainComplex.HomComplex.Cochain.δ_leftUnshift`, `HomotopyCategory.spectralObjectMappingCone_ω₁`, `mem_box`, `CochainComplex.mappingCone.d_fst_v'`, `CochainComplex.shiftFunctorAdd'_hom_app_f'`, `CochainComplex.mappingCone.inl_v_descCochain_v`, `CochainComplex.HomComplex.Cochain.leftShift_add`, `CategoryTheory.DifferentialObject.eqToHom_f'_assoc`, `CochainComplex.HomComplex.Cochain.leftShift_comp_zero_cochain`, `CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃_assoc`, `CochainComplex.shiftEval_hom_app`, `ZNum.div_to_int`, `CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_comp_triangle_mor₃`, `HomologicalComplex.homologicalComplexToDGO_obj_d`, `CochainComplex.instHasMapBifunctorObjIntShiftFunctor_1`, `Module.Baer.of_divisible`, `CochainComplex.HomComplex.Cocycle.equivHomShift_comp`, `Ico_eq_finset_map`, `CochainComplex.cm5b.i_f_comp_assoc`, `CochainComplex.HomComplex_X`, `CochainComplex.instIsStrictlyGEExtendNatIntEmbeddingUpNatOfNat`, `CochainComplex.ConnectData.homologyMap_map_of_eq_succ`, `CochainComplex.HomComplex.leftHomologyData'_H_coe`, `CochainComplex.mappingCone.triangleRotateShortComplex_g`, `CochainComplex.shiftFunctor_obj_d'`, `CochainComplex.instHasMapBifunctorObjIntShiftFunctor`, `ZNum.lt_to_int`, `CochainComplex.HomComplex.Cocycle.equivHom_apply`, `ModEq.listProd_one`, `CategoryTheory.Functor.mapHomologicalComplex_commShiftIso_hom_app_f`, `Submodule.fg_iff_add_subgroup_fg`, `CochainComplex.mappingCone.inr_descShortComplex`, `DerivedCategory.instAdditiveCochainComplexIntQ`, `CochainComplex.ι_mapBifunctorShift₁Iso_hom_f_assoc`, `CochainComplex.cm5b.I_d`, `CochainComplex.triangleOfDegreewiseSplit_mor₁`, `CochainComplex.mappingCone.mapHomologicalComplexXIso'_hom`, `CochainComplex.mapBifunctorHomologicalComplexShift₁Iso_inv_f_f`, `CochainComplex.HomComplex.Cochain.d_comp_ofHom_v`, `HomologicalComplex.homologicalComplexToDGO_obj_obj`, `CochainComplex.HomComplex.Cochain.leftShift_units_smul`, `CochainComplex.HomComplex.Cochain.equivHomotopy_apply_coe`, `AddSubgroup.toIntSubmodule_toAddSubgroup`, `HomotopyCategory.homologyShiftIso_hom_app`, `divisorsAntidiag_ofNat`, `CochainComplex.shiftFunctorAdd_hom_app_f`, `Subgroup.transferFunction_apply`, `ComplexShape.instIsTruncLENatIntEmbeddingDownNat`, `DerivedCategory.Qh_obj_singleFunctors_obj`, `Num.to_nat_to_int`, `CochainComplex.HomComplex.δ_map`, `NumberField.Units.unitLattice_rank`, `Num.ofZNum'_toNat`, `CochainComplex.mapBifunctorShift₁Iso_trans_mapBifunctorShift₂Iso`, `CochainComplex.mappingCone.inl_v_descShortComplex_f`, `ZMod.intCast_zmod_cast`, `CochainComplex.HomComplex.Cochain.d_comp_ofHoms_v`, `CochainComplex.HomComplex.Cochain.toSingleMk_postcomp`, `CochainComplex.HomComplex.Cochain.ofHom_add`, `CochainComplex.mappingCone.triangleRotateShortComplexSplitting_s`, `CochainComplex.mappingCone.inr_f_descShortComplex_f`, `ZLattice.normBound_spec`, `CochainComplex.HomComplex.Cochain.id_comp`, `CategoryTheory.ProjectiveResolution.instQuasiIsoIntπ'`, `CochainComplex.HomComplex.Cochain.single_v_eq_zero'`, `DerivedCategory.exists_iso_Q_obj_of_isLE`, `CategoryTheory.ShortComplex.ShortExact.singleTriangleIso_hom_hom₂`, `CochainComplex.shiftShortComplexFunctor'_inv_app_τ₃`, `CochainComplex.shiftFunctorAdd'_hom_app_f`, `DerivedCategory.instFullFunctorHomotopyCategoryIntUpObjWhiskeringLeftQh`, `CochainComplex.HomComplex.Cochain.ofHom_zero`, `CochainComplex.g_shortComplexTruncLEX₃ToTruncGE_assoc`, `CochainComplex.mappingCone.inr_f_triangle_mor₃_f_assoc`, `CochainComplex.HomComplex.leftHomologyData'_π`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_add`, `NumberField.Units.logEmbeddingEquiv_apply`, `ZNum.cast_to_int`, `Module.Basis.ofZLatticeComap_repr_apply`, `CochainComplex.HomComplex.Cochain.map_ofHom`, `CochainComplex.HomComplex.CohomologyClass.toHom_mk_eq_zero_iff`, `ArithmeticFunction.coe_zeta_mul_moebius`, `CochainComplex.shiftFunctorComm_hom_app_f`, `cyclotomic_comp_X_add_one_isEisensteinAt`, `Profinite.NobelingProof.one_sub_e_mem_of_false`, `Ring.descPochhammer_eq_factorial_smul_choose`, `CochainComplex.mappingCone.inl_v_snd_v`, `Finset.prod_indicator_biUnion_sub_indicator`, `Module.Basis.ofZLatticeBasis_repr_apply`, `CochainComplex.mappingConeHomOfDegreewiseSplitIso_inv_f`, `Subgroup.transferTransversal_apply''`, `CochainComplex.HomComplex.Cochain.leftShiftAddEquiv_symm_apply`, `HomotopyCategory.Pretriangulated.rotate_distinguished_triangle`, `CochainComplex.HomComplex.Cochain.rightShift_neg`, `CochainComplex.mappingConeCompTriangle_mor₃_naturality_assoc`, `HomotopyCategory.quotient_obj_singleFunctors_obj`, `CochainComplex.mappingCone.triangleMapOfHomotopy_comm₃`, `CharacterModule.intSpanEquivQuotAddOrderOf_apply_self`, `DerivedCategory.instEssSurjCochainComplexIntQ`, `CochainComplex.HomComplex.Cochain.fromSingleMk_v_eq_zero`, `HomologicalComplex.dgoEquivHomologicalComplex_inverse`, `DerivedCategory.singleFunctorsPostcompQIso_hom_hom`, `CochainComplex.shiftShortComplexFunctor'_inv_app_τ₂`, `CochainComplex.HomComplex.Cocycle.equivHomShift_symm_precomp`, `AddSubgroup.relIndex_eq_natAbs_det`, `CategoryTheory.Functor.mapCochainComplexShiftIso_hom_app_f`, `jacobiSym.list_prod_right`, `CochainComplex.shiftEval_inv_app`, `ZNum.dvd_to_int`, `CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁`, `ZSpan.vadd_mem_fundamentalDomain`, `PosNum.to_nat_to_int`, `Subgroup.quotientEquivSigmaZMod_symm_apply`, `HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_acyclic`, `CategoryTheory.DifferentialObject.objEqToHom_d_assoc`, `CochainComplex.HomComplex.Cocycle.rightShiftAddEquiv_apply`, `CategoryTheory.DifferentialObject.d_squared_apply_assoc`, `CochainComplex.ConnectData.homologyMap_map_of_eq_neg_succ`, `CochainComplex.HomComplex.Cochain.equivHomotopy_symm_apply_hom`, `ComplexShape.ε_up_ℤ`, `CochainComplex.HomComplex.Cocycle.equivHomShift_comp_shift`, `HomotopyCategory.homologyFunctor_shiftMap`, `CochainComplex.HomComplex.Cochain.rightShiftLinearEquiv_symm_apply`, `Ring.descPochhammer_succ_succ_smeval`, `CochainComplex.shiftShortComplexFunctor'_inv_app_τ₁`, `CochainComplex.mappingCone.lift_f_snd_v`, `CochainComplex.shiftShortComplexFunctorIso_zero_add_hom_app`, `CochainComplex.isKProjective_shift_iff`, `ComplexShape.embeddingDownIntUpInt_f`, `CochainComplex.instIsStrictlyLEObjIntSingleFunctor`, `ComplexShape.embeddingUpIntGE_f`, `CochainComplex.mappingCone.triangle_obj₂`, `ZMod.coe_intCast`, `CochainComplex.instIsStrictlyGEObjIntSingleFunctor`, `Profinite.NobelingProof.list_prod_apply`, `CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₃`, `padicValuation_le_one`, `CochainComplex.mappingConeCompTriangle_mor₂`, `DerivedCategory.instLinearHomotopyCategoryIntUpQh`, `exists_signed_sum`, `CochainComplex.cm5b.degreewiseEpiWithInjectiveKernel_p`, `CochainComplex.HomComplex.Cochain.rightShift_v`, `CochainComplex.HomComplex.Cochain.rightUnshift_zero`, `CochainComplex.mappingConeCompTriangleh_comm₁`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_extMk`, `ModN.instModuleFinite`, `CochainComplex.HomComplex.Cocycle.leftShift_coe`, `CochainComplex.HomComplex.Cochain.shift_v'`, `CochainComplex.cm5b.instInjectiveXIntMappingConeIdI`, `Polynomial.descPochhammer_smeval_eq_ascPochhammer`, `Mathlib.Meta.NormNum.isNat_intOfNat`, `IsPrimitiveRoot.minpoly_dvd_cyclotomic`, `Tactic.NormNum.isInt_ratNum`, `jacobiSym.list_prod_left`, `DerivedCategory.mem_distTriang_iff`, `ZLattice.sum_piFinset_Icc_rpow_le`, `CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_inv_assoc`, `CategoryTheory.Functor.instCommShiftCochainComplexIntMapMap₂CochainComplex`, `CochainComplex.isKInjective_iff_rightOrthogonal`, `CochainComplex.HomComplex.Cochain.rightShift_add`, `CochainComplex.ShiftSequence.shiftIso_inv_app`, `Polynomial.cyclotomic_eq_minpoly`, `CochainComplex.HomComplex.Cochain.diff_v`, `HomologicalComplex.dgoEquivHomologicalComplexUnitIso_inv_app_f`, `DerivedCategory.instIsLEObjCochainComplexIntQOfIsLE`, `CategoryTheory.Functor.instCommShiftCochainComplexIntMapFlipMap₂CochainComplex`, `CochainComplex.HomComplex.Cochain.toSingleEquiv_toSingleMk`, `CochainComplex.isGE_shift`, `CochainComplex.HomComplex.δ_neg_one_cochain`, `CochainComplex.HomComplex.Cochain.ofHoms_zero`, `DerivedCategory.Q_map_eq_of_homotopy`, `CategoryTheory.Functor.commShiftIso_map₂CochainComplex_hom_app`, `instModuleFree_of_discrete_submodule`, `instNormOneClass`, `ModularGroup.S_mul_S_eq`, `CochainComplex.mappingCone.triangleRotateShortComplex_f`, `ZMod.intCast_cast`, `HomotopyCategory.quotient_obj_mem_subcategoryAcyclic_iff_exactAt`, `CochainComplex.HomComplex.Cocycle.rightUnshift_coe`, `CochainComplex.mappingCone.rotateHomotopyEquiv_comm₃`, `ComplexShape.instIsRelIffIntEmbeddingUpIntDownInt`, `ZNum.to_int_inj`, `ModuleCat.forget₂AddCommGroupIsEquivalence`, `CochainComplex.mappingCone.lift_f`, `CochainComplex.HomComplex.Cochain.δ_leftShift`, `DerivedCategory.isIso_Q_map_iff_quasiIso`, `ZNum.mul_to_int`, `DerivedCategory.isIso_Qh_map_iff`, `CochainComplex.HomComplex.CohomologyClass.toHom_mk`, `Mathlib.Tactic.Ring.intCast_negOfNat_Int`, `CochainComplex.HomComplex.Cochain.add_v`, `CochainComplex.HomComplex.Cocycle.leftShiftAddEquiv_apply`, `CochainComplex.instIsMultiplicativeIntDegreewiseEpiWithInjectiveKernel`, `DerivedCategory.left_fac_of_isStrictlyGE`, `CochainComplex.mappingConeHomOfDegreewiseSplitIso_hom_f`, `CochainComplex.mappingCone.inl_v_fst_v_assoc`, `CategoryTheory.ProjectiveResolution.cochainComplex_d_assoc`, `HomotopyCategory.mappingConeCompTriangleh_distinguished`, `CochainComplex.HomComplex.Cochain.leftShift_neg`, `CategoryTheory.InjectiveResolution.extEquivCohomologyClass_symm_mk_hom`, `CategoryTheory.Functor.mapDerivedCategoryFactorsh_hom_app`, `CochainComplex.HomComplex.Cochain.toSingleMk_sub`, `Module.Basis.addSubgroupOfClosure_apply`, `CochainComplex.HomComplex.Cocycle.equivHomShift_apply`, `CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₁`, `CochainComplex.HomComplex.Cochain.leftUnshift_neg`, `CochainComplex.isLE_shift`, `CochainComplex.mappingCone.triangle_obj₁`, `HomologicalComplex.dgoEquivHomologicalComplexCounitIso_inv_app_f`, `Rat.isInt_intFloor_ofIsRat_neg`, `HomotopyCategory.instIsClosedUnderIsomorphismsIntUpSubcategoryAcyclic`, `Polynomial.neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq`, `CochainComplex.mappingCone.lift_f_snd_v_assoc`, `Profinite.NobelingProof.factors_prod_eq_basis`, `castAddHom_int`, `CochainComplex.mappingCone.mapHomologicalComplexXIso'_inv`, `ComplexShape.boundaryLE_embeddingUpIntLE_iff`, `ZLattice.covolume_div_covolume_eq_relIndex'`, `CochainComplex.cm5b`, `divisorsAntidiag_neg_natCast`, `CategoryTheory.InjectiveResolution.Hom.ι'_comp_hom'`, `Profinite.NobelingProof.factors_prod_eq_basis_of_eq`, `ZNum.of_to_int'`, `CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_symm_apply`, `padicValuation_eq_zero_iff`, `CategoryTheory.InjectiveResolution.instInjectiveXIntCochainComplex`, `CochainComplex.shiftFunctor_obj_d`, `CochainComplex.HomComplex.Cochain.toSingleMk_precomp`, `PeriodPair.finrank_lattice`, `CochainComplex.HomComplex.Cocycle.rightShift_coe`, `CochainComplex.mappingCone.d_fst_v`, `CochainComplex.mappingConeCompHomotopyEquiv_hom_inv_id_assoc`, `CochainComplex.HomComplex.Cochain.leftUnshift_zero`, `submodule_toAddSubgroup_index_ne_zero_iff`, `DerivedCategory.left_fac`, `Polynomial.int_cyclotomic_unique`, `CochainComplex.mappingCone.triangle_obj₃`, `CochainComplex.HomComplex.Cochain.map_neg`, `CochainComplex.isZero_of_isLE`, `CochainComplex.HomComplex_d_hom_apply`, `CochainComplex.instFaithfulIntSingleFunctor`, `ZLattice.exists_finsetSum_norm_rpow_le_tsum`, `CochainComplex.HomComplex.CohomologyClass.homAddEquiv_apply`, `CochainComplex.mappingConeCompTriangle_obj₁`, `CochainComplex.cm5b.I_X`, `ZLattice.abs_repr_le`, `Rat.isInt_intCeil_ofIsRat_neg`, `CategoryTheory.InjectiveResolution.extAddEquivCohomologyClass_apply`, `ZLattice.covolume_eq_det`, `CochainComplex.instAdditiveHomologicalComplexIntUpShiftFunctor`, `ComplexShape.instIsTruncGENatIntEmbeddingUpNat`, `instEnoughInjectivesModuleCatInt`, `IsPrimitiveRoot.minpoly_dvd_x_pow_sub_one`, `Submodule.natAbs_det_basis_change`, `CochainComplex.ι_mapBifunctorShift₁Iso_hom_f`, `Profinite.NobelingProof.succ_mono`, `CochainComplex.ShiftSequence.shiftIso_hom_app`, `CategoryTheory.ProjectiveResolution.extEquivCohomologyClass_symm_neg`, `CochainComplex.HomComplex.Cochain.single_v_eq_zero`, `CategoryTheory.InjectiveResolution.cochainComplex_d`, `HomotopyCategory.instCommShiftHomologicalComplexIntUpHomFunctorMapHomotopyCategoryFactors`, `CochainComplex.mappingCone.map_δ`, `DerivedCategory.instIsLocalizationHomotopyCategoryIntUpQhTrWSubcategoryAcyclic`, `CochainComplex.HomComplex.Cochain.ofHom_comp`, `CochainComplex.HomComplex.Cochain.ofHomotopy_ofEq`, `CochainComplex.ConnectData.restrictionGEIso_hom_f`, `DerivedCategory.instHasRightCalculusOfFractionsHomotopyCategoryIntUpQuasiIso`, `Polynomial.int_cyclotomic_spec`
`instSemiring` 📖	CompOp	565 math math: `RatFunc.instFaithfulSMulPolynomialLaurentSeries`, `NumberField.Ideal.ramificationIdx_primesOverSpanEquivMonicFactorsMod_symm_apply'`, `NumberField.basisMatrix_eq_embeddingsMatrixReindex`, `NumberField.mixedEmbedding.fundamentalDomain_integerLattice`, `Module.isTorsionFree_int_iff_isAddTorsionFree`, `FreeAbelianGroup.instFiniteInt`, `Polynomial.natDegree_hermite`, `IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime`, `Polynomial.cardPowDegree_zero`, `odd_mul`, `tendsto_tsum_div_pow_atTop_integral`, `NumberField.canonicalEmbedding.mem_span_latticeBasis`, `quotientSpanEquivZMod_comp_Quotient_mk`, `NumberField.integralBasis_apply`, `PeriodPair.hasSumLocallyUniformly_weierstrassP`, `Polynomial.eval₂_intCastRingHom_X`, `NumberField.Units.logEmbedding_fundSystem`, `PeriodPair.coeff_weierstrassPExceptSeries`, `Profinite.NobelingProof.injective_πs'`, `Nat.ofDigits_zmodeq`, `AddEquiv.toIntLinearEquiv_toAddEquiv`, `NumberField.instFreeIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule`, `RootPairing.EmbeddedG2.mem_span_of_mem_allRoots`, `PeriodPair.derivWeierstrassPExcept_sub`, `NumberField.Units.fun_eq_repr`, `NumberField.canonicalEmbedding.latticeBasis_apply`, `addMonoidHomLequivInt_apply`, `NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_completeFamily_of_ne`, `Rat.padicValuation_cast`, `one_le_pow_mul_abs_eval_div`, `PeriodPair.ω₁_div_two_notMem_lattice`, `AddEquiv.toIntLinearEquiv_refl`, `instIsStrictOrderedRing`, `Polynomial.exists_partition_polynomial`, `IsPrimitiveRoot.minpoly_dvd_pow_mod`, `Profinite.NobelingProof.Products.span_nil_eq_top`, `LaurentSeries.LaurentSeriesRingEquiv_def`, `odd_sign_iff`, `Profinite.NobelingProof.GoodProducts.linearIndependent_iff_union_smaller`, `Profinite.NobelingProof.coe_πs`, `RootPairing.Base.root_mem_span_int`, `Padic.instCompatibleWithZeroMultiplicativeIntMulValuation`, `NumberField.FinitePlace.norm_def'`, `Module.Basis.ofZLatticeBasis_apply`, `quotientSpanNatEquivZMod_comp_Quotient_mk`, `NumberField.mixedEmbedding.mem_idealLattice`, `BoxIntegral.unitPartition.mem_smul_span_iff`, `FunctionField.inftyValuation.X_inv`, `padicValuation_lt_one_iff`, `Polynomial.coeff_shiftedLegendre`, `IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg`, `IsDedekindDomain.HeightOneSpectrum.valuation_of_algebraMap`, `odd_pow'`, `LaurentSeries.valuation_le_iff_coeff_lt_eq_zero`, `LaurentSeries.valuation_single_zpow`, `IsDedekindDomain.HeightOneSpectrum.intValuation_le_one`, `IsCyclotomicExtension.Rat.ramificationIdxIn_eq`, `WeierstrassCurve.valuation_Δ_aux_eq_of_isIntegral`, `PeriodPair.eqOn_deriv_weierstrassPExcept_derivWeierstrassPExcept`, `PeriodPair.weierstrassP_coe`, `ZSpan.smul`, `Module.Basis.ofZLatticeComap_apply`, `even_xor'_odd`, `Polynomial.exists_partition_polynomial_aux`, `Algebra.discr_eq_discr`, `Nat.ceil_int`, `Profinite.NobelingProof.Products.max_eq_eval`, `IsDedekindDomain.HeightOneSpectrum.instIsNontrivialWithZeroMultiplicativeIntValuation`, `Polynomial.coeff_hermite_succ_zero`, `Polynomial.coeff_hermite_succ_succ`, `Profinite.NobelingProof.Products.eval_πs`, `PeriodPair.hasSum_derivWeierstrassPExcept`, `padicValuation_eq_one_iff`, `CategoryTheory.Functor.intLinear`, `negOnePow_eq_neg_one_iff`, `PowerSeries.coe_add`, `LocallyConstant.freeOfProfinite`, `ZLattice.comap_discreteTopology`, `Ideal.absNorm_eq_pow_inertiaDeg'`, `IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_mem`, `Polynomial.leadingCoeff_hermite`, `IsPrimitiveRoot.is_roots_of_minpoly`, `CharacterModule.instLinearMapClassIntAddCircleRatOfNat`, `LaurentSeries.ofPowerSeries_powerSeriesPart`, `IsDedekindDomain.HeightOneSpectrum.intValuation_singleton`, `LaurentSeries.single_order_mul_powerSeriesPart`, `FunctionField.instIsNontrivialRatFuncWithZeroMultiplicativeIntInftyValuation`, `AddEquiv.toIntLinearEquiv_trans`, `Rat.padicValuation_self`, `ModN.basis_apply_eq_mkQ`, `RatFunc.coe_X`, `PowerSeries.coeff_coe`, `Profinite.NobelingProof.Products.eval_πs'`, `BoxIntegral.unitPartition.integralSum_eq_tsum_div`, `ZLattice.module_finite`, `zpow_eq_neg_zpow_iff₀`, `LaurentSeries.coe_algebraMap`, `PeriodPair.latticeBasis_zero`, `Polynomial.int_coeff_of_cyclotomic'`, `RatFunc.coe_coe`, `LindemannWeierstrass.exp_polynomial_approx`, `tendsto_card_div_pow_atTop_volume`, `coe_castRingHom`, `Polynomial.valuation_of_mk`, `RootPairing.finrank_corootSpanIn_int`, `Polynomial.unique_int_coeff_of_cycl`, `Ideal.isPrime_int_iff`, `ArithmeticFunction.moebius_mul_coe_zeta`, `odd_add`, `ZLattice.rank`, `ZSpan.quotientEquiv_apply_mk`, `Polynomial.cardPowDegree_isEuclidean`, `PeriodPair.ω₂_div_two_notMem_lattice`, `LaurentSeries.inducing_coe`, `PowerSeries.coe_smul`, `PeriodPair.hasSum_derivWeierstrassP`, `PeriodPair.compl_lattice_diff_singleton_mem_nhds`, `LaurentSeries.continuous_coe`, `LaurentSeries.algebraMap_C_mem_adicCompletionIntegers`, `AddSubgroup.index_eq_natAbs_det`, `PeriodPair.hasSumLocallyUniformly_derivWeierstrassP`, `Zsqrtd.mker_norm_eq_unitary`, `Profinite.NobelingProof.GoodProducts.spanFin`, `RootPairing.Base.coroot_mem_span_int`, `CharP.ker_intAlgebraMap_eq_span`, `Padic.norm_eq_zpow_log_mulValuation`, `Module.Free.addMonoidHom`, `Profinite.NobelingProof.GoodProducts.smaller_factorization`, `PowerSeries.intValuation_eq_of_coe`, `ZLattice.covolume.tendsto_card_div_pow`, `PeriodPair.mem_lattice`, `instCountable_of_discrete_submodule`, `Polynomial.card_eq_of_natDegree_le_of_coeff_le`, `Polynomial.isUnitTrinomial_iff`, `PeriodPair.analyticOnNhd_derivWeierstrassPExcept`, `Profinite.NobelingProof.πs'_apply_apply`, `RootPairing.finrank_rootSpanIn_int`, `NumberField.Units.span_basisOfIsMaxRank`, `LaurentSeries.val_le_one_iff_eq_coe`, `NumberField.canonicalEmbedding.integralBasis_repr_apply`, `IsDedekindDomain.HeightOneSpectrum.valuation_exists_uniformizer`, `PowerSeries.coe_mul`, `Finsupp.toFreeAbelianGroup_comp_singleAddHom`, `NumberField.mixedEmbedding.fundamentalDomain_idealLattice`, `Submodule.span_int_eq`, `Module.End.intCast_def`, `IsCyclotomicExtension.Rat.inertiaDegIn_of_not_dvd`, `not_isField`, `PowerSeries.coe_sub`, `Polynomial.hermite_succ`, `ZSpan.repr_ceil_apply`, `NumberField.Units.instFiniteIntAdditiveUnitsRingOfIntegers`, `ZLattice.comap_equiv_apply`, `CommRingCat.coproductCocone_inl`, `Polynomial.hermite_eq_iterate`, `LaurentSeries.algebraMap_apply`, `ZLattice.FG`, `IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd`, `odd_coe_nat`, `Module.Basis.addSubgroupOfClosure_repr_apply`, `NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis`, `PeriodPair.isClosed_lattice`, `NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIdealLattice`, `IsDedekindDomain.HeightOneSpectrum.valuation_def`, `Real.finrank_eq_int_finrank_of_discrete`, `NumberField.det_basisOfFractionalIdeal_eq_absNorm`, `Polynomial.int_cyclotomic_rw`, `PeriodPair.periodic_derivWeierstrassP`, `NumberField.RingOfIntegers.instIsNoetherianInt`, `span_natAbs`, `Nat.floor_int`, `IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime_pow`, `Submodule.finiteQuotient_iff`, `LaurentSeries.exists_ratFunc_val_lt`, `NumberField.RingOfIntegers.instIsLocalizationAlgebraMapSubmonoidIntNonZeroDivisors`, `AddSubgroup.toIntSubmodule_symm`, `NumberField.mixedEmbedding.span_idealLatticeBasis`, `ideal_span_isMaximal_of_prime`, `Padic.mulValuation_toFun`, `IsDedekindDomain.HeightOneSpectrum.valuation_div_le_one_iff`, `NumberField.Units.fundSystem_mk`, `IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd`, `Padic.comap_mulValuation_eq_padicValuation`, `CharacterModule.intSpanEquivQuotAddOrderOf_symm_apply_coe`, `Polynomial.X_pow_sub_X_sub_one_irreducible`, `RootPairing.EmbeddedG2.allRoots_eq_map_allCoeffs`, `Rat.valuation_le_one_iff_den`, `PeriodPair.differentiableOn_derivWeierstrassP`, `PeriodPair.weierstrassPExcept_def`, `NumberField.Units.rank_modTorsion`, `Module.Basis.ofZLatticeBasis_span`, `CharacterModule.intSpanEquivQuotAddOrderOf_apply`, `NumberField.mixedEmbedding.mem_span_latticeBasis`, `WeierstrassCurve.isGoodReduction_iff`, `isCompl_even_odd`, `Polynomial.IsUnitTrinomial.card_support_eq_three`, `fwdDiff_aux.shiftₗ_pow_apply`, `odd_sub`, `LaurentSeries.exists_Polynomial_intValuation_lt`, `IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation'`, `ArithmeticFunction.intCoe_mul`, `NumberField.Units.dirichletUnitTheorem.unitLattice_span_eq_top`, `orderedSMul`, `NumberField.mixedEmbedding.covolume_idealLattice`, `Submodule.span_singleton_toAddSubgroup_eq_zmultiples`, `OreLocalization.zsmul_eq_zsmul`, `Submodule.toIntSubmodule_toAddSubgroup`, `Profinite.NobelingProof.Products.eval_πs_image'`, `Polynomial.one_le_mahlerMeasure_of_ne_zero`, `Polynomial.degree_hermite`, `PeriodPair.hasSumLocallyUniformly_weierstrassPExcept`, `NumberField.discr_eq_discr`, `legendreSym.hom_apply`, `NumberField.Units.regOfFamily_of_isMaxRank`, `IsDedekindDomain.HeightOneSpectrum.valuation_of_mk'`, `ModN.natCard_eq`, `Polynomial.IsPrimitive.Int.irreducible_iff_irreducible_map_cast`, `RootPairing.IsG2.span_eq_rootSpan_int`, `LaurentSeries.of_powerSeries_localization`, `IsPrimitiveRoot.minpoly_dvd_mod_p`, `Polynomial.coeff_hermite_explicit`, `ZSpan.coe_floor_self`, `RatFunc.valuation_eq_LaurentSeries_valuation`, `Polynomial.IsUnitTrinomial.leadingCoeff_isUnit`, `descPochhammer_eq_ascPochhammer`, `ZLattice.module_free`, `instIsZLatticeRealSpan`, `quotientSpanEquivZMod_comp_castRingHom`, `Ideal.relNorm_int`, `NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm`, `Polynomial.coeff_hermite_self`, `Polynomial.IsUnitTrinomial.not_isUnit`, `PeriodPair.derivWeierstrassP_sub_coe`, `Submodule.toAddSubgroup_toIntSubmodule`, `Profinite.NobelingProof.GoodProducts.span`, `Submodule.natAbs_det_equiv`, `even_or_odd`, `NumberField.RingOfIntegers.rank`, `addMonoidEndRingEquivInt_apply`, `Submodule.span_int_eq_addSubgroup_closure`, `IsPrimitiveRoot.separable_minpoly_mod`, `NumberField.integralBasis_repr_apply`, `ZSpan.isAddFundamentalDomain'`, `IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_mem`, `Profinite.NobelingProof.GoodProducts.linearIndependent_iff_smaller`, `Submodule.fg_iff_addSubgroup_fg`, `LaurentSeries.coe_X_compare`, `ZLattice.covolume.tendsto_card_le_div'`, `NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def`, `LaurentSeries.intValuation_le_iff_coeff_lt_eq_zero`, `IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_not_dvd`, `RatFunc.algebraMap_apply_div`, `Polynomial.coeff_hermite_of_even_add`, `PowerSeries.coe_zero`, `instModuleFinite_of_discrete_submodule`, `Module.Finite.addMonoidHom`, `Rat.HeightOneSpectrum.natGenerator_dvd_iff`, `padicValuation_self`, `PeriodPair.weierstrassP_add_coe`, `PeriodPair.instProperSpaceSubtypeComplexMemSubmoduleIntLattice`, `ZSpan.span_top`, `AddEquiv.toIntLinearEquiv_symm`, `RootPairing.Base.span_int_root_support`, `LaurentSeries.exists_powerSeries_of_memIntegers`, `NumberField.mixedEmbedding.span_latticeBasis`, `Polynomial.cardPowDegree_apply`, `fermatLastTheoremFor_iff_int`, `IsDedekindDomain.HeightOneSpectrum.adicValued_apply`, `NumberField.Units.dirichletUnitTheorem.unitLattice_inter_ball_finite`, `NumberField.FinitePlace.norm_def_int`, `Profinite.NobelingProof.GoodProducts.linearIndependent_iff_sum`, `ZSpan.map`, `PowerSeries.coe_C`, `ZSpan.exist_unique_vadd_mem_fundamentalDomain`, `odd_iff`, `PowerSeries.coe_neg`, `odd_sub'`, `Polynomial.exists_approx_polynomial`, `fwdDiff_aux.fwdDiffₗ_apply`, `Submodule.span_int_eq_addSubgroupClosure`, `fwdDiff_aux.shiftₗ_apply`, `PeriodPair.latticeBasis_one`, `AbsoluteValue.IsAdmissible.exists_approx`, `ZLattice.covolume_eq_det_mul_measureReal`, `not_even_iff_odd`, `fermatLastTheoremWith_nat_int_rat_tfae`, `IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd`, `PeriodPair.weierstrassP_sub_coe`, `ZSpan.instDiscreteTopologySubtypeMemSubmoduleIntSpanRangeCoeBasisRealOfFinite`, `NumberField.RingOfIntegers.instFreeInt`, `ZSpan.isAddFundamentalDomain`, `Ring.smeval_ascPochhammer_int_ofNat`, `Profinite.NobelingProof.πs_apply_apply`, `NumberField.Units.instDiscrete_unitLattice`, `TensorProduct.CompatibleSMul.int`, `NumberField.mixedEmbedding.euclidean.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice`, `Profinite.NobelingProof.GoodProducts.finsuppSum_mem_span_eval`, `cyclotomic_prime_pow_comp_X_add_one_isEisensteinAt`, `ZLattice.exists_forall_abs_repr_le_norm`, `IsDedekindDomain.HeightOneSpectrum.intValuation_zero_lt`, `LaurentSeries.LaurentSeriesRingEquiv_mem_valuationSubring`, `Profinite.NobelingProof.GoodProducts.linearIndependent`, `IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation`, `groupHomology.H1AddEquivOfIsTrivial_symm_apply`, `PeriodPair.hasSum_weierstrassP`, `PeriodPair.coeff_weierstrassPSeries`, `PeriodPair.isOpen_compl_lattice_diff`, `Ideal.span_singleton_toAddSubgroup_eq_zmultiples`, `NumberField.fractionalIdeal_rank`, `PeriodPair.derivWeierstrassP_coe`, `LaurentSeries.valuation_LaurentSeries_equal_extension`, `Polynomial.IsUnitTrinomial.irreducible_of_coprime'`, `Profinite.NobelingProof.Nobeling_aux`, `RatFunc.v_def`, `Rat.HeightOneSpectrum.span_natGenerator`, `groupHomology.H1ToTensorOfIsTrivial_H1π_single`, `Rat.padicValuation_eq_zero_iff`, `NumberField.mixedEmbedding.volume_fundamentalDomain_fractionalIdealLatticeBasis`, `LaurentSeries.LaurentSeries_coe`, `IsDedekindDomain.HeightOneSpectrum.intValuation_eq_one_iff`, `Profinite.NobelingProof.spanFinBasis.span`, `Polynomial.IsPrimitive.Int.dvd_iff_map_cast_dvd_map_cast`, `AbsoluteValue.IsAdmissible.exists_partition`, `LaurentSeries.powerSeries_ext_subring`, `Set.unit_valuation_eq_one`, `Liouville.exists_pos_real_of_irrational_root`, `AddMonoidHom.coe_toIntLinearMap_ker`, `ZLattice.covolume.tendsto_card_div_pow'`, `Polynomial.factorial_mul_shiftedLegendre_eq`, `not_odd_zero`, `ZMod.intCast_eq_one_iff_odd`, `NumberField.inverse_basisMatrix_mulVec_eq_repr`, `RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply`, `FunctionField.inftyValuation.X_zpow`, `AddSubgroup.coe_toIntSubmodule`, `LaurentSeries.powerSeriesRingEquiv_coe_apply`, `AbsoluteValue.IsAdmissible.exists_partition'`, `even_add'`, `PeriodPair.latticeEquiv_symm_apply`, `NumberField.canonicalEmbedding.mem_rat_span_latticeBasis`, `PeriodPair.hasSumLocallyUniformly_derivWeierstrassPExcept`, `LaurentSeries.powerSeriesEquivSubring_apply`, `Nat.ofDigits_zmodeq'`, `IsDedekindDomain.HeightOneSpectrum.intValuation_def`, `ContinuousMultilinearMap.alternatization_apply_toContinuousMultilinearMap`, `IsPrimitiveRoot.squarefree_minpoly_mod`, `natAbsHom_apply`, `FunctionField.inftyValuation.X`, `ZLattice.covolume.tendsto_card_le_div`, `IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_not_dvd`, `odd_add'`, `IsZLattice.span_top`, `IsCyclotomicExtension.Rat.ramificationIdxIn_eq_of_prime_pow`, `ZMod.ker_intCastRingHom`, `Polynomial.map_cyclotomic_int`, `IsCyclotomicExtension.Rat.inertiaDegIn_eq`, `NumberField.mixedEmbedding.instDiscreteTopologySubtypeMixedSpaceMemSubmoduleIntIntegerLattice`, `PeriodPair.analyticOnNhd_derivWeierstrassP`, `AddMonoidHom.coe_toIntLinearMap_map`, `AddMonoid.isTorsion_iff_isTorsion_int`, `Ideal.natAbs_det_equiv`, `ZSpan.quotientEquiv.symm_apply`, `NumberField.mem_span_integralBasis`, `groupHomology.H1AddEquivOfIsTrivial_apply`, `natAbs_odd`, `LaurentSeries.powerSeriesEquivSubring_coe_apply`, `IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero_eq`, `odd_pow`, `NumberField.mem_span_basisOfFractionalIdeal`, `RingHom.Int.subsingleton_ringHom`, `AddMonoidHom.coe_toIntLinearMap_range`, `PowerSeries.coe_X`, `LaurentSeries.instLaurentSeriesComplete`, `PeriodPair.instDiscreteTopologySubtypeComplexMemSubmoduleIntLattice`, `AbsoluteValue.map_units_int`, `Profinite.NobelingProof.GoodProducts.linearIndependentEmpty`, `IsDedekindDomain.HeightOneSpectrum.valuation_surjective`, `ZSpan.instDiscreteTopologySubtypeMemAddSubgroupToAddSubgroupIntSpanRangeCoeBasisRealOfFinite`, `NumberField.mixedEmbedding.latticeBasis_apply`, `LaurentSeries.valuation_coe_ratFunc`, `DistribSMul.toAddMonoidHom_eq_zsmulAddGroupHom`, `Padic.comap_mulValuation_eq_int_padicValuation`, `Surreal.dyadicMap_apply`, `Polynomial.coeff_hermite_of_odd_add`, `LaurentSeries.valuation_compare`, `Nat.span_singleton_setGcd`, `Submodule.AddMonoidHom.coe_toIntLinearMap_comap`, `ZLattice.isAddFundamentalDomain`, `addMonoidHomLequivInt_symm_apply`, `ArithmeticFunction.isMultiplicative_moebius`, `AbsoluteValue.IsAdmissible.toIsEuclidean`, `RatFunc.single_one_eq_pow`, `instDiscreteTopologySubtypeMemSubmoduleIntComap`, `NumberField.mixedEmbedding.latticeBasis_repr_apply`, `AddMonoid.End.intCast_def`, `AddEquiv.coe_toIntLinearEquiv`, `Profinite.NobelingProof.GoodProducts.span_iff_products`, `LaurentSeries.coe_range_dense`, `PowerSeries.intValuation_X`, `IsCyclotomicExtension.Rat.map_eq_span_zeta_sub_one_pow`, `IsDedekindDomain.HeightOneSpectrum.adicValued_apply'`, `Polynomial.cardPowDegree_nonzero`, `PeriodPair.hasSum_weierstrassPExcept`, `NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply`, `AbsoluteValue.IsAdmissible.exists_approx_aux`, `Submodule.fg_iff_add_subgroup_fg`, `not_odd_iff`, `FractionalIdeal.abs_det_basis_change`, `not_odd_iff_even`, `Ideal.span_singleton_absNorm`, `Ideal.map_comap_natCastRingHom_int`, `Nat.dvd_iff_dvd_ofDigits`, `AddSubgroup.toIntSubmodule_toAddSubgroup`, `LaurentSeries.comparePkg_eq_extension`, `Polynomial.coeff_hermite`, `PeriodPair.differentiableOn_weierstrassPExcept`, `PeriodPair.derivWeierstrassPExcept_add_coe`, `LaurentSeries.valuation_def`, `NumberField.Units.unitLattice_rank`, `Profinite.NobelingProof.CC_comp_zero`, `PeriodPair.differentiableOn_weierstrassP`, `Ideal.absNorm_eq_pow_inertiaDeg`, `FunctionField.inftyValuation.C`, `ZLattice.normBound_spec`, `Profinite.NobelingProof.eval_eq_πJ`, `Polynomial.degree_shiftedLegendre`, `Polynomial.hermite_zero`, `Polynomial.natDegree_shiftedLegendre`, `ZSpan.discreteTopology_pi_basisFun`, `NumberField.mixedEmbedding.volume_fundamentalDomain_latticeBasis`, `NumberField.Units.logEmbeddingEquiv_apply`, `ZLattice.covolume.tendsto_card_le_div''`, `Rat.HeightOneSpectrum.valuation_equiv_padicValuation`, `LaurentSeries.valuation_le_iff_coeff_lt_log_eq_zero`, `Polynomial.coeff_hermite_of_lt`, `NumberField.basisOfFractionalIdeal_apply`, `PeriodPair.hasSum_sumInvPow`, `FreeAbelianGroup.instFreeInt`, `Module.Basis.ofZLatticeComap_repr_apply`, `IsPrimitiveRoot.pow_isRoot_minpoly`, `LaurentSeries.uniformContinuous_coeff`, `PowerSeries.coe_one`, `Matrix.SpecialLinearGroup.coe_matrix_coe`, `ArithmeticFunction.coe_zeta_mul_moebius`, `Padic.norm_rat_le_one_iff_padicValuation_le_one`, `PeriodPair.periodic_weierstrassP`, `cyclotomic_comp_X_add_one_isEisensteinAt`, `Set.integer_valuation_le_one`, `Rat.surjective_padicValuation`, `Module.Basis.ofZLatticeBasis_repr_apply`, `groupHomology.mkH1OfIsTrivial_apply`, `tendsto_card_div_pow_atTop_volume'`, `QuadraticMap.separatingLeft_of_anisotropic`, `Nat.ofDigits_neg_one`, `AddMonoidHom.coe_toIntLinearMap`, `NumberField.instFiniteIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmodule`, `CharacterModule.intSpanEquivQuotAddOrderOf_apply_self`, `LaurentSeries.ratfuncAdicComplRingEquiv_apply`, `instIsLocalizationIntPosRat`, `Profinite.NobelingProof.injective_πs`, `Nat.zmodeq_ofDigits_digits`, `Polynomial.isUnitTrinomial_iff'`, `AddSubgroup.relIndex_eq_natAbs_det`, `IsDedekindDomain.HeightOneSpectrum.intValuation_exists_uniformizer`, `NumberField.exists_ne_zero_mem_ideal_of_norm_le_mul_sqrt_discr`, `PeriodPair.mul_ω₁_add_mul_ω₂_mem_lattice`, `ZSpan.vadd_mem_fundamentalDomain`, `Polynomial.ringHom_eval₂_intCastRingHom`, `ZSpan.fract_apply`, `Profinite.NobelingProof.coe_πs'`, `NumberField.Units.instFiniteIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion`, `one_lt_natDegree_of_irrational_root`, `addMonoidEndRingEquivInt_symm_apply`, `ideal_span_absNorm_eq_self`, `AddSubgroup.toIntSubmodule_closure`, `MonoidWithZeroHomClass.ext_rat_iff`, `fwdDiff_aux.coe_fwdDiffₗ_pow`, `PeriodPair.analyticOnNhd_weierstrassPExcept`, `NumberField.canonicalEmbedding_eq_basisMatrix_mulVec`, `IsCyclotomicExtension.Rat.ramificationIdxIn_of_not_dvd`, `AddCommMonoid.subsingletonIntModule`, `NumberField.coe_discr`, `Profinite.NobelingProof.list_prod_apply`, `ZSpan.repr_floor_apply`, `Module.Finite.iff_addGroup_fg`, `padicValuation_le_one`, `NumberField.instIsLocalizedModuleIntSubtypeMemSubmoduleRingOfIntegersCoeToSubmoduleValFractionalIdealNonZeroDivisorsRestrictScalarsSubtype`, `NumberField.mixedEmbedding.disjoint_span_commMap_ker`, `AddCommGroup.smul_top_eq_top_of_divisibleBy_int`, `AddMonoidHom.toIntLinearMap_injective`, `PowerSeries.coe_pow`, `Polynomial.IsUnitTrinomial.trailingCoeff_isUnit`, `LaurentSeries.mem_integers_of_powerSeries`, `AddMonoid.FG.to_moduleFinite_int`, `WeierstrassCurve.IsGoodReduction.goodReduction`, `LaurentSeries.instIsFractionRingPowerSeries`, `ZSpan.fract_eq_fract`, `Polynomial.finite_mahlerMeasure_le`, `IsCyclotomicExtension.Rat.ramificationIdxIn_of_prime`, `ZLattice.sum_piFinset_Icc_rpow_le`, `RootPairing.Base.span_int_coroot_support`, `Profinite.NobelingProof.GoodProducts.linearIndependent_iff_range`, `instIsTorsionFreeIntOfIsAddTorsionFree`, `ZLattice.covolume.tendsto_card_div_pow''`, `Profinite.NobelingProof.GoodProducts.max_eq_eval`, `PeriodPair.lattice_eq_span_range_basis`, `IsDedekindDomain.HeightOneSpectrum.valuation_le_one`, `instModuleFree_of_discrete_submodule`, `PeriodPair.ω₁_mem_lattice`, `LaurentSeries.X_order_mul_powerSeriesPart`, `Ideal.natAbs_det_basis_change`, `PeriodPair.analyticOnNhd_weierstrassP`, `IsDedekindDomain.HeightOneSpectrum.valuationOfNeZeroToFun_eq`, `fwdDiff_aux.coe_fwdDiffₗ`, `LaurentSeries.coeff_coe_powerSeries`, `Profinite.NobelingProof.GoodProducts.linearIndependentSingleton`, `IsCyclotomicExtension.Rat.inertiaDegIn_eq_of_prime`, `FunctionField.inftyValuation_apply`, `Surreal.dyadicMap_apply_pow`, `PeriodPair.ω₂_mem_lattice`, `MonoidWithZeroHom.ext_int_iff`, `Profinite.NobelingProof.Products.eval_πs_image`, `LaurentSeries.exists_ratFunc_eq_v`, `Module.Basis.addSubgroupOfClosure_apply`, `ZSpan.setFinite_inter`, `PeriodPair.derivWeierstrassPExcept_def`, `ZLattice.coe_comap`, `NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply`, `NumberField.house.basis_repr_norm_le_const_mul_house`, `Polynomial.neg_one_pow_mul_shiftedLegendre_comp_one_sub_X_eq`, `quotientSpanNatEquivZMod_comp_castRingHom`, `IsDedekindDomain.HeightOneSpectrum.intValuation_apply`, `even_sub'`, `LaurentSeries.valuation_X_pow`, `Polynomial.card_mahlerMeasure_le_prod`, `IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_mem`, `padicValuation_eq_zero_iff`, `RingHom.injective_int`, `LinearEquiv.toAddEquiv_toIntLinearEquiv`, `PeriodPair.finrank_lattice`, `PeriodPair.derivWeierstrassP_add_coe`, `MonoidHom.ext_int_iff`, `NumberField.Units.instFreeIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion`, `castRingHom_int`, `zpow_eq_neg_one_iff₀`, `ClassGroup.exists_mem_finset_approx'`, `NumberField.mixedEmbedding.mem_rat_span_latticeBasis`, `submodule_toAddSubgroup_index_ne_zero_iff`, `int_smul_eq_zsmul`, `BoxIntegral.unitPartition.tag_mem_smul_span`, `ClassGroup.exists_mem_finsetApprox`, `Rat.padicValuation_le_one_iff`, `PeriodPair.weierstrassPExcept_add`, `ZLattice.exists_finsetSum_norm_rpow_le_tsum`, `ZLattice.abs_repr_le`, `ZLattice.covolume_eq_det`, `Profinite.NobelingProof.GoodProducts.max_eq_eval_unapply`, `Nat.ofDigits_zmod`, `Submodule.natAbs_det_basis_change`, `Polynomial.hermite_monic`, `Polynomial.valuation_X_eq_neg_one`, `Polynomial.hermite_one`, `AddEquiv.coe_symm_toIntLinearEquiv`, `PeriodPair.differentiableOn_derivWeierstrassPExcept`, `Polynomial.int_cyclotomic_spec`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`cast_mul` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `AddCommGroupWithOne.toAddGroupWithOne` `NonAssocRing.toAddCommGroupWithOne` `Distrib.toMul` `NonUnitalNonAssocSemiring.toDistrib` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonAssocRing.toNonUnitalNonAssocRing`	—	`Nat.cast_zero` `MulZeroClass.zero_mul` `cast_zero` `Nat.cast_add` `Nat.cast_one` `add_mul` `Distrib.rightDistribClass` `one_mul` `cast_add` `cast_natCast` `cast_one` `neg_zero` `neg_add_rev` `neg_mul` `cast_neg`
`cast_mul_eq_zsmul_cast` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `SubNegMonoid.toZSMul` `AddGroup.toSubNegMonoid` `AddGroupWithOne.toAddGroup`	—	`induction_on` `MulZeroClass.zero_mul` `cast_zero` `zero_zsmul` `add_mul` `Distrib.rightDistribClass` `one_mul` `cast_add` `natCast_zsmul` `add_zsmul` `one_zsmul` `sub_mul` `cast_sub` `sub_zsmul`
`cast_pow` 📖	mathematical	—	`AddGroupWithOne.toIntCast` `Ring.toAddGroupWithOne` `Monoid.toNatPow` `instMonoid` `MonoidWithZero.toMonoid` `Semiring.toMonoidWithZero` `Ring.toSemiring`	—	`pow_zero` `cast_one` `pow_succ` `cast_mul`
`instCharZero` 📖	mathematical	—	`CharZero` `AddGroupWithOne.toAddMonoidWithOne` `Ring.toAddGroupWithOne` `CommRing.toRing` `instCommRing`	—	—
`instIsCancelMulZero` 📖	mathematical	—	`IsCancelMulZero` `MulZeroClass.toZero` `NonUnitalNonAssocSemiring.toMulZeroClass` `NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring` `NonUnitalNonAssocCommRing.toNonUnitalNonAssocRing` `NonUnitalCommRing.toNonUnitalNonAssocCommRing` `CommRing.toNonUnitalCommRing` `instCommRing`	—	—
`instIsDomain` 📖	mathematical	—	`IsDomain` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing`	—	`instIsCancelMulZero` `instNontrivial`
`instMulDivCancelClass` 📖	mathematical	—	`MulDivCancelClass` `Semiring.toMonoidWithZero` `CommSemiring.toSemiring` `CommRing.toCommSemiring` `instCommRing`	—	—

---

← Back to Index