| Name | Category | Theorems |
|---|
aroots 📖 | CompOp | 45 mathmath: IntermediateField.AdjoinSimple.trace_gen_eq_sum_roots, mem_aroots', aroots_smul_nonzero, isConjRoot_iff_mem_minpoly_aroots, aroots_X_sub_C, aroots_quadratic_eq_pair_iff_of_ne_zero', aroots_X, nodup_aroots_iff_of_splits, aroots_C_mul, aroots_map, Splits.aeval_eq_prod_aroots, rootSet_def, trace_eq_sum_roots, aeval_eq_prod_aroots_sub_of_monic_of_splits, Algebra.IsAlgebraic.lift_cardinalMk_le_sigma_polynomial, IsAlgClosed.card_aroots_eq_natDegree, aroots_zero, Algebra.IsAlgebraic.cardinalMk_le_sigma_polynomial, IsAlgClosed.card_aroots_eq_natDegree_of_leadingCoeff_ne_zero, aroots_quadratic_eq_pair_iff_of_ne_zero, IntermediateField.algHomAdjoinIntegralEquiv_symm_apply_gen, ConjRootClass.nodup_aroots_minpoly, aroots_C_mul_X_pow, IntermediateField.AdjoinSimple.norm_gen_eq_prod_roots, Splits.aeval_eq_prod_aroots_of_monic, ConjRootClass.aroots_minpoly_eq_carrier_val, aeval_eq_prod_aroots_sub_of_splits, ConjRootClass.carrier_eq_mk_aroots_minpoly, PowerBasis.trace_gen_eq_sum_roots, aroots_monomial, aroots_X_pow, natSepDegree_eq_of_isAlgClosed, aroots_neg, mem_aroots, PowerBasis.liftEquiv'_apply_coe, IsAlgClosed.card_aroots_eq_natDegree_of_isUnit_leadingCoeff, Algebra.norm_eq_prod_roots, aroots_one, aroots_mul, PowerBasis.liftEquiv'_symm_apply_apply, Algebra.PowerBasis.norm_gen_eq_prod_roots, natSepDegree_eq_of_splits, aroots_def, aroots_C, aroots_pow
|
instMulActionElemRootSetOfSMulCommClass 📖 | CompOp | 5 mathmath: instSMulCommClassElemRootSet, instIsScalarTowerElemRootSet, rootSet.coe_smul, Splits.toPermHom_apply_eq_one_or_isSwap_of_ncard_le_of_mem_inertia, Splits.surjective_toPermHom_of_iSup_inertia_eq_top
|
nthRoots 📖 | CompOp | 16 mathmath: mem_rootsOfUnity_iff_mem_nthRoots, nthRoots_zero_right, nthRoots_two_one, card_nthRoots, card_nthRoots_subgroup_units, nthRoots_zero, IsPrimitiveRoot.nthRoots_one_nodup, nthRoots_two_eq_zero_iff, nthRootsFinset_def, rootsOfUnityEquivNthRoots_apply, IsPrimitiveRoot.card_nthRoots_one, mem_nthRoots, IsPrimitiveRoot.nthRoots_nodup, IsPrimitiveRoot.card_nthRoots, rootsOfUnityEquivNthRoots_symm_apply, IsPrimitiveRoot.nthRoots_eq
|
nthRootsFinset 📖 | CompOp | 12 mathmath: IsPrimitiveRoot.nthRoots_one_eq_biUnion_primitiveRoots, IsPrimitiveRoot.mem_nthRootsFinset, nthRootsFinset_toSet, X_pow_sub_one_eq_prod, one_mem_nthRootsFinset, IsPrimitiveRoot.card_nthRootsFinset, IsPrimitiveRoot.ntRootsFinset_pairwise_associated_sub_one_sub_of_prime, nthRootsFinset_def, nthRootsFinset_zero, IsPrimitiveRoot.pow_sub_pow_eq_prod_sub_mul, IsPrimitiveRoot.pow_add_pow_eq_prod_add_mul, mem_nthRootsFinset
|
rootSet 📖 | CompOp | 61 mathmath: Gal.galActionHom_restrict, rootSet_mapsTo, Gal.smul_def, card_rootSet_le_derivative, Gal.restrict_smul, Gal.galActionHom_injective, mem_rootSet_of_injective, ConjRootClass.rootSet_minpoly_eq_carrier, Gal.mapRoots_bijective, IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_root_cyclotomic, IsSplittingField.adjoin_rootSet, IsNormalClosure.adjoin_rootSet, instSMulCommClassElemRootSet, SplittingFieldAux.adjoin_rootSet, normalClosure_eq_iSup_adjoin', card_rootSet_eq_natDegree_iff_of_splits, adjoin_rootSet_eq_range, Splits.adjoin_rootSet_eq_range, isConjRoot_iff_mem_minpoly_rootSet, smul_mem_rootSet_iff, rootSet_zero, rootSet_C_mul_X_pow, rootSet_derivative_subset_convexHull_rootSet, IntermediateField.exists_finset_of_mem_supr'', rootSet_def, Splits.image_rootSet, IsSplittingField.adjoin_rootSet', Monic.mem_rootSet, image_rootSet, rootSet_finite, rootSet_maps_to', card_rootSet_eq_natDegree, rootSet_C, Gal.galAction_isPretransitive, IntermediateField.isSplittingField_iff, mem_rootSet', rootSet_one, instIsScalarTowerElemRootSet, normalClosure_eq_iSup_adjoin, Splits.image_rootSet_of_map_ne_zero, mem_rootSet, rootSet.coe_smul, ncard_rootSet_le, smul_mem_rootSet_iff_of_isUnit, mem_rootSet_of_ne, Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv, rootSet_monomial, rootSet_X_pow, rootSet_prod, Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly, Algebra.IsAlgebraic.range_eval_eq_rootSet_minpoly_of_splits, IsCyclotomicExtension.adjoin_roots_cyclotomic_eq_adjoin_nth_roots, IsSplittingField.adjoin_rootSet_eq_range, NumberField.Embeddings.range_eval_eq_rootSet_minpoly, preimage_eval_singleton, SplittingField.adjoin_rootSet, isSplittingField_iff_intermediateField, Algebra.IsAlgebraic.normalClosure_eq_iSup_adjoin_of_splits, Algebra.IsAlgebraic.normalClosure_le_iSup_adjoin, IntermediateField.adjoin_rootSet_isSplittingField, rootSet_neg
|
rootSetFintype 📖 | CompOp | 4 mathmath: card_rootSet_le_derivative, card_rootSet_eq_natDegree_iff_of_splits, card_rootSet_eq_natDegree, Gal.card_complex_roots_eq_card_real_add_card_not_gal_inv
|
roots 📖 | CompOp | 176 mathmath: rightInverse_ofMultiset_roots, IsAlgClosed.roots_eq_zero_iff_degree_nonpos, roots_normalize, roots_expand, roots_scaleRoots, mahlerMeasure_eq_leadingCoeff_mul_prod_roots, card_roots_le_map, mem_roots_sub_C', roots_monomial, card_roots_sub_C', Splits.nextCoeff_eq_neg_sum_roots_mul_leadingCoeff, one_le_prod_max_one_norm_roots, Splits.eval_derivative, irreducible_iff_roots_eq_zero_of_degree_le_three, roots_C_mul_X_pow, eq_prod_roots_of_splits, eq_prod_roots_of_monic_of_splits_id, Splits.roots_map_of_injective, map_sub_roots_sprod_eq_prod_map_eval, IsAlgClosed.card_roots_eq_natDegree, roots_C_mul, roots_eq_zero_iff_isRoot_eq_bot, roots_degree_eq_one, count_map_roots, IsPrimitiveRoot.is_roots_of_minpoly, roots_zero, natDegree_eq_card_roots', Splits.eval_derivative_eq_eval_mul_sum, card_roots_le_derivative, roots_eq_zero_of_irreducible_of_natDegree_ne_one, rootsExpandPowEquivRoots_apply, card_roots_map_le_degree, IsSepClosed.roots_eq_zero_iff, prod_roots_eq_coeff_zero_of_monic_of_splits, FiniteField.roots_X_pow_card_sub_X, Splits.degree_eq_card_roots, eval_derivative_of_splits, roots_X_pow_char_pow_sub_C_pow, Multiset.prod_X_sub_C_dvd_iff_le_roots, prod_multiset_root_eq_finset_root, IsAlgClosed.card_roots_map_eq_natDegree_of_isUnit_leadingCoeff, rootsExpandEquivRoots_apply, card_roots_toFinset_le_card_roots_derivative_diff_roots_succ, Splits.coeff_zero_eq_prod_roots_of_monic, prod_multiset_X_sub_C_dvd, coeff_zero_eq_leadingCoeff_mul_prod_roots_of_splits, resultant_eq_prod_eval, mem_roots_map_of_injective, roots_pow, cyclotomic.roots_to_finset_eq_primitiveRoots, roots_expand_map_frobenius, roots_expand_image_frobenius, roots_C_mul_X_sub_C_of_IsUnit, bUnion_roots_finite, roots_quadratic_eq_pair_iff_of_ne_zero, count_map_roots_of_injective, rootsExpandPowToRoots_apply, roots_C_mul_X_add_C, roots_cyclotomic_nodup, eval_derivative_eq_eval_mul_sum_of_splits, Splits.eq_prod_roots, spectralNorm.spectralNorm_pow_natDegree_eq_prod_roots, Splits.eval_derivative_div_eval_of_ne_zero, prod_max_one_norm_roots_le_mahlerMeasure_of_one_le_leadingCoeff, IsAlgClosed.card_roots_map_eq_natDegree_from_simpleRing, roots_X_sub_C, Matrix.det_eq_prod_roots_charpoly_of_splits, count_roots, map_roots_le, map_sub_sprod_roots_eq_prod_map_eval, Subfield.roots_X_pow_char_sub_X_bot, Splits.roots_map, roots_eq_of_degree_le_card_of_ne_zero, Matrix.trace_eq_sum_roots_charpoly, logMahlerMeasure_eq_log_leadingCoeff_add_sum_log_roots, eq_centerMass_of_eval_derivative_eq_zero, roots_expand_image_frobenius_subset, Splits.eval_eq_prod_roots_of_monic, Matrix.IsHermitian.roots_charpoly_eq_eigenvalues, roots_X, Splits.nextCoeff_eq_neg_sum_roots_of_monic, IsAlgClosed.roots_eq_zero_iff_natDegree_eq_zero, eq_prod_roots_of_splits_id, Matrix.IsHermitian.sort_roots_charpoly_eq_eigenvalues₀, eval_eq_prod_roots_sub_of_splits_id, splits_iff_card_roots, roots_X_pow_char_sub_C_pow, Matrix.trace_eq_sum_roots_charpoly_of_splits, roots_ofMultiset, roots_expand_pow_map_iterateFrobenius_le, roots_multiset_prod_X_sub_C, eval_derivative_div_eval_of_ne_zero_of_splits, map_roots_le_of_injective, Splits.eval_eq_prod_roots, card_roots_le_one_of_irreducible, Splits.dvd_iff_roots_le_roots, cyclotomic.roots_eq_primitiveRoots_val, card_roots', card_roots_X_pow_sub_C, filter_roots_map_range_eq_map_roots, mem_roots_sub_C, roots_smul_nonzero, roots_eq_of_degree_eq_card, mem_roots_iff_aeval_eq_zero, Splits.natDegree_eq_card_roots, card_roots_map_le_natDegree, eval_eq_prod_roots_sub_of_monic_of_splits_id, roots_expand_pow_map_iterateFrobenius, aeval_derivative_of_splits, sum_roots_eq_nextCoeff_of_monic_of_split, sum_derivRootWeight_pos, IsAlgClosed.card_roots_map_eq_natDegree_of_injective, nextCoeff_eq_neg_sum_roots_of_monic_of_splits, roots_prod, roots_mul, mem_roots, roots_list_prod, mem_roots', rootsExpandToRoots_apply, Splits.map_roots, Splits.eq_prod_roots_of_monic, resultant_eq_prod_roots_sub, roots.le_of_dvd, card_roots, degree_eq_card_roots, mem_roots_map, Chebyshev.roots_T_real, IsAlgClosed.card_roots_map_eq_natDegree_of_leadingCoeff_ne_zero, roots_one, Matrix.IsHermitian.roots_charpoly_eq_eigenvalues₀, roots_C_mul_X_sub_C, Splits.coeff_zero_eq_leadingCoeff_mul_prod_roots, roots_of_cyclotomic, roots_quadratic_eq_pair_iff_of_ne_zero', Matrix.det_eq_prod_roots_charpoly, roots_X_pow_char_sub_C, eval₂_derivative_of_splits, Associated.roots_eq, roots_expand_image_iterateFrobenius, roots_expand_pow_image_iterateFrobenius_subset, roots_neg, IsAlgClosed.roots_eq_zero_iff, card_roots_le_map_of_injective, coeff_eq_esymm_roots_of_splits, roots_eq_zero_iff_eq_zero_or_isRoot_eq_bot, nodup_roots_iff_of_splits, roots_expand_pow, exists_prod_multiset_X_sub_C_mul, Cubic.map_roots, roots_eq_of_degree_le_card, degree_eq_card_roots', roots_X_pow, roots_X_add_C, roots_multiset_prod, Splits.roots_map_of_ne_zero, natDegree_eq_card_roots, roots_countP_pos_le_signVariations, aroots_def, count_roots_le_one, roots_C_mul_X_add_C_of_IsUnit, roots_eq_of_natDegree_le_card_of_ne_zero, roots_C, card_roots_toFinset_le_derivative, IsAlgClosed.associated_iff_roots_eq_roots, nodup_roots, card_roots_sub_C, roots_map, roots_expand_map_frobenius_le, Chebyshev.roots_U_real, Monic.irreducible_iff_roots_eq_zero_of_degree_le_three, IsAlgClosed.dvd_iff_roots_le_roots, roots_X_pow_char_pow_sub_C, roots_def, coeff_zero_eq_prod_roots_of_monic_of_splits, roots_prod_X_sub_C, nextCoeff_eq_neg_sum_roots_mul_leadingCoeff_of_splits
|