instField 📖 | CompOp | 68 mathmath: exists_sq_eq_prime_iff_of_mod_four_eq_one, legendreSym.eq_neg_one_iff, pow_card_sub_one, IsPrimitiveRoot.minpoly_dvd_pow_mod, units_pow_card_sub_one_eq_one, charpoly_pow_card, exists_sq_eq_prime_iff_of_mod_four_eq_three, exists_sq_eq_neg_one_iff, wilsons_lemma, trace_pow_card, exists_sq_eq_two_iff, FiniteField.instIsScalarTowerZModExtension, GaloisField.finrank, card_units, pow_card, instIsDomain, FiniteField.pow_finrank_eq_natCard, WittVector.frobeniusPoly_zmod, FiniteField.finrank_zmod_extension, Subfield.bot_eq_of_zMod_algebra, pow_card_sub_one_eq_one, FiniteField.isSplittingField_of_nat_card_eq, legendreSym.eq_one_iff, IsPrimitiveRoot.minpoly_dvd_mod_p, instSubsingletonSubfieldZMod, sq_add_sq, euler_criterion_units, IsPrimitiveRoot.separable_minpoly_mod, FiniteField.splits_X_pow_nat_card_sub_X, PadicInt.toZMod_eq_residueField_comp_residue, gauss_lemma, MvPolynomial.frobenius_zmod, FiniteField.isSplittingField_of_card_eq, Polynomial.dickson_one_one_zmod_p, legendreSym.eq_zero_iff, RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply, IsPrimitiveRoot.squarefree_minpoly_mod, FiniteField.splits_X_pow_card_sub_X, Ico_map_valMinAbs_natAbs_eq_Ico_map_id, FiniteField.pow_finrank_eq_card, legendreSym.eq_one_iff', FiniteField.nonempty_algHom_extension, legendreSym.eq_pow, orderOf_dvd_card_sub_one, quadraticChar_odd_prime, frobenius_zmod, instSubsingletonSubfield, legendreSym.card_sqrts, gauss_lemma_aux, PadicInt.zmod_congr_of_sub_mem_max_ideal, nonsquare_iff_jacobiSym_eq_neg_one, expand_card, pow_card_pow, legendreSym.eq_neg_one_iff', isCyclic_units_two, isSquare_of_jacobiSym_eq_one, PadicInt.ker_toZMod, MvPolynomial.expand_zmod, prod_Ico_one_prime, fieldRange_castHom_eq_bot, euler_criterion, exists_sq_eq_neg_two_iff, orderOf_units_dvd_card_sub_one, eisenstein_lemma_aux, PadicInt.val_toZMod_eq_zmodRepr, PadicInt.toZMod_spec, pow_div_two_eq_neg_one_or_one, GaloisField.splits_zmod_X_pow_sub_X
|