| Metric | Count |
|---|
DefinitionsinstZModModule, instZModSMul, residueClassesEquiv, cast, castHom, chineseRemainder, finEquiv, instInv, inv, ringEquiv, ringEquivCongr, ringEquivOfPrime, unitOfCoprime, unitsEquivCoprime, val | 15 |
Theoremscoe_zmod_smul, intCast_zmod_two, natCast_zmod_two, range_mul_add, intCast_zmod_two, natCast_zmod_two, fst_zmod_cast, snd_zmod_cast, ext_zmod, addOrderOf_coe, addOrderOf_coe', addOrderOf_one, add_self_eq_zero_iff_eq_zero, castHom_apply, castHom_bijective, castHom_comp, castHom_injective, castHom_self, castHom_surjective, cast_add, cast_add', cast_add_eq_ite, cast_cast_zmod_of_le, cast_eq_val, cast_id, cast_id', cast_injective_of_le, cast_intCast, cast_intCast', cast_mul, cast_mul', cast_natCast, cast_natCast', cast_neg, cast_neg_one, cast_one, cast_one', cast_pow, cast_pow', cast_sub, cast_sub', cast_sub_one, cast_zero, cast_zmod_eq_zero_iff_of_le, charP, charZero, coe_intCast, coe_mul_inv_eq_one, coe_unitOfCoprime, coprime_mod_iff_coprime, eq_one_iff_odd, eq_one_of_isUnit_natCast, eq_zero_iff_even, exists, forall, instIsDomainOfNatNat, instSubsingletonModule, instSubsingletonUnits, intCast_abs_mod_two, intCast_cast, intCast_cast_add, intCast_cast_mul, intCast_cast_neg, intCast_cast_sub, intCast_comp_cast, intCast_eq_iff, intCast_eq_intCast_iff, intCast_eq_intCast_iff', intCast_eq_intCast_iff_dvd_sub, intCast_eq_one_iff_odd, intCast_eq_zero_iff_even, intCast_mod, intCast_rightInverse, intCast_surjective, intCast_zmod_cast, intCast_zmod_eq_zero_iff_dvd, inv_coe_unit, inv_eq_of_mul_eq_one, inv_mul_eq_one_of_isUnit, inv_mul_of_unit, inv_neg_one, inv_one, inv_zero, isUnit_iff_coprime, isUnit_prime_iff_not_dvd, isUnit_prime_of_not_dvd, ker_intCastAddHom, lift_castAddHom, lift_coe, lift_comp_castAddHom, lift_comp_coe, lift_injective, mul_inv_eq_gcd, mul_inv_of_unit, mul_val_inv, natAbs_min_of_le_div_two, natAbs_mod_two, natCast_comp_val, natCast_eq_iff, natCast_eq_natCast_iff, natCast_eq_natCast_iff', natCast_eq_one_iff_odd, natCast_eq_zero_iff, natCast_eq_zero_iff_even, natCast_mod, natCast_ne_zero_iff_odd, natCast_pow_eq_zero_of_le, natCast_rightInverse, natCast_self, natCast_self', natCast_toNat, natCast_val, natCast_zmod_surjective, natCast_zmod_val, ne_neg_self, ne_zero_iff_odd, neg_eq_self_iff, neg_eq_self_mod_two, neg_one_ne_one, neg_val, neg_val', nontrivial, nontrivial', nontrivial_iff, one_eq_zero_iff, ringChar_zmod_n, ringEquivCongr_intCast, ringEquivCongr_refl, ringEquivCongr_refl_apply, ringEquivCongr_ringEquivCongr_apply, ringEquivCongr_symm, ringEquivCongr_trans, ringEquivCongr_val, ringEquivOfPrime_eq_ringEquiv, ringHom_map_cast, ringHom_rightInverse, ringHom_surjective, subsingleton_iff, subsingleton_ringEquiv, subsingleton_ringHom, val_add, val_add_le, val_add_of_le, val_add_of_lt, val_add_val_of_le, val_cast_eq_val_of_lt, val_cast_of_lt, val_cast_zmod_lt, val_coe_unit_coprime, val_eq_one, val_eq_zero, val_injective, val_intCast, val_inv_mul, val_le, val_lt, val_mul, val_mul', val_mul_iff_lt, val_mul_le, val_mul_of_lt, val_natCast, val_natCast_of_lt, val_ne_zero, val_neg', val_neg_of_ne_zero, val_neg_one, val_ofNat, val_ofNat_of_lt, val_one, val_one', val_one'', val_one_eq_one_mod, val_pos, val_pow, val_pow_le, val_sub, val_two_eq_two_mod, val_unit', val_zero, add_add_add_cancel, add_self, char_ne_one, char_nsmul_eq_zero, neg_eq_self, periodicPts_add_left, sub_eq_add, two_le_char, nsmul_zmod_val_inv_nsmul, pow_pow_zmod_val_inv, pow_zmod_val_inv_pow, smulMemClass, zmod_smul_mem, zmod_val_inv_nsmul_nsmul | 194 |
| Total | 209 |
| Name | Category | Theorems |
|---|
cast 📖 | CompOp | 57 mathmath: intCast_cast_neg, cast_one, Prod.fst_zmod_cast, intCast_cast_mul, intCast_cast_add, cast_intCast', cast_add_eq_ite, cast_eq_val, AddAction.orbitZMultiplesEquiv_symm_apply, ringHom_rightInverse, cast_sub', cast_pow', cast_injective_of_le, AddAction.zmultiplesQuotientStabilizerEquiv_symm_apply, χ₈'_eq_χ₄_mul_χ₈, castHom_apply, cast_natCast', cast_one', cast_add', cast_zmod_eq_zero_iff_of_le, natCast_val, cast_mul', natCast_comp_val, intCast_comp_cast, cast_cast_zmod_of_le, intCast_cast_sub, ringHom_map_cast, cast_id', MulAction.orbitZPowersEquiv_symm_apply, cast_sub, cast_natCast, cast_neg_one, cast_zero, Subgroup.transferTransversal_apply', cast_intCast, Prod.snd_zmod_cast, intCast_rightInverse, unitsMap_val, MulAction.zpowersQuotientStabilizerEquiv_symm_apply, cast_id, Subgroup.transferFunction_apply, intCast_zmod_cast, isUnit_cast_of_dvd, cast_pow, cast_neg, Subgroup.transferTransversal_apply'', cast_sub_one, Subgroup.quotientEquivSigmaZMod_symm_apply, val_cast_eq_val_of_lt, coe_intCast, intCast_cast, val_cast_zmod_lt, PadicInt.cast_toZModPow, DirichletCharacter.changeLevel_eq_cast_of_dvd, PadicInt.toZMod_spec, cast_mul, cast_add
|
castHom 📖 | CompOp | 15 mathmath: WittVector.toZModPow_compat, castHom_apply, TruncatedWittVector.commutes_symm', castHom_self, PadicInt.zmod_cast_comp_toZModPow, castHom_comp, castHom_bijective, TruncatedWittVector.zmodEquivTrunc_apply, TruncatedWittVector.commutes, castHom_injective, TruncatedWittVector.commutes', fieldRange_castHom_eq_bot, castHom_surjective, TruncatedWittVector.commutes_symm, unitsMap_def
|
chineseRemainder 📖 | CompOp | — |
finEquiv 📖 | CompOp | — |
instInv 📖 | CompOp | 25 mathmath: ArithmeticFunction.vonMangoldt.residueClass_eq, inv_neg_one, ArithmeticFunction.vonMangoldt.residueClass_apply, zmod_val_inv_nsmul_nsmul, mul_inv_of_unit, inv_one, val_inv_mul, isUnit_inv, inv_coe_unit, DirichletCharacter.sum_char_inv_mul_char_eq, coe_int_inv_mul_eq_one, mul_val_inv, inv_mul_of_unit, pow_zmod_val_inv_pow, coe_int_mul_val_inv, inv_mul_eq_one_of_isUnit, inv_eq_of_mul_eq_one, ArithmeticFunction.vonMangoldt.LSeries_residueClass_eq, pow_pow_zmod_val_inv, mul_inv_eq_gcd, inv_zero, coe_mul_inv_eq_one, coe_int_mul_inv_eq_one, coe_int_val_inv_mul, nsmul_zmod_val_inv_nsmul
|
inv 📖 | CompOp | — |
ringEquiv 📖 | CompOp | 1 mathmath: ringEquivOfPrime_eq_ringEquiv
|
ringEquivCongr 📖 | CompOp | 7 mathmath: ringEquivCongr_trans, ringEquivCongr_refl_apply, ringEquivCongr_symm, ringEquivCongr_ringEquivCongr_apply, ringEquivCongr_refl, ringEquivCongr_val, ringEquivCongr_intCast
|
ringEquivOfPrime 📖 | CompOp | 1 mathmath: ringEquivOfPrime_eq_ringEquiv
|
unitOfCoprime 📖 | CompOp | 6 mathmath: Polynomial.natDegree_of_dvd_cyclotomic_of_irreducible, DihedralGroup.oddCommuteEquiv_symm_apply, Polynomial.natDegree_of_mem_normalizedFactors_cyclotomic, Polynomial.orderOf_root_cyclotomic_dvd, coe_unitOfCoprime, Polynomial.normalizedFactors_cyclotomic_card
|
unitsEquivCoprime 📖 | CompOp | — |
val 📖 | CompOp | 84 mathmath: PadicInt.lift_sub_val_mem_span, val_ofNat, DihedralGroup.orderOf_r, val_eq_one, Nat.sumByResidueClasses, natCast_natAbs_valMinAbs, val_unit', IsCyclic.unique_zpow_zmod, val_natCast_of_lt, IsAddCyclic.unique_zsmul_zmod, valMinAbs_def_pos, cast_eq_val, intCast_eq_iff, modularCyclotomicCharacter.spec, modularCyclotomicCharacter.toFun_spec', val_pow_le, val_injective, natCast_rightInverse, zmod_val_inv_nsmul_nsmul, val_one'', val_add, val_inv_mul, val_neg_of_ne_zero, val_mul, valMinAbs_nonneg_iff, val_cast_of_lt, modularCyclotomicCharacter.toFun_spec, val_one', neg_val, val_one_eq_one_mod, mul_val_inv, valMinAbs_natAbs_eq_min, natCast_eq_iff, QuaternionGroup.orderOf_a, natCast_val, valMinAbs_mul_two_eq_iff, natCast_comp_val, IsCyclotomicExtension.Rat.galEquivZMod_apply_of_pow_eq, val_zero, val_eq_ite_valMinAbs, val_neg_one, val_coe_unit_coprime, pow_zmod_val_inv_pow, AddChar.zmodChar_apply, val_neg', gauss_lemma, natCast_zmod_val, coe_int_mul_val_inv, neg_eq_self_iff, toAddCircle_apply, val_intCast, val_natCast, pow_pow_zmod_val_inv, val_ofNat_of_lt, mul_inv_eq_gcd, val_mul_le, gauss_lemma_aux, cyclotomicCharacter.spec, val_one, val_mul', rootsOfUnityCircleEquiv_comp_rootsOfUnityAddChar_val, val_two_eq_two_mod, IsPrimitiveRoot.autToPow_spec, modularCyclotomicCharacter'.spec', toCircle_apply, val_pos, val_mul_iff_lt, ringEquivCongr_val, val_eq_zero, neg_val', val_lt, val_cast_zmod_lt, eisenstein_lemma_aux, val_le, smul_units_def, coe_int_val_inv_mul, PadicInt.val_toZMod_eq_zmodRepr, toCircle_eq_circleExp, modularCyclotomicCharacter.toFun_spec'', IsCyclotomicExtension.autEquivPow_symm_apply, cyclotomicCharacter.toFun_spec, val_add_le, IsCyclotomicExtension.Rat.galEquivZMod_smul_of_pow_eq, nsmul_zmod_val_inv_nsmul
|