# Generated by tools/translator: qualified upstream name -> MoonBit name.
ACCP_DOMAIN_ATOMIC accp_domain_atomic
ACCP_DOMAIN_IRREDUCIBLE_FACTOR_EXISTS accp_domain_irreducible_factor_exists
ACCP_RING_PROPER_DIVISOR_INDUCT accp_ring_proper_divisor_induct
BEZOUT_DOMAIN_IRREDUCIBLE_EQ_PRIME bezout_domain_irreducible_eq_prime
BEZOUT_INTEGER_RING bezout_integer_ring
BEZOUT_QUOTIENT_RING bezout_quotient_ring
BEZOUT_RING bezout_ring_v1
BEZOUT_RING_2 bezout_ring_2
BEZOUT_RING_COMAXIMAL_COPRIME bezout_ring_comaximal_coprime
BEZOUT_RING_COPRIME bezout_ring_coprime
BEZOUT_RING_COPRIME_COMAXIMAL bezout_ring_coprime_comaximal
BEZOUT_RING_EPIMORPHIC_IMAGE bezout_ring_epimorphic_image
BEZOUT_RING_FINITELY_GENERATED_EQ_PRINCIPAL_IDEAL bezout_ring_finitely_generated_eq_principal_ideal
BEZOUT_RING_IMP_BEZOUT bezout_ring_imp_bezout
BEZOUT_RING_IMP_GCD bezout_ring_imp_gcd
BEZOUT_RING_IRREDUCIBLE_IMP_PRIME bezout_ring_irreducible_imp_prime
BEZOUT_RING_LOCALIZATION bezout_ring_localization
BEZOUT_RING_SETADD bezout_ring_setadd
BOOLEAN_IMP_BEZOUT_RING boolean_imp_bezout_ring
BOOLEAN_IMP_VNREGULAR_RING boolean_imp_vnregular_ring
BOOLEAN_INTEGRAL_DOMAIN boolean_integral_domain
BOOLEAN_PRODUCT_RING boolean_product_ring
BOOLEAN_PROD_RING boolean_prod_ring
BOOLEAN_PROPER_IDEAL_COMPLEMENT boolean_proper_ideal_complement
BOOLEAN_QUOTIENT_RING boolean_quotient_ring
BOOLEAN_RING_10 boolean_ring_10
BOOLEAN_RING_2 boolean_ring_2
BOOLEAN_RING_BOOL_RING boolean_ring_bool_ring
BOOLEAN_RING_CHAR boolean_ring_char
BOOLEAN_RING_DIVIDES boolean_ring_divides
BOOLEAN_RING_DOUBLE boolean_ring_double
BOOLEAN_RING_EPIMORPHIC_IMAGE boolean_ring_epimorphic_image
BOOLEAN_RING_IRREDUCIBLE boolean_ring_irreducible
BOOLEAN_RING_MAXIMAL_EQ_PRIME_IDEAL boolean_ring_maximal_eq_prime_ideal
BOOLEAN_RING_MONOMORPHIC_PREIMAGE boolean_ring_monomorphic_preimage
BOOLEAN_RING_MULTSYS boolean_ring_multsys
BOOLEAN_RING_NEG boolean_ring_neg
BOOLEAN_RING_NILPOTENT boolean_ring_nilpotent
BOOLEAN_RING_OF_NUM boolean_ring_of_num
BOOLEAN_RING_POW boolean_ring_pow
BOOLEAN_RING_RADICAL boolean_ring_radical
BOOLEAN_RING_REGULAR boolean_ring_regular
BOOLEAN_RING_SQUARE boolean_ring_square
BOOLEAN_RING_SUBRING_GENERATED boolean_ring_subring_generated
BOOLEAN_RING_UNIT boolean_ring_unit
BOOLEAN_RING_ZERODIVISOR boolean_ring_zerodivisor
BOOL_RING bool_ring_v1
BOOL_RING_CARRIER_HAS_SIZE_2 bool_ring_carrier_has_size_2
CARD_DIVIDES_RING_EPIMORPHIC_IMAGE card_divides_ring_epimorphic_image
CARD_DIVIDES_RING_MONOMORPHIC_IMAGE card_divides_ring_monomorphic_image
CARD_EQ_MONOMIALS_COUNTABLE card_eq_monomials_countable
CARD_EQ_MONOMIALS_FINITE card_eq_monomials_finite
CARD_EQ_MONOMIALS_INFINITE card_eq_monomials_infinite
CARD_EQ_POLY_RING_COUNTABLE card_eq_poly_ring_countable
CARD_EQ_POLY_RING_FINITE card_eq_poly_ring_finite
CARD_EQ_POLY_RING_INFINITE card_eq_poly_ring_infinite
CARD_EQ_POWSER_RING_COUNTABLE card_eq_powser_ring_countable
CARD_EQ_POWSER_RING_FINITE card_eq_powser_ring_finite
CARD_EQ_POWSER_RING_INFINITE card_eq_powser_ring_infinite
CARD_EQ_RING_COSETS card_eq_ring_cosets
CARD_EQ_RING_COSET_IDEAL card_eq_ring_coset_ideal
CARD_EQ_RING_IMAGE_KERNEL card_eq_ring_image_kernel
CARD_EQ_RING_ISOMORPHIC_IMAGE card_eq_ring_isomorphic_image
CARD_EQ_RING_MONOMORPHIC_IMAGE card_eq_ring_monomorphic_image
CARD_INTEGER_MOD_RING card_integer_mod_ring
CARD_LE_QUOTIENT_RING card_le_quotient_ring
CARD_LE_RING_EPIMORPHIC_IMAGE card_le_ring_epimorphic_image
CARD_LE_RING_MONOMORPHIC_IMAGE card_le_ring_monomorphic_image
CARD_PRIME_SUBRING card_prime_subring
CARD_QUOTIENT_RING_DIVIDES card_quotient_ring_divides
CARD_RING_COSETS_DIVIDES card_ring_cosets_divides
CARRIER_SUBRING_GENERATED_SUBRING carrier_subring_generated_subring
CARRIER_SUBRING_OF carrier_subring_of
CARTESIAN_PRODUCT_SUBRING_OF_PRODUCT_RING cartesian_product_subring_of_product_ring
COEFF coeff_v1
COEFF_0 coeff_0
COEFF_0_POLY_RECIP_EQ_0 coeff_0_poly_recip_eq_0
COEFF_ABOVE_DEG coeff_above_deg
COEFF_COMPOSE coeff_compose
COEFF_IN_CARRIER coeff_in_carrier
COEFF_IN_CARRIER_ALT coeff_in_carrier_alt
COEFF_NONZERO_LE coeff_nonzero_le
COEFF_NONZERO_LE_DEG coeff_nonzero_le_deg
COEFF_POLY_0 coeff_poly_0
COEFF_POLY_1 coeff_poly_1
COEFF_POLY_ADD coeff_poly_add
COEFF_POLY_CONST coeff_poly_const
COEFF_POLY_DERIV coeff_poly_deriv
COEFF_POLY_LMUL coeff_poly_lmul
COEFF_POLY_MUL coeff_poly_mul
COEFF_POLY_MUL_ALT coeff_poly_mul_alt
COEFF_POLY_MUL_VAR coeff_poly_mul_var
COEFF_POLY_MUL_VARPOW coeff_poly_mul_varpow
COEFF_POLY_NEG coeff_poly_neg
COEFF_POLY_RECIP coeff_poly_recip
COEFF_POLY_RMUL coeff_poly_rmul
COEFF_POLY_SUB coeff_poly_sub
COEFF_POLY_SUM coeff_poly_sum
COEFF_POLY_VAR coeff_poly_var
COEFF_POLY_VARPOW coeff_poly_varpow
COEFF_POLY_VARPOW_MUL coeff_poly_varpow_mul
COEFF_POLY_VAR_MUL coeff_poly_var_mul
COEFF_POWSER_SUM coeff_powser_sum
COMAXIMAL_RADICALS comaximal_radicals
COMPATIBLE_MONOMIAL_ORDER compatible_monomial_order
CROSS_SUBRING_OF_PROD_RING cross_subring_of_prod_ring
DISJOINT_RING_COSETS disjoint_ring_cosets
EISENSTEIN_IRREDUCIBILITY eisenstein_irreducibility
EISENSTEIN_IRREDUCIBILITY_FRACTION_RING eisenstein_irreducibility_fraction_ring
EISENSTEIN_IRREDUCIBILITY_GEN eisenstein_irreducibility_gen
EUCLIDEAN_DOMAIN_IMP_PID euclidean_domain_imp_pid
EUCLIDEAN_IMP_PRINCIPAL_IDEAL_RING euclidean_imp_principal_ideal_ring
EUCLIDEAN_INTEGER_RING euclidean_integer_ring
EUCLIDEAN_POLY_RING euclidean_poly_ring
EUCLIDEAN_QUOTIENT_RING euclidean_quotient_ring
EUCLIDEAN_RING euclidean_ring_v1
EUCLIDEAN_RING_ALT euclidean_ring_alt
EUCLIDEAN_RING_EPIMORPHIC_IMAGE euclidean_ring_epimorphic_image
EUCLIDEAN_RING_UNIVERSAL_SIDE_DIVISOR euclidean_ring_universal_side_divisor
EXISTS_FUN_FROM_1 exists_fun_from_1
FIELD_10 field_10
FIELD_ASSOCIATES field_associates
FIELD_BOOL_RING field_bool_ring
FIELD_COPRIME field_coprime
FIELD_DIVIDES field_divides
FIELD_DIV_EQ_0 field_div_eq_0
FIELD_EPIMORPHIC_IMAGE field_epimorphic_image
FIELD_EPIMORPHISM_IMP_ISOMORPHISM field_epimorphism_imp_isomorphism
FIELD_EQ_ALL_DIVIDE_1 field_eq_all_divide_1
FIELD_EQ_ALL_UNITS field_eq_all_units
FIELD_EQ_NO_PROPER_IDEALS field_eq_no_proper_ideals
FIELD_EQ_NO_PROPER_IDEALS_EQ field_eq_no_proper_ideals_eq
FIELD_EQ_PROPER_IMP_MAXIMAL_IDEAL field_eq_proper_imp_maximal_ideal
FIELD_EQ_PROPER_IMP_PRIME_IDEAL field_eq_proper_imp_prime_ideal
FIELD_EQ_TRIVIAL_IDEALS field_eq_trivial_ideals
FIELD_EQ_TRIVIAL_IDEALS_EQ field_eq_trivial_ideals_eq
FIELD_GCD field_gcd
FIELD_HOMOMORPHISM_DIV field_homomorphism_div
FIELD_HOMOMORPHISM_IMP_MONOMORPHISM field_homomorphism_imp_monomorphism
FIELD_HOMOMORPHISM_INV field_homomorphism_inv
FIELD_IMP_BEZOUT_RING field_imp_bezout_ring
FIELD_IMP_INTEGRAL_DOMAIN field_imp_integral_domain
FIELD_IMP_LOCAL_RING field_imp_local_ring
FIELD_IMP_NOETHERIAN_RING field_imp_noetherian_ring
FIELD_IMP_NONTRIVIAL_RING field_imp_nontrivial_ring
FIELD_IMP_PID field_imp_pid
FIELD_IMP_UFD field_imp_ufd
FIELD_IMP_VNREGULAR_RING field_imp_vnregular_ring
FIELD_INTEGER_MOD_RING field_integer_mod_ring
FIELD_INV_EQ_0 field_inv_eq_0
FIELD_IRREDUCIBLE field_irreducible
FIELD_MONIC_ASSOCIATE field_monic_associate
FIELD_MONIC_IRREDUCIBLE_ASSOCIATE field_monic_irreducible_associate
FIELD_MUL_EQ_0 field_mul_eq_0
FIELD_MUL_LINV field_mul_linv
FIELD_MUL_RINV field_mul_rinv
FIELD_NILPOTENT field_nilpotent
FIELD_NILRADICAL field_nilradical
FIELD_NONTRIVIAL field_nontrivial
FIELD_POLY_RING field_poly_ring
FIELD_POW_EQ_0 field_pow_eq_0
FIELD_PRIME field_prime
FIELD_PRIME_SUBRING field_prime_subring
FIELD_PRODUCT_EQ_0 field_product_eq_0
FIELD_QUOTIENT_RING field_quotient_ring
FIELD_REAL_RING field_real_ring
FIELD_REGULAR field_regular
FIELD_RING_HOMOMORPHISM_MONOMORPHISM field_ring_homomorphism_monomorphism
FIELD_TAC field_tac
FIELD_UNIT field_unit
FIELD_ZERODIVISOR field_zerodivisor
FINITELY_GENERATED_IDEAL_0 finitely_generated_ideal_0
FINITELY_GENERATED_IDEAL_ALT finitely_generated_ideal_alt
FINITELY_GENERATED_IDEAL_CARRIER finitely_generated_ideal_carrier
FINITELY_GENERATED_IDEAL_EPIMORPHIC_IMAGE finitely_generated_ideal_epimorphic_image
FINITELY_GENERATED_IDEAL_GENERATED finitely_generated_ideal_generated
FINITELY_GENERATED_IDEAL_IMP_SUBSET finitely_generated_ideal_imp_subset
FINITELY_GENERATED_IDEAL_LOCALIZATION finitely_generated_ideal_localization
FINITELY_GENERATED_IDEAL_SETADD finitely_generated_ideal_setadd
FINITELY_GENERATED_IDEAL_SUBSET finitely_generated_ideal_subset
FINITELY_GENERATED_IMP_RING_IDEAL finitely_generated_imp_ring_ideal
FINITE_COEFF_SUPPORT finite_coeff_support
FINITE_FUN_FROM_1 finite_fun_from_1
FINITE_IDEAL_GENERATED finite_ideal_generated
FINITE_INTEGER_MOD_RING finite_integer_mod_ring
FINITE_INTEGRAL_DOMAIN_CHAR finite_integral_domain_char
FINITE_INTEGRAL_DOMAIN_EQ_FIELD finite_integral_domain_eq_field
FINITE_INTEGRAL_DOMAIN_IMP_FIELD finite_integral_domain_imp_field
FINITE_MONOMIAL_VARS finite_monomial_vars
FINITE_MONOMIAL_VARS_1 finite_monomial_vars_1
FINITE_POLYNOMIAL_VARS finite_polynomial_vars
FINITE_POLY_VARS finite_poly_vars
FINITE_PRIME_SUBRING finite_prime_subring
FINITE_PRODUCT_RING finite_product_ring
FINITE_PROD_RING finite_prod_ring
FINITE_RING_EPIMORPHIC_IMAGE finite_ring_epimorphic_image
FINITE_RING_MONOMORPHIC_PREIMAGE finite_ring_monomorphic_preimage
FINITE_SINGLETON_RING finite_singleton_ring
FINITE_SUBRING_GENERATED finite_subring_generated
FIRST_RING_EPIMORPHISM_THEOREM first_ring_epimorphism_theorem
FIRST_RING_ISOMORPHISM_THEOREM first_ring_isomorphism_theorem
FIRST_RING_ISOMORPHISM_THEOREM_GEN first_ring_isomorphism_theorem_gen
FIRST_RING_ISOMORPHISM_THEOREM_GEN_ALT first_ring_isomorphism_theorem_gen_alt
FLD_MONOMIAL_DIVIDES fld_monomial_divides
FLD_MONOMIAL_LE fld_monomial_le
FORALL_FUN_FROM_1 forall_fun_from_1
FRACTION_DOMAIN fraction_domain
FRACTION_FIELD fraction_field
FRACTION_RING_UNIT_EQ_REGULAR fraction_ring_unit_eq_regular
FRACTION_RING_UNIT_OR_ZERODIVISOR fraction_ring_unit_or_zerodivisor
FRACTION_RING_UNIVERSAL fraction_ring_universal
FROBENIUS_FIXED frobenius_fixed
FUN_EQ_COEFF fun_eq_coeff
FUN_ONE_EQ_ONE fun_one_eq_one
FUN_ONE_NUM_EQ fun_one_num_eq
HAS_SIZE_PRIME_SUBRING has_size_prime_subring
IDEALS_GENERATED_SING_EQ ideals_generated_sing_eq
IDEALS_GENERATED_SUBSET ideals_generated_subset
IDEAL_GENERATED_0 ideal_generated_0
IDEAL_GENERATED_2 ideal_generated_2
IDEAL_GENERATED_BY_EPIMORPHIC_IMAGE ideal_generated_by_epimorphic_image
IDEAL_GENERATED_BY_HOMOMORPHIC_IMAGE ideal_generated_by_homomorphic_image
IDEAL_GENERATED_BY_IDEAL_GENERATED ideal_generated_by_ideal_generated
IDEAL_GENERATED_CARTESIAN_PRODUCT ideal_generated_cartesian_product
IDEAL_GENERATED_COMPONENTWISE ideal_generated_componentwise
IDEAL_GENERATED_CROSS ideal_generated_cross
IDEAL_GENERATED_EMPTY ideal_generated_empty
IDEAL_GENERATED_EQ_0 ideal_generated_eq_0
IDEAL_GENERATED_EXPLICIT ideal_generated_explicit
IDEAL_GENERATED_FINITARY ideal_generated_finitary
IDEAL_GENERATED_FINITARY_ALT ideal_generated_finitary_alt
IDEAL_GENERATED_FINITE ideal_generated_finite
IDEAL_GENERATED_FINITE_IMAGE ideal_generated_finite_image
IDEAL_GENERATED_INC ideal_generated_inc
IDEAL_GENERATED_INC_GEN ideal_generated_inc_gen
IDEAL_GENERATED_INDUCT ideal_generated_induct
IDEAL_GENERATED_INDUCT_STRONG ideal_generated_induct_strong
IDEAL_GENERATED_INSERT ideal_generated_insert
IDEAL_GENERATED_INSERT_ZERO ideal_generated_insert_zero
IDEAL_GENERATED_MINIMAL ideal_generated_minimal
IDEAL_GENERATED_MINIMAL_EQ ideal_generated_minimal_eq
IDEAL_GENERATED_MONO ideal_generated_mono
IDEAL_GENERATED_NONEMPTY ideal_generated_nonempty
IDEAL_GENERATED_PAIRWISE ideal_generated_pairwise
IDEAL_GENERATED_REFL ideal_generated_refl
IDEAL_GENERATED_RESTRICT ideal_generated_restrict
IDEAL_GENERATED_RING_CARRIER ideal_generated_ring_carrier
IDEAL_GENERATED_RING_IDEAL ideal_generated_ring_ideal
IDEAL_GENERATED_RING_IDEAL_EQ ideal_generated_ring_ideal_eq
IDEAL_GENERATED_RING_LOCALIZATION ideal_generated_ring_localization
IDEAL_GENERATED_SCALE ideal_generated_scale
IDEAL_GENERATED_SETADD_SUBSET ideal_generated_setadd_subset
IDEAL_GENERATED_SING ideal_generated_sing
IDEAL_GENERATED_SING_ALT ideal_generated_sing_alt
IDEAL_GENERATED_SING_EQ_CARRIER ideal_generated_sing_eq_carrier
IDEAL_GENERATED_SING_SETMUL_LEFT ideal_generated_sing_setmul_left
IDEAL_GENERATED_SING_SETMUL_RIGHT ideal_generated_sing_setmul_right
IDEAL_GENERATED_SUBSET ideal_generated_subset
IDEAL_GENERATED_SUBSET_CARRIER ideal_generated_subset_carrier
IDEAL_GENERATED_SUBSET_CARRIER_SUBSET ideal_generated_subset_carrier_subset
IDEAL_GENERATED_UNION ideal_generated_union
IDEAL_LOCALIZATION_CONTRACTION ideal_localization_contraction
IMAGE_POLY_EVAL image_poly_eval
IMAGE_POLY_EXTEND image_poly_extend
IMAGE_POLY_EXTEND_1 image_poly_extend_1
IMAGE_RING_COSET_SWITCH image_ring_coset_switch
INFINITE_INTEGRAL_DOMAIN_POLY_EVAL_ALL_ZERO infinite_integral_domain_poly_eval_all_zero
INTEGER_MOD_RING integer_mod_ring_v1
INTEGER_MOD_RING_ASSOCIATES integer_mod_ring_associates
INTEGER_MOD_RING_CARRIER_REM integer_mod_ring_carrier_rem
INTEGER_MOD_RING_CHAR integer_mod_ring_char
INTEGER_MOD_RING_CLAUSES integer_mod_ring_clauses
INTEGER_MOD_RING_DIVIDES integer_mod_ring_divides
INTEGER_MOD_RING_OF_INT integer_mod_ring_of_int
INTEGER_MOD_RING_OF_NUM integer_mod_ring_of_num
INTEGER_MOD_RING_POW integer_mod_ring_pow
INTEGER_MOD_RING_RED_CONV integer_mod_ring_red_conv
INTEGER_MOD_RING_SUB integer_mod_ring_sub
INTEGER_MOD_RING_TRIVIAL integer_mod_ring_trivial
INTEGER_MOD_RING_UNIT integer_mod_ring_unit
INTEGER_QUOTIENT_RING_ISOMORPHIC_MOD integer_quotient_ring_isomorphic_mod
INTEGER_RING integer_ring_v1
INTEGER_RING_ASSOCIATES integer_ring_associates
INTEGER_RING_CHAR integer_ring_char
INTEGER_RING_COPRIME integer_ring_coprime
INTEGER_RING_COSET_IDEAL_GENERATED_SING integer_ring_coset_ideal_generated_sing
INTEGER_RING_DIVIDES integer_ring_divides
INTEGER_RING_GCD integer_ring_gcd
INTEGER_RING_IDEAL_GENERATED_SING integer_ring_ideal_generated_sing
INTEGER_RING_OF_INT integer_ring_of_int
INTEGER_RING_OF_NUM integer_ring_of_num
INTEGER_RING_POW integer_ring_pow
INTEGER_RING_UNIT integer_ring_unit
INTEGRAL_DOMAIN_10 integral_domain_10
INTEGRAL_DOMAIN_ASSOCIATES integral_domain_associates
INTEGRAL_DOMAIN_ASSOCIATES_LMUL2 integral_domain_associates_lmul2
INTEGRAL_DOMAIN_ASSOCIATES_RMUL2 integral_domain_associates_rmul2
INTEGRAL_DOMAIN_BOOL_RING integral_domain_bool_ring
INTEGRAL_DOMAIN_CHAR integral_domain_char
INTEGRAL_DOMAIN_DIVIDES_ASSOCIATES_MUL_SELF integral_domain_divides_associates_mul_self
INTEGRAL_DOMAIN_DIVIDES_LMUL2 integral_domain_divides_lmul2
INTEGRAL_DOMAIN_DIVIDES_MUL_SELF integral_domain_divides_mul_self
INTEGRAL_DOMAIN_DIVIDES_PRIME_LMUL integral_domain_divides_prime_lmul
INTEGRAL_DOMAIN_DIVIDES_PRIME_RMUL integral_domain_divides_prime_rmul
INTEGRAL_DOMAIN_DIVIDES_RMUL2 integral_domain_divides_rmul2
INTEGRAL_DOMAIN_EQ_ALL_REGULAR integral_domain_eq_all_regular
INTEGRAL_DOMAIN_EQ_NO_ZERODIVISORS integral_domain_eq_no_zerodivisors
INTEGRAL_DOMAIN_IMP_NONTRIVIAL_RING integral_domain_imp_nontrivial_ring
INTEGRAL_DOMAIN_INTEGER_MOD_RING integral_domain_integer_mod_ring
INTEGRAL_DOMAIN_INTEGER_RING integral_domain_integer_ring
INTEGRAL_DOMAIN_IRREDUCIBLE integral_domain_irreducible
INTEGRAL_DOMAIN_IRREDUCIBLE_ALT integral_domain_irreducible_alt
INTEGRAL_DOMAIN_IRREDUCIBLE_DIVISORS integral_domain_irreducible_divisors
INTEGRAL_DOMAIN_LOCALIZATION integral_domain_localization
INTEGRAL_DOMAIN_MONOMORPHIC_PREIMAGE integral_domain_monomorphic_preimage
INTEGRAL_DOMAIN_MUL_EQ_0 integral_domain_mul_eq_0
INTEGRAL_DOMAIN_MUL_EQ_SELF integral_domain_mul_eq_self
INTEGRAL_DOMAIN_MUL_LCANCEL integral_domain_mul_lcancel
INTEGRAL_DOMAIN_MUL_LCANCEL_EQ integral_domain_mul_lcancel_eq
INTEGRAL_DOMAIN_MUL_RCANCEL integral_domain_mul_rcancel
INTEGRAL_DOMAIN_MUL_RCANCEL_EQ integral_domain_mul_rcancel_eq
INTEGRAL_DOMAIN_NILPOTENT integral_domain_nilpotent
INTEGRAL_DOMAIN_NILRADICAL integral_domain_nilradical
INTEGRAL_DOMAIN_NONTRIVIAL integral_domain_nontrivial
INTEGRAL_DOMAIN_POLY_RING integral_domain_poly_ring
INTEGRAL_DOMAIN_POWSER_RING integral_domain_powser_ring
INTEGRAL_DOMAIN_POW_EQ_0 integral_domain_pow_eq_0
INTEGRAL_DOMAIN_PRIMES_COPRIME_OR_ASSOCIATES integral_domain_primes_coprime_or_associates
INTEGRAL_DOMAIN_PRIMES_DIVIDES_EQ_ASSOCIATES integral_domain_primes_divides_eq_associates
INTEGRAL_DOMAIN_PRIME_COPRIME_EQ integral_domain_prime_coprime_eq
INTEGRAL_DOMAIN_PRIME_DIVIDES_OR_COPRIME integral_domain_prime_divides_or_coprime
INTEGRAL_DOMAIN_PRIME_IMP_IRREDUCIBLE integral_domain_prime_imp_irreducible
INTEGRAL_DOMAIN_PRIME_PRODUCT_DIVIDES integral_domain_prime_product_divides
INTEGRAL_DOMAIN_PRODUCT_EQ_0 integral_domain_product_eq_0
INTEGRAL_DOMAIN_QUOTIENT_RING integral_domain_quotient_ring
INTEGRAL_DOMAIN_REAL_RING integral_domain_real_ring
INTEGRAL_DOMAIN_REGULAR integral_domain_regular
INTEGRAL_DOMAIN_RULE integral_domain_rule
INTEGRAL_DOMAIN_SUBRING_GENERATED integral_domain_subring_generated
INTEGRAL_DOMAIN_ZERODIVISOR integral_domain_zerodivisor
INTERS_PRIME_IDEALS inters_prime_ideals
IN_IDEAL_GENERATED_SELF in_ideal_generated_self
IN_IDEAL_GENERATED_SING in_ideal_generated_sing
IN_IDEAL_GENERATED_SING_EQ in_ideal_generated_sing_eq
IN_INTEGER_MOD_RING_CARRIER in_integer_mod_ring_carrier
IN_POLY_RING_CARRIER in_poly_ring_carrier
IN_POLY_RING_SUBRING_GENERATED_FINITARY in_poly_ring_subring_generated_finitary
IN_RING_COSET in_ring_coset
IN_RING_COSET_SELF in_ring_coset_self
IN_RING_IDEAL_0 in_ring_ideal_0
IN_RING_IDEAL_ADD in_ring_ideal_add
IN_RING_IDEAL_LMUL in_ring_ideal_lmul
IN_RING_IDEAL_MUL in_ring_ideal_mul
IN_RING_IDEAL_NEG in_ring_ideal_neg
IN_RING_IDEAL_RMUL in_ring_ideal_rmul
IN_RING_IDEAL_SUB in_ring_ideal_sub
IN_RING_IDEAL_SUM in_ring_ideal_sum
IN_RING_POLYNOMIAL_CARRIER_COMPOSE in_ring_polynomial_carrier_compose
IN_RING_POWERSERIES_CARRIER_COMPOSE in_ring_powerseries_carrier_compose
IN_SUBRING_0 in_subring_0
IN_SUBRING_1 in_subring_1
IN_SUBRING_ADD in_subring_add
IN_SUBRING_GENERATED_FINITARY in_subring_generated_finitary
IN_SUBRING_INT in_subring_int
IN_SUBRING_MUL in_subring_mul
IN_SUBRING_NEG in_subring_neg
IN_SUBRING_NUM in_subring_num
IN_SUBRING_POW in_subring_pow
IN_SUBRING_PRODUCT in_subring_product
IN_SUBRING_SUB in_subring_sub
IN_SUBRING_SUM in_subring_sum
IRREDUCIBLE_IMP_POLY_DEG_NZ irreducible_imp_poly_deg_nz
IRREDUCIBLE_PRIMITIVE_POLY_FRACTION_RING irreducible_primitive_poly_fraction_ring
ISOMORPHIC_COPY_OF_RING isomorphic_copy_of_ring
ISOMORPHIC_POLY_RINGS isomorphic_poly_rings
ISOMORPHIC_POLY_RING_TRIVIAL isomorphic_poly_ring_trivial
ISOMORPHIC_POWSER_RINGS isomorphic_powser_rings
ISOMORPHIC_POWSER_RING_TRIVIAL isomorphic_powser_ring_trivial
ISOMORPHIC_PRIME_SUBRING isomorphic_prime_subring
ISOMORPHIC_PRODUCT_RING_BIJECTIONS isomorphic_product_ring_bijections
ISOMORPHIC_PRODUCT_RING_DISJOINT_UNION isomorphic_product_ring_disjoint_union
ISOMORPHIC_PRODUCT_RING_INSERT isomorphic_product_ring_insert
ISOMORPHIC_PRODUCT_RING_SING isomorphic_product_ring_sing
ISOMORPHIC_PRODUCT_RING_SUPPORT isomorphic_product_ring_support
ISOMORPHIC_PRODUCT_RING_SYMDIFF isomorphic_product_ring_symdiff
ISOMORPHIC_PROD_INTEGER_MOD_RING isomorphic_prod_integer_mod_ring
ISOMORPHIC_PROD_TRIVIAL_RING isomorphic_prod_trivial_ring
ISOMORPHIC_RINGS_POLY_SUBRING_GENERATED isomorphic_rings_poly_subring_generated
ISOMORPHIC_RINGS_POWSER_SUBRING_GENERATED isomorphic_rings_powser_subring_generated
ISOMORPHIC_RING_BEZOUTNESS isomorphic_ring_bezoutness
ISOMORPHIC_RING_BOOLEANNESS isomorphic_ring_booleanness
ISOMORPHIC_RING_BOOL_RING isomorphic_ring_bool_ring
ISOMORPHIC_RING_CARD isomorphic_ring_card
ISOMORPHIC_RING_CARD_EQ isomorphic_ring_card_eq
ISOMORPHIC_RING_CHAR isomorphic_ring_char
ISOMORPHIC_RING_EQ isomorphic_ring_eq
ISOMORPHIC_RING_EUCLIDEANNESS isomorphic_ring_euclideanness
ISOMORPHIC_RING_FIELDNESS isomorphic_ring_fieldness
ISOMORPHIC_RING_FINITENESS isomorphic_ring_finiteness
ISOMORPHIC_RING_INFINITENESS isomorphic_ring_infiniteness
ISOMORPHIC_RING_INTEGRAL_DOMAINNESS isomorphic_ring_integral_domainness
ISOMORPHIC_RING_LOCALITY isomorphic_ring_locality
ISOMORPHIC_RING_NOETHERIANNESS isomorphic_ring_noetherianness
ISOMORPHIC_RING_PIDNESS isomorphic_ring_pidness
ISOMORPHIC_RING_POLY_POLY isomorphic_ring_poly_poly
ISOMORPHIC_RING_POLY_POLY_GEN isomorphic_ring_poly_poly_gen
ISOMORPHIC_RING_POWSER_POWSER isomorphic_ring_powser_powser
ISOMORPHIC_RING_POWSER_POWSER_GEN isomorphic_ring_powser_powser_gen
ISOMORPHIC_RING_PRODUCT_RING isomorphic_ring_product_ring
ISOMORPHIC_RING_PROD_RINGS isomorphic_ring_prod_rings
ISOMORPHIC_RING_PROD_RING_SWAP_LEFT isomorphic_ring_prod_ring_swap_left
ISOMORPHIC_RING_PROD_RING_SWAP_RIGHT isomorphic_ring_prod_ring_swap_right
ISOMORPHIC_RING_PROD_RING_SYM isomorphic_ring_prod_ring_sym
ISOMORPHIC_RING_REFL isomorphic_ring_refl
ISOMORPHIC_RING_SINGLETON_RING isomorphic_ring_singleton_ring
ISOMORPHIC_RING_SIZE isomorphic_ring_size
ISOMORPHIC_RING_SYM isomorphic_ring_sym
ISOMORPHIC_RING_TRANS isomorphic_ring_trans
ISOMORPHIC_RING_TRIVIALITY isomorphic_ring_triviality
ISOMORPHIC_RING_UFDNESS isomorphic_ring_ufdness
ISOMORPHIC_RING_VNREGULARITY isomorphic_ring_vnregularity
ISOMORPHIC_SUBCOPY_OF_RING isomorphic_subcopy_of_ring
ISOMORPHIC_TO_TRIVIAL_RING isomorphic_to_trivial_ring
ISOMORPHIC_TRANSPORT_OF_RING isomorphic_transport_of_ring
ISOMORPHIC_TRIVIAL_RINGS isomorphic_trivial_rings
KAPLANSKY_LEMMA kaplansky_lemma
LAGRANGE_THEOREM_RING lagrange_theorem_ring
LAGRANGE_THEOREM_RING_EXPLICIT lagrange_theorem_ring_explicit
LAMBDA_1_EQ lambda_1_eq
LOCALEQUIV_MUL_LCANCEL localequiv_mul_lcancel
LOCALEQUIV_MUL_RCANCEL localequiv_mul_rcancel
LOCAL_IMP_NONTRIVIAL_RING local_imp_nontrivial_ring
LOCAL_POWSER_RING local_powser_ring
LOCAL_QUOTIENT_RING local_quotient_ring
LOCAL_RING_EPIMORPHIC_IMAGE local_ring_epimorphic_image
LOCAL_RING_IDEAL_NONUNITS local_ring_ideal_nonunits
LOCAL_RING_LOCALIZATION local_ring_localization
MAKE_PRIMITIVE_IN_IDEAL make_primitive_in_ideal
MAXIMAL_AMONG_PRIME_IDEALS maximal_among_prime_ideals
MAXIMAL_CONTAINING_IDEAL_EXISTS maximal_containing_ideal_exists
MAXIMAL_EXCLUDING_IMP_PRIME_IDEAL maximal_excluding_imp_prime_ideal
MAXIMAL_IDEAL_0 maximal_ideal_0
MAXIMAL_IDEAL_CORRESPONDENCE maximal_ideal_correspondence
MAXIMAL_IDEAL_EPIMORPHIC_PREIMAGE maximal_ideal_epimorphic_preimage
MAXIMAL_IDEAL_EXISTS maximal_ideal_exists
MAXIMAL_IDEAL_IMP_PSUBSET maximal_ideal_imp_psubset
MAXIMAL_IDEAL_IMP_SUBSET maximal_ideal_imp_subset
MAXIMAL_IDEAL_ISOMORPHIC_IMAGE_EQ maximal_ideal_isomorphic_image_eq
MAXIMAL_IDEAL_NONUNITS maximal_ideal_nonunits
MAXIMAL_IDEAL_SING maximal_ideal_sing
MAXIMAL_IDEAL_SING_IMP_IRREDUCIBLE maximal_ideal_sing_imp_irreducible
MAXIMAL_IMP_PRIME_IDEAL maximal_imp_prime_ideal
MAXIMAL_IMP_PROPER_IDEAL maximal_imp_proper_ideal
MAXIMAL_IMP_RING_IDEAL maximal_imp_ring_ideal
MAXIMAL_NONFG_IMP_PRIME_IDEAL maximal_nonfg_imp_prime_ideal
MAXIMAL_SUPERIDEAL_EXISTS maximal_superideal_exists
MONIC_ASSOCIATES_EQ monic_associates_eq
MONIC_CMUL monic_cmul
MONIC_DEG_0 monic_deg_0
MONIC_IMP_NONZERO monic_imp_nonzero
MONIC_IN_TRIVIAL_RING monic_in_trivial_ring
MONIC_POLY_0 monic_poly_0
MONIC_POLY_1 monic_poly_1
MONIC_POLY_CONST monic_poly_const
MONIC_POLY_MUL monic_poly_mul
MONIC_POLY_POW monic_poly_pow
MONIC_POLY_PRODUCT monic_poly_product
MONIC_POLY_VAR monic_poly_var
MONIC_SUBRING_GENERATED monic_subring_generated
MONOIDAL_RING_ADD monoidal_ring_add
MONOIDAL_RING_MUL monoidal_ring_mul
MONOMIAL monomial_v1
MONOMIALS_POLY_REINDEX monomials_poly_reindex
MONOMIAL_1 monomial_1_v1
MONOMIAL_DEG monomial_deg_v1
MONOMIAL_DEG_1 monomial_deg_1
MONOMIAL_DEG_EQ_0 monomial_deg_eq_0
MONOMIAL_DEG_EQ_0_ALT monomial_deg_eq_0_alt
MONOMIAL_DEG_LE monomial_deg_le
MONOMIAL_DEG_LE_POLY_DEG monomial_deg_le_poly_deg
MONOMIAL_DEG_MUL monomial_deg_mul
MONOMIAL_DEG_ONE monomial_deg_one
MONOMIAL_DEG_UNIVARIATE monomial_deg_univariate
MONOMIAL_DEG_VAR monomial_deg_var
MONOMIAL_DIV monomial_div_v1
MONOMIAL_DIVIDES_1 monomial_divides_1
MONOMIAL_DIVIDES_ANTISYM monomial_divides_antisym
MONOMIAL_DIVIDES_EXISTS monomial_divides_exists
MONOMIAL_DIVIDES_LMUL monomial_divides_lmul
MONOMIAL_DIVIDES_REFL monomial_divides_refl
MONOMIAL_DIVIDES_RMUL monomial_divides_rmul
MONOMIAL_DIVIDES_TRANS monomial_divides_trans
MONOMIAL_DIVISOR monomial_divisor
MONOMIAL_DIVISORS_1 monomial_divisors_1
MONOMIAL_DIV_DIVIDES monomial_div_divides
MONOMIAL_DIV_LMUL monomial_div_lmul
MONOMIAL_DIV_LMUL_EQ monomial_div_lmul_eq
MONOMIAL_DIV_RMUL monomial_div_rmul
MONOMIAL_DIV_RMUL_EQ monomial_div_rmul_eq
MONOMIAL_FINITE_DIVISORPAIRS monomial_finite_divisorpairs
MONOMIAL_FINITE_DIVISORS monomial_finite_divisors
MONOMIAL_GE_1 monomial_ge_1
MONOMIAL_INDUCT monomial_induct
MONOMIAL_LET_ANTISYM monomial_let_antisym
MONOMIAL_LET_MUL2 monomial_let_mul2
MONOMIAL_LET_TRANS monomial_let_trans
MONOMIAL_LE_ANTISYM monomial_le_antisym
MONOMIAL_LE_DIVISOR monomial_le_divisor
MONOMIAL_LE_IMPROPERLY monomial_le_improperly
MONOMIAL_LE_LMUL monomial_le_lmul
MONOMIAL_LE_LT monomial_le_lt
MONOMIAL_LE_MONO monomial_le_mono
MONOMIAL_LE_MUL2 monomial_le_mul2
MONOMIAL_LE_POSET monomial_le_poset
MONOMIAL_LE_PROPERLY monomial_le_properly
MONOMIAL_LE_REFL monomial_le_refl
MONOMIAL_LE_RMUL monomial_le_rmul
MONOMIAL_LE_TOSET monomial_le_toset
MONOMIAL_LE_TRANS monomial_le_trans
MONOMIAL_LE_VARS monomial_le_vars
MONOMIAL_LE_VARS_EQ monomial_le_vars_eq
MONOMIAL_LTE_ANTISYM monomial_lte_antisym
MONOMIAL_LTE_MUL2 monomial_lte_mul2
MONOMIAL_LTE_TRANS monomial_lte_trans
MONOMIAL_LT_ANTISYM monomial_lt_antisym
MONOMIAL_LT_IMPROPERLY monomial_lt_improperly
MONOMIAL_LT_IMP_LE monomial_lt_imp_le
MONOMIAL_LT_LMUL monomial_lt_lmul
MONOMIAL_LT_MONO monomial_lt_mono
MONOMIAL_LT_MUL2 monomial_lt_mul2
MONOMIAL_LT_PROPERLY monomial_lt_properly
MONOMIAL_LT_REFL monomial_lt_refl
MONOMIAL_LT_RMUL monomial_lt_rmul
MONOMIAL_LT_TOSET monomial_lt_toset
MONOMIAL_LT_TRANS monomial_lt_trans
MONOMIAL_LT_VARS monomial_lt_vars
MONOMIAL_LT_VARS_EQ monomial_lt_vars_eq
MONOMIAL_MONO monomial_mono
MONOMIAL_MUL monomial_mul_v1
MONOMIAL_MUL_AC monomial_mul_ac
MONOMIAL_MUL_ASSOC monomial_mul_assoc
MONOMIAL_MUL_EQ_1 monomial_mul_eq_1
MONOMIAL_MUL_EQ_VAR monomial_mul_eq_var
MONOMIAL_MUL_LCANCEL monomial_mul_lcancel
MONOMIAL_MUL_LID monomial_mul_lid
MONOMIAL_MUL_RCANCEL monomial_mul_rcancel
MONOMIAL_MUL_RESTRICT monomial_mul_restrict
MONOMIAL_MUL_RID monomial_mul_rid
MONOMIAL_MUL_SYM monomial_mul_sym
MONOMIAL_MUL_VAR_ONE monomial_mul_var_one
MONOMIAL_POINTWISE_TAC monomial_pointwise_tac
MONOMIAL_RESTRICT monomial_restrict_v1
MONOMIAL_RESTRICT_EQ monomial_restrict_eq
MONOMIAL_RESTRICT_MUL monomial_restrict_mul
MONOMIAL_RESTRICT_REFL monomial_restrict_refl
MONOMIAL_RULE monomial_rule
MONOMIAL_TAC monomial_tac
MONOMIAL_UNIV monomial_univ
MONOMIAL_UNIV_1 monomial_univ_1
MONOMIAL_VAR monomial_var_v1
MONOMIAL_VARS_1 monomial_vars_1
MONOMIAL_VARS_DIVISOR monomial_vars_divisor
MONOMIAL_VARS_EQ_EMPTY monomial_vars_eq_empty
MONOMIAL_VARS_MUL monomial_vars_mul
MONOMIAL_VARS_RESTRICT monomial_vars_restrict
MONOMIAL_VARS_UNIVARIATE monomial_vars_univariate
MONOMIAL_VARS_VAR monomial_vars_var
MONOMIAL_VAR_1 monomial_var_1
MONOMIAL_VAR_DIVIDES monomial_var_divides
MONOMIAL_VAR_DIVIDES_MUL monomial_var_divides_mul
MONOMIAL_VAR_EQ monomial_var_eq
NEUTRAL_RING_ADD neutral_ring_add
NEUTRAL_RING_MUL neutral_ring_mul
NOETHERIAN_DOMAIN_ATOMIC noetherian_domain_atomic
NOETHERIAN_DOMAIN_IRREDUCIBLE_FACTOR_EXISTS noetherian_domain_irreducible_factor_exists
NOETHERIAN_LOCAL_RING_LOCALIZATION noetherian_local_ring_localization
NOETHERIAN_POLY_RING noetherian_poly_ring
NOETHERIAN_POLY_RING_1 noetherian_poly_ring_1
NOETHERIAN_POWSER_RING noetherian_powser_ring
NOETHERIAN_POWSER_RING_1 noetherian_powser_ring_1
NOETHERIAN_PRODUCT_RING noetherian_product_ring
NOETHERIAN_PROD_RING noetherian_prod_ring
NOETHERIAN_QUOTIENT_RING noetherian_quotient_ring
NOETHERIAN_RING noetherian_ring_v1
NOETHERIAN_RING_EPIMORPHIC_IMAGE noetherian_ring_epimorphic_image
NOETHERIAN_RING_EQ_ACC noetherian_ring_eq_acc
NOETHERIAN_RING_EQ_FG_PRIME_IDEALS noetherian_ring_eq_fg_prime_ideals
NOETHERIAN_RING_EQ_MAXIMAL noetherian_ring_eq_maximal
NOETHERIAN_RING_LOCALIZATION noetherian_ring_localization
NONFINITELY_GENERATED_IMP_PROPER_IDEAL nonfinitely_generated_imp_proper_ideal
NONPRINCIPAL_IMP_PROPER_IDEAL nonprincipal_imp_proper_ideal
NOT_FIELD_INTEGER_RING not_field_integer_ring
NOT_TRIVIAL_BOOL_RING not_trivial_bool_ring
NOT_TRIVIAL_INTEGER_RING not_trivial_integer_ring
PAIRWISE_DISJOINT_RING_COSETS pairwise_disjoint_ring_cosets
PID pid
PID_EQ_ACCP_BEZOUT_DOMAIN pid_eq_accp_bezout_domain
PID_EQ_BEZOUT_ATOMIC pid_eq_bezout_atomic
PID_EQ_INTEGRAL_DOMAIN_PRIME_PRINCIPAL pid_eq_integral_domain_prime_principal
PID_EQ_NOETHERIAN_BEZOUT_DOMAIN pid_eq_noetherian_bezout_domain
PID_EQ_UFD_BEZOUT_RING pid_eq_ufd_bezout_ring
PID_EQ_UFD_PRIME_MAXIMAL pid_eq_ufd_prime_maximal
PID_IMP_BEZOUT_RING pid_imp_bezout_ring
PID_IMP_INTEGRAL_DOMAIN pid_imp_integral_domain
PID_IMP_NOETHERIAN_RING pid_imp_noetherian_ring
PID_IMP_UFD pid_imp_ufd
PID_INTEGER_RING pid_integer_ring
PID_IRREDUCIBLE_EQ_PRIME pid_irreducible_eq_prime
PID_MAXIMAL_EQ_PRIME_IDEAL pid_maximal_eq_prime_ideal
PID_POLY_RING pid_poly_ring
PID_RING_LOCALIZATION pid_ring_localization
POLY_0 poly_0_v1
POLY_ADD_ASSOC poly_add_assoc
POLY_ADD_LDISTRIB poly_add_ldistrib
POLY_ADD_LNEG poly_add_lneg
POLY_ADD_LZERO poly_add_lzero
POLY_ADD_RZERO poly_add_rzero
POLY_ADD_SYM poly_add_sym
POLY_CARRIER_SUBRING_OF_POWSER_RING poly_carrier_subring_of_powser_ring
POLY_CLAUSES poly_clauses
POLY_CLEAR_DENOMINATORS poly_clear_denominators
POLY_COMPOSE_HOMOMORPHISM_ADD poly_compose_homomorphism_add
POLY_COMPOSE_HOMOMORPHISM_CONST poly_compose_homomorphism_const
POLY_COMPOSE_HOMOMORPHISM_MUL poly_compose_homomorphism_mul
POLY_COMPOSE_HOMOMORPHISM_NEG poly_compose_homomorphism_neg
POLY_COMPOSE_HOMOMORPHISM_POW poly_compose_homomorphism_pow
POLY_COMPOSE_HOMOMORPHISM_SUB poly_compose_homomorphism_sub
POLY_COMPOSE_HOMOMORPHISM_VAR poly_compose_homomorphism_var
POLY_CONST poly_const_v1
POLY_CONST_0 poly_const_0
POLY_CONST_1 poly_const_1
POLY_CONST_ADD poly_const_add
POLY_CONST_DIVIDES_COEFFS poly_const_divides_coeffs
POLY_CONST_DIVIDES_COEFFS_EQ poly_const_divides_coeffs_eq
POLY_CONST_DIVIDES_COEFFS_REV poly_const_divides_coeffs_rev
POLY_CONST_DIVIDES_CONST poly_const_divides_const
POLY_CONST_EQ poly_const_eq
POLY_CONST_EQ_0 poly_const_eq_0
POLY_CONST_EQ_1 poly_const_eq_1
POLY_CONST_MUL poly_const_mul
POLY_CONST_NEG poly_const_neg
POLY_CONST_OF_NUM poly_const_of_num
POLY_CONST_SUBRING_GENERATED poly_const_subring_generated
POLY_DEG_0 poly_deg_0
POLY_DEG_1 poly_deg_1
POLY_DEG_1_IMP_IRREDUCIBLE poly_deg_1_imp_irreducible
POLY_DEG_1_ROOT poly_deg_1_root
POLY_DEG_ADD poly_deg_add
POLY_DEG_ADD_LE poly_deg_add_le
POLY_DEG_CMUL poly_deg_cmul
POLY_DEG_CONST poly_deg_const
POLY_DEG_DERIV poly_deg_deriv
POLY_DEG_DERIV_LE poly_deg_deriv_le
POLY_DEG_DIVIDES_LE poly_deg_divides_le
POLY_DEG_DIVIDES_LE_MONIC poly_deg_divides_le_monic
POLY_DEG_DIVIDES_LE_UNIVARIATE poly_deg_divides_le_univariate
POLY_DEG_EQ poly_deg_eq
POLY_DEG_EQ_0 poly_deg_eq_0
POLY_DEG_EQ_0_ALT poly_deg_eq_0_alt
POLY_DEG_EQ_0_UNIT poly_deg_eq_0_unit
POLY_DEG_EQ_COEFF poly_deg_eq_coeff
POLY_DEG_EQ_COEFF_EQ poly_deg_eq_coeff_eq
POLY_DEG_EQ_FROM_LE poly_deg_eq_from_le
POLY_DEG_GE poly_deg_ge
POLY_DEG_GE_COEFF poly_deg_ge_coeff
POLY_DEG_GE_COEFF_EQ poly_deg_ge_coeff_eq
POLY_DEG_GE_EQ poly_deg_ge_eq
POLY_DEG_HOMOMORPHIC_IMAGE poly_deg_homomorphic_image
POLY_DEG_LE poly_deg_le
POLY_DEG_LE_COEFF poly_deg_le_coeff
POLY_DEG_LE_COEFF_EQ poly_deg_le_coeff_eq
POLY_DEG_LE_EQ poly_deg_le_eq
POLY_DEG_LT_FROM_LE poly_deg_lt_from_le
POLY_DEG_MONOMIAL_EXISTS poly_deg_monomial_exists
POLY_DEG_MONOMORPHIC_IMAGE poly_deg_monomorphic_image
POLY_DEG_MUL poly_deg_mul
POLY_DEG_MUL_LE poly_deg_mul_le
POLY_DEG_MUL_MONIC poly_deg_mul_monic
POLY_DEG_MUL_UNIVARIATE poly_deg_mul_univariate
POLY_DEG_MUL_VAR poly_deg_mul_var
POLY_DEG_MUL_VARPOW poly_deg_mul_varpow
POLY_DEG_MUL_X_MINUS_A poly_deg_mul_x_minus_a
POLY_DEG_NEG poly_deg_neg
POLY_DEG_POW poly_deg_pow
POLY_DEG_POW_LE poly_deg_pow_le
POLY_DEG_RECIP poly_deg_recip
POLY_DEG_RECIP_LE poly_deg_recip_le
POLY_DEG_REM poly_deg_rem
POLY_DEG_REM_ALT poly_deg_rem_alt
POLY_DEG_RING_ADD_LE poly_deg_ring_add_le
POLY_DEG_RING_SUB_LE poly_deg_ring_sub_le
POLY_DEG_RING_SUM_LE poly_deg_ring_sum_le
POLY_DEG_SUB poly_deg_sub
POLY_DEG_SUBRING_GENERATED poly_deg_subring_generated
POLY_DEG_SUB_LE poly_deg_sub_le
POLY_DEG_UNIQUE poly_deg_unique
POLY_DEG_UNIT poly_deg_unit
POLY_DEG_VAR poly_deg_var
POLY_DEG_VARPOW_MUL poly_deg_varpow_mul
POLY_DEG_VAR_MUL poly_deg_var_mul
POLY_DEG_VAR_POW poly_deg_var_pow
POLY_DEG_X_MINUS_A poly_deg_x_minus_a
POLY_DERIV_0 poly_deriv_0
POLY_DERIV_1 poly_deriv_1
POLY_DERIV_ADD poly_deriv_add
POLY_DERIV_CMUL poly_deriv_cmul
POLY_DERIV_CONST poly_deriv_const
POLY_DERIV_HOMOMORPHIC_IMAGE poly_deriv_homomorphic_image
POLY_DERIV_IN_CARRIER poly_deriv_in_carrier
POLY_DERIV_MUL poly_deriv_mul
POLY_DERIV_NEG poly_deriv_neg
POLY_DERIV_NONZERO_CHAR0 poly_deriv_nonzero_char0
POLY_DERIV_POW poly_deriv_pow
POLY_DERIV_PRODUCT poly_deriv_product
POLY_DERIV_SUB poly_deriv_sub
POLY_DERIV_SUBRING_GENERATED poly_deriv_subring_generated
POLY_DERIV_SUM poly_deriv_sum
POLY_DERIV_VAR poly_deriv_var
POLY_DERIV_VAR_POW poly_deriv_var_pow
POLY_DIV poly_div_v1
POLY_DIVIDES_RECIP poly_divides_recip
POLY_DIVIDES_RECIP_EQ poly_divides_recip_eq
POLY_DIVIDES_RECIP_GALOIS poly_divides_recip_galois
POLY_DIVIDES_RECIP_RECIP poly_divides_recip_recip
POLY_DIVIDES_REM poly_divides_rem
POLY_DIVIDES_X_MINUS_A poly_divides_x_minus_a
POLY_DIVIDES_X_MINUS_ROOT poly_divides_x_minus_root
POLY_DIVIDES_X_MINUS_ROOT_EQ poly_divides_x_minus_root_eq
POLY_DIVISION poly_division
POLY_DIVISION_GEN poly_division_gen
POLY_DIV_REM poly_div_rem
POLY_DIV_REM_SIMP poly_div_rem_simp
POLY_EQ_0_MONOMORPHIC_IMAGE poly_eq_0_monomorphic_image
POLY_EVAL poly_eval_v1
POLY_EVALUATE poly_evaluate_v1
POLY_EVALUATE_0 poly_evaluate_0
POLY_EVALUATE_1 poly_evaluate_1
POLY_EVALUATE_ADD poly_evaluate_add
POLY_EVALUATE_AT_0 poly_evaluate_at_0
POLY_EVALUATE_CONST poly_evaluate_const
POLY_EVALUATE_EQ poly_evaluate_eq
POLY_EVALUATE_HOMOMORPHIC_IMAGE poly_evaluate_homomorphic_image
POLY_EVALUATE_MUL poly_evaluate_mul
POLY_EVALUATE_POW poly_evaluate_pow
POLY_EVALUATE_REINDEX poly_evaluate_reindex
POLY_EVALUATE_RING_PRODUCT poly_evaluate_ring_product
POLY_EVALUATE_RING_SUM poly_evaluate_ring_sum
POLY_EVALUATE_SUB poly_evaluate_sub
POLY_EVALUATE_VAR poly_evaluate_var
POLY_EVAL_0 poly_eval_0
POLY_EVAL_1 poly_eval_1
POLY_EVAL_ADD poly_eval_add
POLY_EVAL_AT_0 poly_eval_at_0
POLY_EVAL_COEFF poly_eval_coeff
POLY_EVAL_CONST poly_eval_const
POLY_EVAL_EXPAND poly_eval_expand
POLY_EVAL_HOMOMORPHIC_IMAGE poly_eval_homomorphic_image
POLY_EVAL_MUL poly_eval_mul
POLY_EVAL_POW poly_eval_pow
POLY_EVAL_RECIP poly_eval_recip
POLY_EVAL_RING_PRODUCT poly_eval_ring_product
POLY_EVAL_RING_SUM poly_eval_ring_sum
POLY_EVAL_SUB poly_eval_sub
POLY_EVAL_VAR poly_eval_var
POLY_EXPAND poly_expand
POLY_EXTEND poly_extend_v1
POLY_EXTEND_0 poly_extend_0
POLY_EXTEND_1 poly_extend_1
POLY_EXTEND_ADD poly_extend_add
POLY_EXTEND_AT_0 poly_extend_at_0
POLY_EXTEND_COMPOSE poly_extend_compose
POLY_EXTEND_CONST poly_extend_const
POLY_EXTEND_EQ poly_extend_eq
POLY_EXTEND_EVALUATE poly_extend_evaluate
POLY_EXTEND_EXTEND poly_extend_extend
POLY_EXTEND_FROM_SUBRING_GENERATED poly_extend_from_subring_generated
POLY_EXTEND_HOMOMORPHIC_IMAGE poly_extend_homomorphic_image
POLY_EXTEND_ID poly_extend_id
POLY_EXTEND_INTO_SUBRING_GENERATED poly_extend_into_subring_generated
POLY_EXTEND_MUL poly_extend_mul
POLY_EXTEND_NEG poly_extend_neg
POLY_EXTEND_POLYNOMIAL poly_extend_polynomial
POLY_EXTEND_POW poly_extend_pow
POLY_EXTEND_REINDEX poly_extend_reindex
POLY_EXTEND_RING_PRODUCT poly_extend_ring_product
POLY_EXTEND_RING_SUM poly_extend_ring_sum
POLY_EXTEND_SUB poly_extend_sub
POLY_EXTEND_SUPERSET poly_extend_superset
POLY_EXTEND_UNIQUE poly_extend_unique
POLY_EXTEND_UNIVARIATE poly_extend_univariate
POLY_EXTEND_VAR poly_extend_var
POLY_IN_POWSER_RING poly_in_powser_ring
POLY_IRREDUCIBLE_IMP_SEPARABLE poly_irreducible_imp_separable
POLY_MAKE_PRIMITIVE poly_make_primitive
POLY_MONOMIALS poly_monomials
POLY_MONOMIALS_ALT poly_monomials_alt
POLY_MONOMIALS_FINITE poly_monomials_finite
POLY_MONOMIAL_IN_CARRIER poly_monomial_in_carrier
POLY_MUL_0 poly_mul_0
POLY_MUL_ASSOC poly_mul_assoc
POLY_MUL_CONST poly_mul_const
POLY_MUL_LEADING_COEFF poly_mul_leading_coeff
POLY_MUL_LID poly_mul_lid
POLY_MUL_MONOMIAL_1 poly_mul_monomial_1
POLY_MUL_RID poly_mul_rid
POLY_MUL_SYM poly_mul_sym
POLY_MUL_UNIVARIATE poly_mul_univariate
POLY_MUL_VAR poly_mul_var
POLY_NONCONSTANT_IRREDUCIBLE_IMP_SEPARABLE poly_nonconstant_irreducible_imp_separable
POLY_POLY_DEG_EQ_0 poly_poly_deg_eq_0
POLY_POW poly_pow_v1
POLY_POW_0 poly_pow_0
POLY_POW_1 poly_pow_1
POLY_POW_ALT poly_pow_alt
POLY_PRIMITIVE_CONST_CANCEL poly_primitive_const_cancel
POLY_RECIP_0 poly_recip_0
POLY_RECIP_1 poly_recip_1
POLY_RECIP_CONST poly_recip_const
POLY_RECIP_EQ_0 poly_recip_eq_0
POLY_RECIP_IN_CARRIER poly_recip_in_carrier
POLY_RECIP_MUL poly_recip_mul
POLY_RECIP_MUL_GEN poly_recip_mul_gen
POLY_RECIP_NEG poly_recip_neg
POLY_RECIP_RECIP poly_recip_recip
POLY_RECIP_RECIP_EQ poly_recip_recip_eq
POLY_REINDEX_CONST poly_reindex_const
POLY_REINDEX_VAR poly_reindex_var
POLY_REM poly_rem_v1
POLY_REM_UNIQUE poly_rem_unique
POLY_RING poly_ring_v1
POLY_RING_AS_SUBRING poly_ring_as_subring
POLY_RING_AS_SUBRING_ALT poly_ring_as_subring_alt
POLY_RING_AS_SUBRING_FINITE poly_ring_as_subring_finite
POLY_RING_CLAUSES poly_ring_clauses
POLY_RING_EPIMORPHISM_COEFF_0 poly_ring_epimorphism_coeff_0
POLY_RING_EQ poly_ring_eq
POLY_RING_EQ_IMP poly_ring_eq_imp
POLY_RING_EXPAND poly_ring_expand
POLY_RING_HOMOMORPHISM_COEFF_0 poly_ring_homomorphism_coeff_0
POLY_RING_HOMOMORPHISM_I poly_ring_homomorphism_i
POLY_RING_HOMOMORPHISM_UNIQUE poly_ring_homomorphism_unique
POLY_RING_INDUCT poly_ring_induct
POLY_RING_INDUCT_STRONG poly_ring_induct_strong
POLY_RING_IN_FINITE_VARIABLES poly_ring_in_finite_variables
POLY_RING_IN_POLY_VARS poly_ring_in_poly_vars
POLY_RING_MONO poly_ring_mono
POLY_RING_POLY_VARS poly_ring_poly_vars
POLY_RING_PRODUCT_VAR poly_ring_product_var
POLY_RING_PRODUCT_VAR_POW poly_ring_product_var_pow
POLY_RING_SUBRING_OF_POWSER_RING poly_ring_subring_of_powser_ring
POLY_RING_VAR_POW poly_ring_var_pow
POLY_ROOT_BOUND poly_root_bound
POLY_ROOT_COUNT_IMP_SQUAREFREE poly_root_count_imp_squarefree
POLY_SEPARABLE_EQ_SQUAREFREE poly_separable_eq_squarefree
POLY_SEPARABLE_IMP_SQUAREFREE poly_separable_imp_squarefree
POLY_SQUAREFREE_IMP_SEPARABLE poly_squarefree_imp_separable
POLY_SQUARE_DIVIDES_DERIV poly_square_divides_deriv
POLY_SQUARE_DIVIDES_DERIV_EQ poly_square_divides_deriv_eq
POLY_SUB poly_sub_v1
POLY_SUBRING_GENERATED poly_subring_generated
POLY_SUBRING_GENERATED_1 poly_subring_generated_1
POLY_SUBRING_GENERATED_CLAUSES poly_subring_generated_clauses
POLY_SUM poly_sum
POLY_TOP_EQ_0 poly_top_eq_0
POLY_TOP_MONOMIAL_LE poly_top_monomial_le
POLY_TOP_MONOMIAL_LT poly_top_monomial_lt
POLY_TOP_NONZERO poly_top_nonzero
POLY_TOP_TAIL poly_top_tail
POLY_VAR poly_var_v1
POLY_VARPOW_RECIP_RECIP poly_varpow_recip_recip
POLY_VARS_0 poly_vars_0
POLY_VARS_1 poly_vars_1
POLY_VARS_ADD poly_vars_add
POLY_VARS_CONST poly_vars_const
POLY_VARS_MUL poly_vars_mul
POLY_VARS_MUL_EQ poly_vars_mul_eq
POLY_VARS_NEG poly_vars_neg
POLY_VARS_POW poly_vars_pow
POLY_VARS_POW_EQ poly_vars_pow_eq
POLY_VARS_REINDEX poly_vars_reindex
POLY_VARS_VAR poly_vars_var
POLY_VAR_DIVIDES_UNIVARIATE poly_var_divides_univariate
POLY_VAR_EQ_CONST poly_var_eq_const
POLY_VAR_MONOMIAL_1 poly_var_monomial_1
POLY_VAR_MUL poly_var_mul
POLY_VAR_UNIV poly_var_univ
POLY_X_MINUS_A_IN_CARRIER poly_x_minus_a_in_carrier
POLY_X_MINUS_A_NONZERO poly_x_minus_a_nonzero
POSET_MONOMIAL_DIVIDES poset_monomial_divides
POSET_MONOMIAL_LE poset_monomial_le
POWSER_CLAUSES powser_clauses
POWSER_CONST powser_const
POWSER_DERIV_IN_CARRIER powser_deriv_in_carrier
POWSER_EVALUATE_AT_0 powser_evaluate_at_0
POWSER_EVAL_AT_0 powser_eval_at_0
POWSER_EXTEND_AT_0 powser_extend_at_0
POWSER_MONOMIALS powser_monomials
POWSER_MONOMIAL_IN_CARRIER powser_monomial_in_carrier
POWSER_MUL_0 powser_mul_0
POWSER_MUL_CONST powser_mul_const
POWSER_MUL_MONOMIAL_1 powser_mul_monomial_1
POWSER_MUL_VAR powser_mul_var
POWSER_RING powser_ring_v1
POWSER_RING_CLAUSES powser_ring_clauses
POWSER_RING_EPIMORPHISM_COEFF_0 powser_ring_epimorphism_coeff_0
POWSER_RING_EQ powser_ring_eq
POWSER_RING_EQ_IMP powser_ring_eq_imp
POWSER_RING_HOMOMORPHISM_COEFF_0 powser_ring_homomorphism_coeff_0
POWSER_RING_MONO powser_ring_mono
POWSER_SUM powser_sum
POWSER_VAR powser_var
POWSER_VARPOW_MUL_EQ_0 powser_varpow_mul_eq_0
POWSER_VAR_MUL powser_var_mul
POWSER_VAR_MUL_EQ_0 powser_var_mul_eq_0
POWSER_VAR_UNIV powser_var_univ
PRIME_IDEAL_0 prime_ideal_0
PRIME_IDEAL_CONTAINS_NILPOTENTS prime_ideal_contains_nilpotents
PRIME_IDEAL_CORRESPONDENCE prime_ideal_correspondence
PRIME_IDEAL_EXCLUDING_EXISTS prime_ideal_excluding_exists
PRIME_IDEAL_EXISTS prime_ideal_exists
PRIME_IDEAL_HOMOMORPHIC_PREIMAGE prime_ideal_homomorphic_preimage
PRIME_IDEAL_IMP_PSUBSET prime_ideal_imp_psubset
PRIME_IDEAL_IMP_SUBSET prime_ideal_imp_subset
PRIME_IDEAL_ISOMORPHIC_IMAGE_EQ prime_ideal_isomorphic_image_eq
PRIME_IDEAL_LOCALIZATION prime_ideal_localization
PRIME_IDEAL_LOCALIZATION_CONTRACTION prime_ideal_localization_contraction
PRIME_IDEAL_LOCALIZATION_EXISTS prime_ideal_localization_exists
PRIME_IDEAL_NONUNITS prime_ideal_nonunits
PRIME_IDEAL_SING prime_ideal_sing
PRIME_IMP_PROPER_IDEAL prime_imp_proper_ideal
PRIME_IMP_RING_IDEAL prime_imp_ring_ideal
PRIME_SUBRING prime_subring
PRIME_SUBRING_FINITE prime_subring_finite
PRIME_SUBRING_MINIMAL prime_subring_minimal
PRIME_SUPERIDEAL_EXCLUDING_EXISTS prime_superideal_excluding_exists
PRIME_SUPERIDEAL_EXISTS prime_superideal_exists
PRINCIPAL_IDEAL_0 principal_ideal_0
PRINCIPAL_IDEAL_ALT principal_ideal_alt
PRINCIPAL_IDEAL_CARRIER principal_ideal_carrier
PRINCIPAL_IDEAL_EPIMORPHIC_IMAGE principal_ideal_epimorphic_image
PRINCIPAL_IDEAL_IDEAL_GENERATED_SING principal_ideal_ideal_generated_sing
PRINCIPAL_IDEAL_IMP_SUBSET principal_ideal_imp_subset
PRINCIPAL_IDEAL_LOCALIZATION principal_ideal_localization
PRINCIPAL_IMP_FINITELY_GENERATED_IDEAL principal_imp_finitely_generated_ideal
PRINCIPAL_IMP_RING_IDEAL principal_imp_ring_ideal
PRODUCT_RING product_ring_v1
PRODUCT_RING_SUBRING_GENERATED product_ring_subring_generated
PROD_RING prod_ring_v1
PROD_RING_SUBRING_GENERATED prod_ring_subring_generated
PROPERLY_MONOMIAL_LE properly_monomial_le
PROPER_IDEAL proper_ideal_v1
PROPER_IDEAL_0 proper_ideal_0
PROPER_IDEAL_ALT proper_ideal_alt
PROPER_IDEAL_CORRESPONDENCE proper_ideal_correspondence
PROPER_IDEAL_EXISTS proper_ideal_exists
PROPER_IDEAL_HOMOMORPHIC_PREIMAGE proper_ideal_homomorphic_preimage
PROPER_IDEAL_IDEAL_GENERATED_SING proper_ideal_ideal_generated_sing
PROPER_IDEAL_IMP_PSUBSET proper_ideal_imp_psubset
PROPER_IDEAL_IMP_SUBSET proper_ideal_imp_subset
PROPER_IDEAL_ISOMORPHIC_IMAGE_EQ proper_ideal_isomorphic_image_eq
PROPER_IDEAL_LOCALIZATION proper_ideal_localization
PROPER_IDEAL_NONUNITS proper_ideal_nonunits
PROPER_IDEAL_SUBSET_NONUNITS proper_ideal_subset_nonunits
PROPER_IDEAL_UNIONS proper_ideal_unions
PROPER_IDEAL_UNIT proper_ideal_unit
PROPER_IMP_RING_IDEAL proper_imp_ring_ideal
PROPER_RADICAL proper_radical
PSUBSET_IDEALS_GENERATED_SING psubset_ideals_generated_sing
QOSET_MONOMIAL_LE qoset_monomial_le
QUOTIENT_RING quotient_ring_v1
QUOTIENT_RING_0 quotient_ring_0
QUOTIENT_RING_1 quotient_ring_1
QUOTIENT_RING_ADD quotient_ring_add
QUOTIENT_RING_CARRIER quotient_ring_carrier
QUOTIENT_RING_IDEAL_CORRESPONDENCE quotient_ring_ideal_correspondence
QUOTIENT_RING_MUL quotient_ring_mul
QUOTIENT_RING_NEG quotient_ring_neg
QUOTIENT_RING_SUBRING_CORRESPONDENCE quotient_ring_subring_correspondence
QUOTIENT_RING_UNIVERSAL quotient_ring_universal
QUOTIENT_RING_UNIVERSAL_EPIMORPHISM quotient_ring_universal_epimorphism
QUOTIENT_RING_UNIVERSAL_EXPLICIT quotient_ring_universal_explicit
RADICAL radical_v1
RADICAL_0 radical_0
RADICAL_ALT radical_alt
RADICAL_EQ_CARRIER radical_eq_carrier
RADICAL_IDEAL_PRIME_IDEAL_EQ radical_ideal_prime_ideal_eq
RADICAL_INTER radical_inter
RADICAL_MONO radical_mono
RADICAL_PRIME_IDEAL radical_prime_ideal
RADICAL_RADICAL radical_radical
RADICAL_RING_CARRIER radical_ring_carrier
RADICAL_SETADD radical_setadd
RADICAL_SUBSET radical_subset
RADICAL_SUBSET_PRIME_IDEAL_EQ radical_subset_prime_ideal_eq
RADICAL_UNION radical_union
RADICAL_UNIONS radical_unions
REAL_FIELD_CLAUSES real_field_clauses
REAL_RING_CHAR real_ring_char
REAL_RING_CLAUSES real_ring_clauses
REAL_RING_DIV real_ring_div
REAL_RING_INV real_ring_inv
REAL_RING_OF_INT real_ring_of_int
REAL_RING_OF_NUM real_ring_of_num
REAL_RING_POW real_ring_pow
REAL_RING_SUB real_ring_sub
REPEATED_ROOT_POLY_DERIV_ZERO repeated_root_poly_deriv_zero
RINGS_EQ rings_eq
RING_0 ring_0_v1
RING_0_IN_SUBRING_GENERATED ring_0_in_subring_generated
RING_1 ring_1_v1
RING_1_DIV ring_1_div
RING_1_IN_SUBRING_GENERATED ring_1_in_subring_generated
RING_1_NOT_IN_PRIME_IDEAL ring_1_not_in_prime_ideal
RING_ACCP ring_accp
RING_ADD ring_add_v1
RING_ADD_AC ring_add_ac
RING_ADD_ASSOC ring_add_assoc
RING_ADD_EQ_0 ring_add_eq_0
RING_ADD_EQ_LEFT ring_add_eq_left
RING_ADD_EQ_RIGHT ring_add_eq_right
RING_ADD_IN_SETADD ring_add_in_setadd
RING_ADD_IN_SUBRING_GENERATED ring_add_in_subring_generated
RING_ADD_LCANCEL ring_add_lcancel
RING_ADD_LCANCEL_IMP ring_add_lcancel_imp
RING_ADD_LDISTRIB ring_add_ldistrib
RING_ADD_LNEG ring_add_lneg
RING_ADD_LZERO ring_add_lzero
RING_ADD_RCANCEL ring_add_rcancel
RING_ADD_RCANCEL_IMP ring_add_rcancel_imp
RING_ADD_RDISTRIB ring_add_rdistrib
RING_ADD_RNEG ring_add_rneg
RING_ADD_RZERO ring_add_rzero
RING_ADD_SYM ring_add_sym
RING_ASSOCIATES_0 ring_associates_0
RING_ASSOCIATES_1 ring_associates_1
RING_ASSOCIATES_ASSOCIATES ring_associates_associates
RING_ASSOCIATES_COPRIME ring_associates_coprime
RING_ASSOCIATES_DIVIDES ring_associates_divides
RING_ASSOCIATES_EQ_0 ring_associates_eq_0
RING_ASSOCIATES_HOMOMORPHIC_IMAGE ring_associates_homomorphic_image
RING_ASSOCIATES_IN_CARRIER ring_associates_in_carrier
RING_ASSOCIATES_IN_IDEAL ring_associates_in_ideal
RING_ASSOCIATES_IRREDUCIBLE ring_associates_irreducible
RING_ASSOCIATES_ISOMORPHIC_IMAGE_EQ ring_associates_isomorphic_image_eq
RING_ASSOCIATES_LMUL ring_associates_lmul
RING_ASSOCIATES_LNEG ring_associates_lneg
RING_ASSOCIATES_MUL ring_associates_mul
RING_ASSOCIATES_NEG ring_associates_neg
RING_ASSOCIATES_NEG_EQ ring_associates_neg_eq
RING_ASSOCIATES_NILPOTENT ring_associates_nilpotent
RING_ASSOCIATES_POW ring_associates_pow
RING_ASSOCIATES_PRIME ring_associates_prime
RING_ASSOCIATES_PRIMEFACTS_BIJECTION ring_associates_primefacts_bijection
RING_ASSOCIATES_PRIMEFACTS_BIJECTIONS ring_associates_primefacts_bijections
RING_ASSOCIATES_PRIMEFACTS_BIJECTIONS_EQ ring_associates_primefacts_bijections_eq
RING_ASSOCIATES_PRIMEFACTS_BIJECTION_EQ ring_associates_primefacts_bijection_eq
RING_ASSOCIATES_PRIMEFACTS_EQ ring_associates_primefacts_eq
RING_ASSOCIATES_PRODUCT ring_associates_product
RING_ASSOCIATES_PRODUCT_RING ring_associates_product_ring
RING_ASSOCIATES_PROD_RING ring_associates_prod_ring
RING_ASSOCIATES_REFL ring_associates_refl
RING_ASSOCIATES_REGULAR ring_associates_regular
RING_ASSOCIATES_RMUL ring_associates_rmul
RING_ASSOCIATES_SAME_DIVISORS ring_associates_same_divisors
RING_ASSOCIATES_SYM ring_associates_sym
RING_ASSOCIATES_TRANS ring_associates_trans
RING_ASSOCIATES_UNIT ring_associates_unit
RING_ASSOCIATES_ZERODIVISOR ring_associates_zerodivisor
RING_AUTOMORPHISM_EQ ring_automorphism_eq
RING_AUTOMORPHISM_FROBENIUS ring_automorphism_frobenius
RING_AUTOMORPHISM_I ring_automorphism_i
RING_AUTOMORPHISM_ID ring_automorphism_id
RING_AUTOMORPHISM_IMP_ENDOMORPHISM ring_automorphism_imp_endomorphism
RING_BINOMIAL_FRESHMAN ring_binomial_freshman
RING_BINOMIAL_THEOREM ring_binomial_theorem
RING_CARRIER_HAS_SIZE_1 ring_carrier_has_size_1
RING_CARRIER_HAS_SIZE_2 ring_carrier_has_size_2
RING_CARRIER_INTEGER_MOD_RING ring_carrier_integer_mod_ring
RING_CARRIER_NONEMPTY ring_carrier_nonempty
RING_CARRIER_POLY_RING ring_carrier_poly_ring
RING_CARRIER_POLY_RING_FINITE ring_carrier_poly_ring_finite
RING_CARRIER_POLY_SUBRING_GENERATED ring_carrier_poly_subring_generated
RING_CARRIER_POLY_SUBRING_GENERATED_MONO ring_carrier_poly_subring_generated_mono
RING_CARRIER_POLY_SUBRING_GENERATED_SUBSET ring_carrier_poly_subring_generated_subset
RING_CARRIER_POWSER_RING ring_carrier_powser_ring
RING_CARRIER_POWSER_SUBRING_GENERATED ring_carrier_powser_subring_generated
RING_CARRIER_POWSER_SUBRING_GENERATED_MONO ring_carrier_powser_subring_generated_mono
RING_CARRIER_POWSER_SUBRING_GENERATED_SUBSET ring_carrier_powser_subring_generated_subset
RING_CARRIER_RULE ring_carrier_rule
RING_CARRIER_SUBRING_GENERATED_0 ring_carrier_subring_generated_0
RING_CARRIER_SUBRING_GENERATED_MONO ring_carrier_subring_generated_mono
RING_CARRIER_SUBRING_GENERATED_SUBSET ring_carrier_subring_generated_subset
RING_CARRIER_TAC ring_carrier_tac
RING_CHAR_DIVIDES_MUL ring_char_divides_mul
RING_CHAR_DIVIDES_ORDER ring_char_divides_order
RING_CHAR_DIVIDES_PRIME ring_char_divides_prime
RING_CHAR_EQ_0 ring_char_eq_0
RING_CHAR_EQ_1 ring_char_eq_1
RING_CHAR_FINITE ring_char_finite
RING_CHAR_HOMOMORPHIC_IMAGE ring_char_homomorphic_image
RING_CHAR_INFINITE ring_char_infinite
RING_CHAR_MONOMORPHIC_IMAGE ring_char_monomorphic_image
RING_CHAR_SUBRING_GENERATED ring_char_subring_generated
RING_CHAR_UNIQUE ring_char_unique
RING_CLAUSES ring_clauses
RING_COMAXIMAL ring_comaximal
RING_COPRIME_0 ring_coprime_0
RING_COPRIME_00 ring_coprime_00
RING_COPRIME_DISTINCT_MONIC_IRREDUCIBLES ring_coprime_distinct_monic_irreducibles
RING_COPRIME_DIVISORS ring_coprime_divisors
RING_COPRIME_DIVPROD_LEFT ring_coprime_divprod_left
RING_COPRIME_DIVPROD_RIGHT ring_coprime_divprod_right
RING_COPRIME_HOMOMORPHIC_IMAGE ring_coprime_homomorphic_image
RING_COPRIME_IN_CARRIER ring_coprime_in_carrier
RING_COPRIME_LMUL ring_coprime_lmul
RING_COPRIME_LPOW ring_coprime_lpow
RING_COPRIME_PRODUCT ring_coprime_product
RING_COPRIME_PRODUCT_DIVIDES ring_coprime_product_divides
RING_COPRIME_PRODUCT_DIVIDES_ALT ring_coprime_product_divides_alt
RING_COPRIME_PRODUCT_EQ ring_coprime_product_eq
RING_COPRIME_REFL ring_coprime_refl
RING_COPRIME_RMUL ring_coprime_rmul
RING_COPRIME_RPOW ring_coprime_rpow
RING_COPRIME_SYM ring_coprime_sym
RING_COPRIME_UNIT ring_coprime_unit
RING_COSET ring_coset_v1
RING_COSETS_EQ ring_cosets_eq
RING_COSET_0 ring_coset_0
RING_COSET_CARRIER ring_coset_carrier
RING_COSET_EQ ring_coset_eq
RING_COSET_EQ_EMPTY ring_coset_eq_empty
RING_COSET_EQ_IDEAL ring_coset_eq_ideal
RING_COSET_IDEAL_GENERATED_SING ring_coset_ideal_generated_sing
RING_COSET_IDEAL_GENERATED_SING_EQ ring_coset_ideal_generated_sing_eq
RING_COSET_NONEMPTY ring_coset_nonempty
RING_COSET_PRODUCT_RING ring_coset_product_ring
RING_COSET_PROD_RING ring_coset_prod_ring
RING_COSET_RELATIONAL ring_coset_relational
RING_COSET_SETADD ring_coset_setadd
RING_COSET_TRIVIAL ring_coset_trivial
RING_DIRECT_LIMIT ring_direct_limit
RING_DIV ring_div_v1
RING_DIVIDES_0 ring_divides_0
RING_DIVIDES_1 ring_divides_1
RING_DIVIDES_ADD ring_divides_add
RING_DIVIDES_ALT ring_divides_alt
RING_DIVIDES_ANTISYM ring_divides_antisym
RING_DIVIDES_ASSOCIATES ring_divides_associates
RING_DIVIDES_GCD ring_divides_gcd
RING_DIVIDES_GCD_EQ ring_divides_gcd_eq
RING_DIVIDES_HOMOMORPHIC_IMAGE ring_divides_homomorphic_image
RING_DIVIDES_IN_CARRIER ring_divides_in_carrier
RING_DIVIDES_ISOMORPHIC_IMAGE_EQ ring_divides_isomorphic_image_eq
RING_DIVIDES_LMUL ring_divides_lmul
RING_DIVIDES_LMUL2 ring_divides_lmul2
RING_DIVIDES_LMUL_REV ring_divides_lmul_rev
RING_DIVIDES_LNEG ring_divides_lneg
RING_DIVIDES_LOCALEQUIV ring_divides_localequiv
RING_DIVIDES_MORE_DIVISORS ring_divides_more_divisors
RING_DIVIDES_MUL ring_divides_mul
RING_DIVIDES_MUL2 ring_divides_mul2
RING_DIVIDES_MUL_EQ ring_divides_mul_eq
RING_DIVIDES_NEG ring_divides_neg
RING_DIVIDES_NEG_EQ ring_divides_neg_eq
RING_DIVIDES_ONE ring_divides_one
RING_DIVIDES_PRIMEFACTS_INJECTION ring_divides_primefacts_injection
RING_DIVIDES_PRIMEFACTS_INJECTION_EQ ring_divides_primefacts_injection_eq
RING_DIVIDES_PRIMEFACTS_LE ring_divides_primefacts_le
RING_DIVIDES_PRIMEFACTS_LT ring_divides_primefacts_lt
RING_DIVIDES_PRODUCTS ring_divides_products
RING_DIVIDES_PRODUCT_RING ring_divides_product_ring
RING_DIVIDES_PRODUCT_SUBSET ring_divides_product_subset
RING_DIVIDES_PROD_RING ring_divides_prod_ring
RING_DIVIDES_REFL ring_divides_refl
RING_DIVIDES_RMUL ring_divides_rmul
RING_DIVIDES_RMUL2 ring_divides_rmul2
RING_DIVIDES_RMUL_REV ring_divides_rmul_rev
RING_DIVIDES_SUB ring_divides_sub
RING_DIVIDES_SUB_POW ring_divides_sub_pow
RING_DIVIDES_TRANS ring_divides_trans
RING_DIVIDES_UNIT ring_divides_unit
RING_DIVIDES_WF ring_divides_wf
RING_DIVIDES_ZERO ring_divides_zero
RING_DIV_1 ring_div_1
RING_ENDOMORPHISM_EQ ring_endomorphism_eq
RING_ENDOMORPHISM_FROBENIUS ring_endomorphism_frobenius
RING_EPIMORPHISM ring_epimorphism_v1
RING_EPIMORPHISM_ALT ring_epimorphism_alt
RING_EPIMORPHISM_BETWEEN_SUBRINGS ring_epimorphism_between_subrings
RING_EPIMORPHISM_COMPOSE ring_epimorphism_compose
RING_EPIMORPHISM_COMPOSE_REV ring_epimorphism_compose_rev
RING_EPIMORPHISM_EQ ring_epimorphism_eq
RING_EPIMORPHISM_FROM_TRIVIAL_RING ring_epimorphism_from_trivial_ring
RING_EPIMORPHISM_FST ring_epimorphism_fst
RING_EPIMORPHISM_I ring_epimorphism_i
RING_EPIMORPHISM_ID ring_epimorphism_id
RING_EPIMORPHISM_IDEAL_CORRESPONDENCE ring_epimorphism_ideal_correspondence
RING_EPIMORPHISM_IDEAL_CORRESPONDENCE_ALT ring_epimorphism_ideal_correspondence_alt
RING_EPIMORPHISM_IMP_HOMOMORPHISM ring_epimorphism_imp_homomorphism
RING_EPIMORPHISM_ISOMORPHISM_COMPOSE_REV ring_epimorphism_isomorphism_compose_rev
RING_EPIMORPHISM_OF_FST ring_epimorphism_of_fst
RING_EPIMORPHISM_OF_SND ring_epimorphism_of_snd
RING_EPIMORPHISM_ONTO_FIELD_EXISTS ring_epimorphism_onto_field_exists
RING_EPIMORPHISM_POLY_EVAL ring_epimorphism_poly_eval
RING_EPIMORPHISM_POLY_EVALUATE ring_epimorphism_poly_evaluate
RING_EPIMORPHISM_POLY_RINGS ring_epimorphism_poly_rings
RING_EPIMORPHISM_POWSER_EVALUATE_AT_0 ring_epimorphism_powser_evaluate_at_0
RING_EPIMORPHISM_POWSER_EVAL_AT_0 ring_epimorphism_powser_eval_at_0
RING_EPIMORPHISM_POWSER_RINGS ring_epimorphism_powser_rings
RING_EPIMORPHISM_PRODUCT_PROJECTION ring_epimorphism_product_projection
RING_EPIMORPHISM_RIGHT_INVERTIBLE ring_epimorphism_right_invertible
RING_EPIMORPHISM_RING_COSET ring_epimorphism_ring_coset
RING_EPIMORPHISM_SND ring_epimorphism_snd
RING_EPIMORPHISM_SUBRING_CORRESPONDENCE ring_epimorphism_subring_correspondence
RING_EPIMORPHISM_SUBRING_CORRESPONDENCE_ALT ring_epimorphism_subring_correspondence_alt
RING_EPIMORPHISM_TO_TRIVIAL_RING ring_epimorphism_to_trivial_ring
RING_EQ_SUB_LADD ring_eq_sub_ladd
RING_EQ_SUB_RADD ring_eq_sub_radd
RING_FRACTIONATE_EQ_0 ring_fractionate_eq_0
RING_FRACTIONATE_EQ_0_GEN ring_fractionate_eq_0_gen
RING_FRACTIONATE_IN_CARRIER ring_fractionate_in_carrier
RING_GCD ring_gcd_v1
RING_GCD_00 ring_gcd_00
RING_GCD_DIVIDES ring_gcd_divides
RING_GCD_EQ ring_gcd_eq
RING_GCD_EQ_1 ring_gcd_eq_1
RING_GCD_LMUL ring_gcd_lmul
RING_GCD_REFL ring_gcd_refl
RING_GCD_RMUL ring_gcd_rmul
RING_GCD_SYM ring_gcd_sym
RING_GCD_UNIQUE ring_gcd_unique
RING_GCD_WORKS ring_gcd_works
RING_GEOM_SERIES ring_geom_series
RING_GEOM_SERIES_GEN ring_geom_series_gen
RING_HOMOMORPHISM ring_homomorphism_v1
RING_HOMOMORPHISMS_EQ_FROM_POLY_RING ring_homomorphisms_eq_from_poly_ring
RING_HOMOMORPHISMS_EQ_FROM_SUBRING_GENERATED ring_homomorphisms_eq_from_subring_generated
RING_HOMOMORPHISM_0 ring_homomorphism_0
RING_HOMOMORPHISM_1 ring_homomorphism_1
RING_HOMOMORPHISM_ADD ring_homomorphism_add
RING_HOMOMORPHISM_BETWEEN_SUBRINGS ring_homomorphism_between_subrings
RING_HOMOMORPHISM_BETWEEN_SUBRINGS_ALT ring_homomorphism_between_subrings_alt
RING_HOMOMORPHISM_COMPONENTWISE ring_homomorphism_componentwise
RING_HOMOMORPHISM_COMPONENTWISE_UNIV ring_homomorphism_componentwise_univ
RING_HOMOMORPHISM_COMPOSE ring_homomorphism_compose
RING_HOMOMORPHISM_DIAG ring_homomorphism_diag
RING_HOMOMORPHISM_DIAGONAL ring_homomorphism_diagonal
RING_HOMOMORPHISM_DIAGONAL_UNIV ring_homomorphism_diagonal_univ
RING_HOMOMORPHISM_EPIMORPHISM_FACTOR ring_homomorphism_epimorphism_factor
RING_HOMOMORPHISM_EQ ring_homomorphism_eq
RING_HOMOMORPHISM_FRACTIONATE ring_homomorphism_fractionate
RING_HOMOMORPHISM_FROM_INTEGER_MOD_RING ring_homomorphism_from_integer_mod_ring
RING_HOMOMORPHISM_FROM_SUBRING_GENERATED ring_homomorphism_from_subring_generated
RING_HOMOMORPHISM_FROM_TRIVIAL_RING ring_homomorphism_from_trivial_ring
RING_HOMOMORPHISM_FST ring_homomorphism_fst
RING_HOMOMORPHISM_I ring_homomorphism_i
RING_HOMOMORPHISM_ID ring_homomorphism_id
RING_HOMOMORPHISM_IMAGE_PREIMAGE ring_homomorphism_image_preimage
RING_HOMOMORPHISM_IMAGE_PREIMAGE_EQ ring_homomorphism_image_preimage_eq
RING_HOMOMORPHISM_INCLUSION ring_homomorphism_inclusion
RING_HOMOMORPHISM_INTEGER_MOD_RINGS ring_homomorphism_integer_mod_rings
RING_HOMOMORPHISM_INTEGER_MOD_RINGS_POW ring_homomorphism_integer_mod_rings_pow
RING_HOMOMORPHISM_INTEGER_MOD_RING_OF_INT ring_homomorphism_integer_mod_ring_of_int
RING_HOMOMORPHISM_INTEGER_RING_OF_INT ring_homomorphism_integer_ring_of_int
RING_HOMOMORPHISM_INTO_SUBRING ring_homomorphism_into_subring
RING_HOMOMORPHISM_INTO_SUBRING_EQ ring_homomorphism_into_subring_eq
RING_HOMOMORPHISM_INTO_SUBRING_EQ_GEN ring_homomorphism_into_subring_eq_gen
RING_HOMOMORPHISM_INV ring_homomorphism_inv
RING_HOMOMORPHISM_IN_CARRIER ring_homomorphism_in_carrier
RING_HOMOMORPHISM_MONOMIAL_1 ring_homomorphism_monomial_1
RING_HOMOMORPHISM_MUL ring_homomorphism_mul
RING_HOMOMORPHISM_NEG ring_homomorphism_neg
RING_HOMOMORPHISM_OF_FST ring_homomorphism_of_fst
RING_HOMOMORPHISM_OF_SND ring_homomorphism_of_snd
RING_HOMOMORPHISM_PAIRED ring_homomorphism_paired
RING_HOMOMORPHISM_PAIRED2 ring_homomorphism_paired2
RING_HOMOMORPHISM_PAIRWISE ring_homomorphism_pairwise
RING_HOMOMORPHISM_POLY_CONST ring_homomorphism_poly_const
RING_HOMOMORPHISM_POLY_EVAL ring_homomorphism_poly_eval
RING_HOMOMORPHISM_POLY_EVALUATE ring_homomorphism_poly_evaluate
RING_HOMOMORPHISM_POLY_EXTEND ring_homomorphism_poly_extend
RING_HOMOMORPHISM_POLY_RINGS ring_homomorphism_poly_rings
RING_HOMOMORPHISM_POW ring_homomorphism_pow
RING_HOMOMORPHISM_POWSER_CONST ring_homomorphism_powser_const
RING_HOMOMORPHISM_POWSER_EVALUATE_AT_0 ring_homomorphism_powser_evaluate_at_0
RING_HOMOMORPHISM_POWSER_EVAL_AT_0 ring_homomorphism_powser_eval_at_0
RING_HOMOMORPHISM_POWSER_EXTEND_AT_0 ring_homomorphism_powser_extend_at_0
RING_HOMOMORPHISM_POWSER_RINGS ring_homomorphism_powser_rings
RING_HOMOMORPHISM_PREIMAGE_IMAGE ring_homomorphism_preimage_image
RING_HOMOMORPHISM_PREIMAGE_IMAGE_GEN ring_homomorphism_preimage_image_gen
RING_HOMOMORPHISM_PRODUCT ring_homomorphism_product
RING_HOMOMORPHISM_PRODUCT_PROJECTION ring_homomorphism_product_projection
RING_HOMOMORPHISM_PROD_INTEGER_MOD_RING ring_homomorphism_prod_integer_mod_ring
RING_HOMOMORPHISM_RING_COSET ring_homomorphism_ring_coset
RING_HOMOMORPHISM_RING_OF_INT ring_homomorphism_ring_of_int
RING_HOMOMORPHISM_RING_OF_NUM ring_homomorphism_ring_of_num
RING_HOMOMORPHISM_SND ring_homomorphism_snd
RING_HOMOMORPHISM_SUB ring_homomorphism_sub
RING_HOMOMORPHISM_SUM ring_homomorphism_sum
RING_IDEAL ring_ideal_v1
RING_IDEAL_0 ring_ideal_0
RING_IDEAL_CARRIER ring_ideal_carrier
RING_IDEAL_CARTESIAN_PRODUCT ring_ideal_cartesian_product
RING_IDEAL_CROSS ring_ideal_cross
RING_IDEAL_EPIMORPHIC_IMAGE ring_ideal_epimorphic_image
RING_IDEAL_EQ_CARRIER ring_ideal_eq_carrier
RING_IDEAL_EQ_CARRIER_UNIT ring_ideal_eq_carrier_unit
RING_IDEAL_HOMOMORPHIC_PREIMAGE ring_ideal_homomorphic_preimage
RING_IDEAL_IDEAL_GENERATED ring_ideal_ideal_generated
RING_IDEAL_IMP_NONEMPTY ring_ideal_imp_nonempty
RING_IDEAL_IMP_SUBSET ring_ideal_imp_subset
RING_IDEAL_INTER ring_ideal_inter
RING_IDEAL_INTERS ring_ideal_inters
RING_IDEAL_INTER_SUBRING ring_ideal_inter_subring
RING_IDEAL_ISOMORPHIC_IMAGE_EQ ring_ideal_isomorphic_image_eq
RING_IDEAL_LOCALIZATION ring_ideal_localization
RING_IDEAL_NONUNITS ring_ideal_nonunits
RING_IDEAL_PRODUCT_RING ring_ideal_product_ring
RING_IDEAL_PROD_RING ring_ideal_prod_ring
RING_IDEAL_QUOTIENT ring_ideal_quotient
RING_IDEAL_QUOTIENT_LMUL ring_ideal_quotient_lmul
RING_IDEAL_QUOTIENT_RMUL ring_ideal_quotient_rmul
RING_IDEAL_RADICAL ring_ideal_radical
RING_IDEAL_RING_KERNEL ring_ideal_ring_kernel
RING_IDEAL_SCALE ring_ideal_scale
RING_IDEAL_SETADD ring_ideal_setadd
RING_IDEAL_SETWISE ring_ideal_setwise
RING_IDEAL_SUBRING_GENERATED ring_ideal_subring_generated
RING_IDEAL_SUBRING_GENERATED_EQ ring_ideal_subring_generated_eq
RING_IDEAL_UNIONS ring_ideal_unions
RING_IMAGE_FROM_SUBRING_GENERATED ring_image_from_subring_generated
RING_IMAGE_FROM_TRIVIAL_RING ring_image_from_trivial_ring
RING_IMAGE_TO_SUBRING_GENERATED ring_image_to_subring_generated
RING_IMAGE_TO_TRIVIAL_RING ring_image_to_trivial_ring
RING_IMP_GCD_EXISTS ring_imp_gcd_exists
RING_INTEGRAL_DOMAIN_UNIVERSAL ring_integral_domain_universal
RING_INV ring_inv_v1
RING_INV_0 ring_inv_0
RING_INV_1 ring_inv_1
RING_INV_INTEGER_MOD_RING ring_inv_integer_mod_ring
RING_INV_INV ring_inv_inv
RING_INV_MUL ring_inv_mul
RING_INV_POW ring_inv_pow
RING_INV_ZERO ring_inv_zero
RING_IRREDUCIBLES_COPRIME_OR_ASSOCIATES ring_irreducibles_coprime_or_associates
RING_IRREDUCIBLE_COPRIME_EQ ring_irreducible_coprime_eq
RING_IRREDUCIBLE_DIVIDES_OR_COPRIME ring_irreducible_divides_or_coprime
RING_IRREDUCIBLE_EQ_MAXIMAL_IDEAL ring_irreducible_eq_maximal_ideal
RING_IRREDUCIBLE_EQ_MAXIMAL_PRINCIPAL_IDEAL ring_irreducible_eq_maximal_principal_ideal
RING_IRREDUCIBLE_IMP_MAXIMAL_PRINCIPAL_IDEAL ring_irreducible_imp_maximal_principal_ideal
RING_IRREDUCIBLE_IMP_NONTRIVIAL_RING ring_irreducible_imp_nontrivial_ring
RING_IRREDUCIBLE_IMP_SQUAREFREE ring_irreducible_imp_squarefree
RING_IRREDUCIBLE_IN_CARRIER ring_irreducible_in_carrier
RING_IRREDUCIBLE_ISOMORPHIC_IMAGE_EQ ring_irreducible_isomorphic_image_eq
RING_IRREDUCIBLE_NEG ring_irreducible_neg
RING_IRREDUCIBLE_POLY_CONST ring_irreducible_poly_const
RING_IRREDUCIBLE_POLY_RECIP ring_irreducible_poly_recip
RING_IRREDUCIBLE_POLY_RECIP_EQ ring_irreducible_poly_recip_eq
RING_IRREDUCIBLE_POLY_VAR ring_irreducible_poly_var
RING_ISOMORPHISM ring_isomorphism_v1
RING_ISOMORPHISMS ring_isomorphisms_v1
RING_ISOMORPHISMS_BETWEEN_SUBRINGS ring_isomorphisms_between_subrings
RING_ISOMORPHISMS_BETWEEN_SUBRINGS_ALT ring_isomorphisms_between_subrings_alt
RING_ISOMORPHISMS_COMPOSE ring_isomorphisms_compose
RING_ISOMORPHISMS_EQ ring_isomorphisms_eq
RING_ISOMORPHISMS_I ring_isomorphisms_i
RING_ISOMORPHISMS_ID ring_isomorphisms_id
RING_ISOMORPHISMS_IMP_ISOMORPHISM ring_isomorphisms_imp_isomorphism
RING_ISOMORPHISMS_IMP_ISOMORPHISM_ALT ring_isomorphisms_imp_isomorphism_alt
RING_ISOMORPHISMS_ISOMORPHISM ring_isomorphisms_isomorphism
RING_ISOMORPHISMS_PAIRED2 ring_isomorphisms_paired2
RING_ISOMORPHISMS_POLY_POLY_RING ring_isomorphisms_poly_poly_ring
RING_ISOMORPHISMS_POLY_REINDEX ring_isomorphisms_poly_reindex
RING_ISOMORPHISMS_POLY_RINGS ring_isomorphisms_poly_rings
RING_ISOMORPHISMS_POLY_SUBRING_GENERATED ring_isomorphisms_poly_subring_generated
RING_ISOMORPHISMS_POWSER_POWSER_RING ring_isomorphisms_powser_powser_ring
RING_ISOMORPHISMS_POWSER_REINDEX ring_isomorphisms_powser_reindex
RING_ISOMORPHISMS_POWSER_RINGS ring_isomorphisms_powser_rings
RING_ISOMORPHISMS_POWSER_SUBRING_GENERATED ring_isomorphisms_powser_subring_generated
RING_ISOMORPHISMS_PRODUCT_RING_DISJOINT_UNION ring_isomorphisms_product_ring_disjoint_union
RING_ISOMORPHISMS_PROD_RING_SWAP ring_isomorphisms_prod_ring_swap
RING_ISOMORPHISMS_SYM ring_isomorphisms_sym
RING_ISOMORPHISM_ALT ring_isomorphism_alt
RING_ISOMORPHISM_BETWEEN_SUBRINGS ring_isomorphism_between_subrings
RING_ISOMORPHISM_COMPOSE ring_isomorphism_compose
RING_ISOMORPHISM_COMPOSE_REV ring_isomorphism_compose_rev
RING_ISOMORPHISM_EPIMORPHISM ring_isomorphism_epimorphism
RING_ISOMORPHISM_EQ ring_isomorphism_eq
RING_ISOMORPHISM_EQ_EPIMORPHISM_FINITE ring_isomorphism_eq_epimorphism_finite
RING_ISOMORPHISM_EQ_MONOMORPHISM_FINITE ring_isomorphism_eq_monomorphism_finite
RING_ISOMORPHISM_FRACTIONATE_GEN ring_isomorphism_fractionate_gen
RING_ISOMORPHISM_FST ring_isomorphism_fst
RING_ISOMORPHISM_I ring_isomorphism_i
RING_ISOMORPHISM_ID ring_isomorphism_id
RING_ISOMORPHISM_IMP_EPIMORPHISM ring_isomorphism_imp_epimorphism
RING_ISOMORPHISM_IMP_HOMOMORPHISM ring_isomorphism_imp_homomorphism
RING_ISOMORPHISM_IMP_ISOMORPHIC ring_isomorphism_imp_isomorphic
RING_ISOMORPHISM_IMP_MONOMORPHISM ring_isomorphism_imp_monomorphism
RING_ISOMORPHISM_INVERSE ring_isomorphism_inverse
RING_ISOMORPHISM_MONOMORPHISM ring_isomorphism_monomorphism
RING_ISOMORPHISM_MONOMORPHISM_ALT ring_isomorphism_monomorphism_alt
RING_ISOMORPHISM_ONTO_IMAGE ring_isomorphism_onto_image
RING_ISOMORPHISM_PAIRED2 ring_isomorphism_paired2
RING_ISOMORPHISM_POLY_REINDEX ring_isomorphism_poly_reindex
RING_ISOMORPHISM_POLY_RINGS ring_isomorphism_poly_rings
RING_ISOMORPHISM_POLY_RING_TRIVIAL ring_isomorphism_poly_ring_trivial
RING_ISOMORPHISM_POWSER_REINDEX ring_isomorphism_powser_reindex
RING_ISOMORPHISM_POWSER_RINGS ring_isomorphism_powser_rings
RING_ISOMORPHISM_POWSER_RING_TRIVIAL ring_isomorphism_powser_ring_trivial
RING_ISOMORPHISM_PRIME_SUBRING ring_isomorphism_prime_subring
RING_ISOMORPHISM_PRODUCT_PROJECTION ring_isomorphism_product_projection
RING_ISOMORPHISM_PRODUCT_RING_DISJOINT_UNION ring_isomorphism_product_ring_disjoint_union
RING_ISOMORPHISM_PROD_INTEGER_MOD_RING ring_isomorphism_prod_integer_mod_ring
RING_ISOMORPHISM_RING_KERNEL_RING_IMAGE ring_isomorphism_ring_kernel_ring_image
RING_ISOMORPHISM_SND ring_isomorphism_snd
RING_ISOMORPHISM_SUBSET ring_isomorphism_subset
RING_KERNEL_0 ring_kernel_0
RING_KERNEL_FROM_SUBRING_GENERATED ring_kernel_from_subring_generated
RING_KERNEL_FROM_TRIVIAL_RING ring_kernel_from_trivial_ring
RING_KERNEL_NONEMPTY ring_kernel_nonempty
RING_KERNEL_RING_COSET ring_kernel_ring_coset
RING_KERNEL_SUBSET_CARRIER ring_kernel_subset_carrier
RING_KERNEL_TO_SUBRING_GENERATED ring_kernel_to_subring_generated
RING_KERNEL_TO_TRIVIAL_RING ring_kernel_to_trivial_ring
RING_LINV_UNIQUE ring_linv_unique
RING_LNEG_UNIQUE ring_lneg_unique
RING_LOCALEQUIV ring_localequiv_v1
RING_LOCALEQUIV_ADD ring_localequiv_add
RING_LOCALEQUIV_EQUIV ring_localequiv_equiv
RING_LOCALEQUIV_EQ_0 ring_localequiv_eq_0
RING_LOCALEQUIV_EQ_0_GEN ring_localequiv_eq_0_gen
RING_LOCALEQUIV_IN_CARRIER ring_localequiv_in_carrier
RING_LOCALEQUIV_IN_LOCALIZED_IDEAL ring_localequiv_in_localized_ideal
RING_LOCALEQUIV_MUL ring_localequiv_mul
RING_LOCALEQUIV_NEG ring_localequiv_neg
RING_LOCALEQUIV_REFL ring_localequiv_refl
RING_LOCALEQUIV_SPLIT ring_localequiv_split
RING_LOCALEQUIV_SPLIT_EXPLICIT ring_localequiv_split_explicit
RING_LOCALEQUIV_SYM ring_localequiv_sym
RING_LOCALEQUIV_TRANS ring_localequiv_trans
RING_LOCALIZATION ring_localization_v1
RING_LOCALIZATION_0 ring_localization_0
RING_LOCALIZATION_1 ring_localization_1
RING_LOCALIZATION_ADD ring_localization_add
RING_LOCALIZATION_CARRIER ring_localization_carrier
RING_LOCALIZATION_HOMOMORPHISM_UNIQUE ring_localization_homomorphism_unique
RING_LOCALIZATION_MUL ring_localization_mul
RING_LOCALIZATION_NEG ring_localization_neg
RING_LOCALIZATION_PRIME_IDEAL_CORRESPONDENCE ring_localization_prime_ideal_correspondence
RING_LOCALIZATION_UNCHANGED ring_localization_unchanged
RING_LOCALIZATION_UNIQUE ring_localization_unique
RING_LOCALIZATION_UNIVERSAL ring_localization_universal
RING_LZERO_UNIQUE ring_lzero_unique
RING_MONOMORPHIC_IMAGE_RULE ring_monomorphic_image_rule
RING_MONOMORPHISM ring_monomorphism_v1
RING_MONOMORPHISM_ALT ring_monomorphism_alt
RING_MONOMORPHISM_ALT_EQ ring_monomorphism_alt_eq
RING_MONOMORPHISM_BETWEEN_SUBRINGS ring_monomorphism_between_subrings
RING_MONOMORPHISM_COMPOSE ring_monomorphism_compose
RING_MONOMORPHISM_COMPOSE_REV ring_monomorphism_compose_rev
RING_MONOMORPHISM_DIAG ring_monomorphism_diag
RING_MONOMORPHISM_DIAGONAL ring_monomorphism_diagonal
RING_MONOMORPHISM_DIAGONAL_UNIV ring_monomorphism_diagonal_univ
RING_MONOMORPHISM_EPIMORPHISM ring_monomorphism_epimorphism
RING_MONOMORPHISM_EQ ring_monomorphism_eq
RING_MONOMORPHISM_EQ_0 ring_monomorphism_eq_0
RING_MONOMORPHISM_FRACTIONATE ring_monomorphism_fractionate
RING_MONOMORPHISM_FRACTIONATE_GEN ring_monomorphism_fractionate_gen
RING_MONOMORPHISM_FROBENIUS ring_monomorphism_frobenius
RING_MONOMORPHISM_FROBENIUS_GEN ring_monomorphism_frobenius_gen
RING_MONOMORPHISM_FROM_INTEGER_MOD_RING ring_monomorphism_from_integer_mod_ring
RING_MONOMORPHISM_FROM_SUBRING_GENERATED ring_monomorphism_from_subring_generated
RING_MONOMORPHISM_FROM_TRIVIAL_RING ring_monomorphism_from_trivial_ring
RING_MONOMORPHISM_I ring_monomorphism_i
RING_MONOMORPHISM_ID ring_monomorphism_id
RING_MONOMORPHISM_IMP_HOMOMORPHISM ring_monomorphism_imp_homomorphism
RING_MONOMORPHISM_INCLUSION ring_monomorphism_inclusion
RING_MONOMORPHISM_INJECTIVE_EQ ring_monomorphism_injective_eq
RING_MONOMORPHISM_INTEGER_MOD_RING_OF_INT ring_monomorphism_integer_mod_ring_of_int
RING_MONOMORPHISM_INTEGER_RING_OF_INT ring_monomorphism_integer_ring_of_int
RING_MONOMORPHISM_INTO_SUBRING ring_monomorphism_into_subring
RING_MONOMORPHISM_INTO_SUPERRING ring_monomorphism_into_superring
RING_MONOMORPHISM_ISOMORPHISM_COMPOSE_REV ring_monomorphism_isomorphism_compose_rev
RING_MONOMORPHISM_LEFT_INVERTIBLE ring_monomorphism_left_invertible
RING_MONOMORPHISM_POLY_CONST ring_monomorphism_poly_const
RING_MONOMORPHISM_POLY_POWSER ring_monomorphism_poly_powser
RING_MONOMORPHISM_POLY_RINGS ring_monomorphism_poly_rings
RING_MONOMORPHISM_POWSER_CONST ring_monomorphism_powser_const
RING_MONOMORPHISM_POWSER_RINGS ring_monomorphism_powser_rings
RING_MONOMORPHISM_PRODUCT ring_monomorphism_product
RING_MONOMORPHISM_PRODUCT_GEN ring_monomorphism_product_gen
RING_MONOMORPHISM_SUM ring_monomorphism_sum
RING_MONOMORPHISM_SUM_GEN ring_monomorphism_sum_gen
RING_MONOMORPHISM_TO_TRIVIAL_RING ring_monomorphism_to_trivial_ring
RING_MUL ring_mul_v1
RING_MULTIPLE_IN_IDEAL ring_multiple_in_ideal
RING_MULTSYS ring_multsys_v1
RING_MULTSYS_IDEMPOT ring_multsys_idempot
RING_MULTSYS_IMP_NONEMPTY ring_multsys_imp_nonempty
RING_MULTSYS_IMP_SUBSET ring_multsys_imp_subset
RING_MULTSYS_INTER ring_multsys_inter
RING_MULTSYS_INTERS ring_multsys_inters
RING_MULTSYS_NILPOTENT_EXISTS ring_multsys_nilpotent_exists
RING_MULTSYS_NONPRIME ring_multsys_nonprime
RING_MULTSYS_NONPRIME_EQ ring_multsys_nonprime_eq
RING_MULTSYS_NONZERO ring_multsys_nonzero
RING_MULTSYS_POWERS ring_multsys_powers
RING_MULTSYS_REGULAR ring_multsys_regular
RING_MULTSYS_UNITS ring_multsys_units
RING_MULYSYS_1 ring_mulysys_1
RING_MULYSYS_CARRIER ring_mulysys_carrier
RING_MUL_AC ring_mul_ac
RING_MUL_ASSOC ring_mul_assoc
RING_MUL_IMP_UNITS ring_mul_imp_units
RING_MUL_IN_PRIME_IDEAL ring_mul_in_prime_ideal
RING_MUL_IN_SETMUL ring_mul_in_setmul
RING_MUL_IN_SUBRING_GENERATED ring_mul_in_subring_generated
RING_MUL_LCANCEL ring_mul_lcancel
RING_MUL_LID ring_mul_lid
RING_MUL_LINV ring_mul_linv
RING_MUL_LINV_EQ ring_mul_linv_eq
RING_MUL_LNEG ring_mul_lneg
RING_MUL_LZERO ring_mul_lzero
RING_MUL_POW ring_mul_pow
RING_MUL_RCANCEL ring_mul_rcancel
RING_MUL_RID ring_mul_rid
RING_MUL_RINV ring_mul_rinv
RING_MUL_RINV_EQ ring_mul_rinv_eq
RING_MUL_RNEG ring_mul_rneg
RING_MUL_RZERO ring_mul_rzero
RING_MUL_SYM ring_mul_sym
RING_NEG ring_neg_v1
RING_NEG_0 ring_neg_0
RING_NEG_ADD ring_neg_add
RING_NEG_EQ ring_neg_eq
RING_NEG_EQ_0 ring_neg_eq_0
RING_NEG_EQ_SWAP ring_neg_eq_swap
RING_NEG_IN_SETNEG ring_neg_in_setneg
RING_NEG_IN_SUBRING_GENERATED ring_neg_in_subring_generated
RING_NEG_NEG ring_neg_neg
RING_NEG_SUB ring_neg_sub
RING_NILPOTENT ring_nilpotent_v1
RING_NILPOTENT_0 ring_nilpotent_0
RING_NILPOTENT_1 ring_nilpotent_1
RING_NILPOTENT_ADD ring_nilpotent_add
RING_NILPOTENT_HOMOMORPHIC_IMAGE ring_nilpotent_homomorphic_image
RING_NILPOTENT_IMP_ZERODIVISOR ring_nilpotent_imp_zerodivisor
RING_NILPOTENT_IN_CARRIER ring_nilpotent_in_carrier
RING_NILPOTENT_LMUL ring_nilpotent_lmul
RING_NILPOTENT_MONOMORPHIC_IMAGE_EQ ring_nilpotent_monomorphic_image_eq
RING_NILPOTENT_NEG ring_nilpotent_neg
RING_NILPOTENT_NEG_EQ ring_nilpotent_neg_eq
RING_NILPOTENT_POLY_RING ring_nilpotent_poly_ring
RING_NILPOTENT_POW ring_nilpotent_pow
RING_NILPOTENT_PRODUCT_RING ring_nilpotent_product_ring
RING_NILPOTENT_PRODUCT_RING_GEN ring_nilpotent_product_ring_gen
RING_NILPOTENT_PROD_RING ring_nilpotent_prod_ring
RING_NILPOTENT_RMUL ring_nilpotent_rmul
RING_NILPOTENT_SUB ring_nilpotent_sub
RING_NILPOTENT_SUM ring_nilpotent_sum
RING_NILPOTENT_UNIT ring_nilpotent_unit
RING_NILRADICAL ring_nilradical
RING_NONUNIT_DIVIDES_IRREDUCIBLE ring_nonunit_divides_irreducible
RING_OF_INT ring_of_int_v1
RING_OF_INT_0 ring_of_int_0
RING_OF_INT_1 ring_of_int_1
RING_OF_INT_ADD ring_of_int_add
RING_OF_INT_CASES ring_of_int_cases
RING_OF_INT_CLAUSES ring_of_int_clauses
RING_OF_INT_EQ ring_of_int_eq
RING_OF_INT_EQ_0 ring_of_int_eq_0
RING_OF_INT_MUL ring_of_int_mul
RING_OF_INT_NEG ring_of_int_neg
RING_OF_INT_OF_NUM ring_of_int_of_num
RING_OF_INT_POW ring_of_int_pow
RING_OF_INT_PROD_RING ring_of_int_prod_ring
RING_OF_INT_REM ring_of_int_rem
RING_OF_INT_SUB ring_of_int_sub
RING_OF_INT_SUBRING_GENERATED ring_of_int_subring_generated
RING_OF_NUM ring_of_num_v1
RING_OF_NUM_0 ring_of_num_0
RING_OF_NUM_1 ring_of_num_1
RING_OF_NUM_ADD ring_of_num_add
RING_OF_NUM_CHAR ring_of_num_char
RING_OF_NUM_CLAUSES ring_of_num_clauses
RING_OF_NUM_EQ ring_of_num_eq
RING_OF_NUM_EQ_0 ring_of_num_eq_0
RING_OF_NUM_EXP ring_of_num_exp
RING_OF_NUM_MOD ring_of_num_mod
RING_OF_NUM_MUL ring_of_num_mul
RING_OF_NUM_POLY_RING ring_of_num_poly_ring
RING_OF_NUM_POWSER_RING ring_of_num_powser_ring
RING_OF_NUM_PROD_RING ring_of_num_prod_ring
RING_OF_NUM_SUBRING_GENERATED ring_of_num_subring_generated
RING_ORDER_1 ring_order_1
RING_ORDER_DIVIDES ring_order_divides
RING_ORDER_EQ_0 ring_order_eq_0
RING_ORDER_EQ_1 ring_order_eq_1
RING_ORDER_MUL ring_order_mul
RING_ORDER_MUL_DIVIDES ring_order_mul_divides
RING_ORDER_MUL_DIVIDES_GEN ring_order_mul_divides_gen
RING_ORDER_MUL_DIVIDES_LCM ring_order_mul_divides_lcm
RING_ORDER_POW ring_order_pow
RING_ORDER_POW_DIVIDES ring_order_pow_divides
RING_ORDER_POW_GEN ring_order_pow_gen
RING_ORDER_UNIQUE ring_order_unique
RING_ORDER_UNIQUE_PRIME ring_order_unique_prime
RING_POLYNOMIAL ring_polynomial_v1
RING_POLYNOMIAL_0 ring_polynomial_0
RING_POLYNOMIAL_1 ring_polynomial_1
RING_POLYNOMIAL_ADD ring_polynomial_add
RING_POLYNOMIAL_CARRIER ring_polynomial_carrier
RING_POLYNOMIAL_CARRIER_GEN ring_polynomial_carrier_gen
RING_POLYNOMIAL_COEFF ring_polynomial_coeff
RING_POLYNOMIAL_COEFF_BOUND ring_polynomial_coeff_bound
RING_POLYNOMIAL_COEFF_ZERO_FROM ring_polynomial_coeff_zero_from
RING_POLYNOMIAL_COMPOSE ring_polynomial_compose
RING_POLYNOMIAL_CONST ring_polynomial_const
RING_POLYNOMIAL_DIV ring_polynomial_div
RING_POLYNOMIAL_IMP_POWERSERIES ring_polynomial_imp_powerseries
RING_POLYNOMIAL_MONOMIAL ring_polynomial_monomial
RING_POLYNOMIAL_MUL ring_polynomial_mul
RING_POLYNOMIAL_NEG ring_polynomial_neg
RING_POLYNOMIAL_POLY_DERIV ring_polynomial_poly_deriv
RING_POLYNOMIAL_POW ring_polynomial_pow
RING_POLYNOMIAL_POWERSERIES_COEFF ring_polynomial_powerseries_coeff
RING_POLYNOMIAL_RECIP ring_polynomial_recip
RING_POLYNOMIAL_REM ring_polynomial_rem
RING_POLYNOMIAL_SUB ring_polynomial_sub
RING_POLYNOMIAL_SUBRING_COEFF ring_polynomial_subring_coeff
RING_POLYNOMIAL_VAR ring_polynomial_var
RING_POLY_UNIVERSAL_CONV ring_poly_universal_conv
RING_POW ring_pow_v1
RING_POWERSERIES ring_powerseries_v1
RING_POWERSERIES_0 ring_powerseries_0
RING_POWERSERIES_1 ring_powerseries_1
RING_POWERSERIES_ADD ring_powerseries_add
RING_POWERSERIES_COEFF ring_powerseries_coeff
RING_POWERSERIES_COMPOSE ring_powerseries_compose
RING_POWERSERIES_CONST ring_powerseries_const
RING_POWERSERIES_MONOMIAL ring_powerseries_monomial
RING_POWERSERIES_MUL ring_powerseries_mul
RING_POWERSERIES_NEG ring_powerseries_neg
RING_POWERSERIES_POLY_DERIV ring_powerseries_poly_deriv
RING_POWERSERIES_POW ring_powerseries_pow
RING_POWERSERIES_RECIP ring_powerseries_recip
RING_POWERSERIES_REINDEX ring_powerseries_reindex
RING_POWERSERIES_SUB ring_powerseries_sub
RING_POWERSERIES_VAR ring_powerseries_var
RING_POW_0 ring_pow_0
RING_POW_1 ring_pow_1
RING_POW_2 ring_pow_2
RING_POW_ADD ring_pow_add
RING_POW_COPRIME_EQ_1 ring_pow_coprime_eq_1
RING_POW_EQ_1 ring_pow_eq_1
RING_POW_GCD_EQ_1 ring_pow_gcd_eq_1
RING_POW_IDEMPOTENT ring_pow_idempotent
RING_POW_INV ring_pow_inv
RING_POW_IN_IDEAL ring_pow_in_ideal
RING_POW_IN_MULTSYS ring_pow_in_multsys
RING_POW_IN_PRIME_IDEAL ring_pow_in_prime_ideal
RING_POW_IN_RADICAL ring_pow_in_radical
RING_POW_IN_SUBRING_GENERATED ring_pow_in_subring_generated
RING_POW_MOD_ORDER ring_pow_mod_order
RING_POW_MOD_ORDER_GEN ring_pow_mod_order_gen
RING_POW_MUL ring_pow_mul
RING_POW_NEG ring_pow_neg
RING_POW_ONE ring_pow_one
RING_POW_POW ring_pow_pow
RING_POW_PRODUCT_RING ring_pow_product_ring
RING_POW_PROD_RING ring_pow_prod_ring
RING_POW_RING_ORDER ring_pow_ring_order
RING_POW_SUBRING_GENERATED ring_pow_subring_generated
RING_POW_ZERO ring_pow_zero
RING_PRIME_DIVIDES_IRREDUCIBLE ring_prime_divides_irreducible
RING_PRIME_DIVIDES_MUL ring_prime_divides_mul
RING_PRIME_DIVIDES_POW ring_prime_divides_pow
RING_PRIME_DIVIDES_PRODUCT ring_prime_divides_product
RING_PRIME_IDEAL ring_prime_ideal
RING_PRIME_IMP_NONTRIVIAL_RING ring_prime_imp_nontrivial_ring
RING_PRIME_IMP_SQUAREFREE ring_prime_imp_squarefree
RING_PRIME_IN_CARRIER ring_prime_in_carrier
RING_PRIME_ISOMORPHIC_IMAGE_EQ ring_prime_isomorphic_image_eq
RING_PRIME_MUL_DIVIDES ring_prime_mul_divides
RING_PRIME_MUL_DIVIDES_EQ ring_prime_mul_divides_eq
RING_PRIME_NEG ring_prime_neg
RING_PRIME_POLY_CONST ring_prime_poly_const
RING_PRIME_POLY_RECIP ring_prime_poly_recip
RING_PRIME_POLY_RECIP_EQ ring_prime_poly_recip_eq
RING_PRIME_POLY_RING_MONO ring_prime_poly_ring_mono
RING_PRIME_POLY_VAR ring_prime_poly_var
RING_PRIME_POLY_VAR_UNIVARIATE ring_prime_poly_var_univariate
RING_PRIME_PRODUCT_DIVIDES ring_prime_product_divides
RING_PRINCIPAL_IDEALS_WF ring_principal_ideals_wf
RING_PRODUCT ring_product_v1
RING_PRODUCT_0 ring_product_0
RING_PRODUCT_1 ring_product_1
RING_PRODUCT_CASES ring_product_cases
RING_PRODUCT_CLAUSES ring_product_clauses
RING_PRODUCT_CLAUSES_LEFT ring_product_clauses_left
RING_PRODUCT_CLAUSES_NUMSEG ring_product_clauses_numseg
RING_PRODUCT_CLAUSES_NUMSEG_ALT ring_product_clauses_numseg_alt
RING_PRODUCT_CLOSED ring_product_closed
RING_PRODUCT_CONST ring_product_const
RING_PRODUCT_DELTA ring_product_delta
RING_PRODUCT_EQ ring_product_eq
RING_PRODUCT_EQ_1 ring_product_eq_1
RING_PRODUCT_EQ_GENERAL_INVERSES ring_product_eq_general_inverses
RING_PRODUCT_IMAGE ring_product_image
RING_PRODUCT_IMAGE_GEN ring_product_image_gen
RING_PRODUCT_INCL_EXCL ring_product_incl_excl
RING_PRODUCT_INJECTION ring_product_injection
RING_PRODUCT_LMUL ring_product_lmul
RING_PRODUCT_MUL ring_product_mul
RING_PRODUCT_NSUM ring_product_nsum
RING_PRODUCT_OFFSET ring_product_offset
RING_PRODUCT_REFLECT ring_product_reflect
RING_PRODUCT_RELATED ring_product_related
RING_PRODUCT_RESTRICT ring_product_restrict
RING_PRODUCT_RESTRICT_SET ring_product_restrict_set
RING_PRODUCT_SING ring_product_sing
RING_PRODUCT_SUBRING_GENERATED ring_product_subring_generated
RING_PRODUCT_SUBRING_GENERATED_GEN ring_product_subring_generated_gen
RING_PRODUCT_SUPERSET ring_product_superset
RING_PRODUCT_SUPPORT ring_product_support
RING_PRODUCT_SWAP ring_product_swap
RING_PRODUCT_TRIVIAL ring_product_trivial
RING_PRODUCT_UNION ring_product_union
RING_PROPERTIES ring_properties
RING_PROPER_DIVISOR_INDUCT ring_proper_divisor_induct
RING_PULL_DIV ring_pull_div
RING_PULL_DIV_CONV ring_pull_div_conv
RING_PULL_DIV_TAC ring_pull_div_tac
RING_REGULAR_0 ring_regular_0
RING_REGULAR_1 ring_regular_1
RING_REGULAR_IN_CARRIER ring_regular_in_carrier
RING_REGULAR_ISOMORPHIC_IMAGE_EQ ring_regular_isomorphic_image_eq
RING_REGULAR_MUL ring_regular_mul
RING_REGULAR_MUL_EQ ring_regular_mul_eq
RING_REGULAR_NEG ring_regular_neg
RING_REGULAR_NEG_EQ ring_regular_neg_eq
RING_REGULAR_NILPOTENT_CLAUSES ring_regular_nilpotent_clauses
RING_REGULAR_POW ring_regular_pow
RING_REGULAR_PRODUCT_RING ring_regular_product_ring
RING_REGULAR_PROD_RING ring_regular_prod_ring
RING_RINV_UNIQUE ring_rinv_unique
RING_RNEG_UNIQUE ring_rneg_unique
RING_RULE ring_rule
RING_RZERO_UNIQUE ring_rzero_unique
RING_SATURATED_MULTSYS_NONPRIME ring_saturated_multsys_nonprime
RING_SCALE_SETMUL ring_scale_setmul
RING_SETADD ring_setadd_v1
RING_SETADD_AC ring_setadd_ac
RING_SETADD_ASSOC ring_setadd_assoc
RING_SETADD_COSETS ring_setadd_cosets
RING_SETADD_EQ_EMPTY ring_setadd_eq_empty
RING_SETADD_IDEAL_LEFT ring_setadd_ideal_left
RING_SETADD_IDEAL_RIGHT ring_setadd_ideal_right
RING_SETADD_LCANCEL ring_setadd_lcancel
RING_SETADD_LCANCEL_SET ring_setadd_lcancel_set
RING_SETADD_LDISTRIB ring_setadd_ldistrib
RING_SETADD_LSUBSET ring_setadd_lsubset
RING_SETADD_LSUBSET_EQ ring_setadd_lsubset_eq
RING_SETADD_LZERO ring_setadd_lzero
RING_SETADD_MONO ring_setadd_mono
RING_SETADD_PRODUCT_RING ring_setadd_product_ring
RING_SETADD_PROD_RING ring_setadd_prod_ring
RING_SETADD_RCANCEL ring_setadd_rcancel
RING_SETADD_RCANCEL_SET ring_setadd_rcancel_set
RING_SETADD_RDISTRIB ring_setadd_rdistrib
RING_SETADD_RSUBSET ring_setadd_rsubset
RING_SETADD_RSUBSET_EQ ring_setadd_rsubset_eq
RING_SETADD_RZERO ring_setadd_rzero
RING_SETADD_SING ring_setadd_sing
RING_SETADD_SUBRING ring_setadd_subring
RING_SETADD_SUBRING_GENERATED ring_setadd_subring_generated
RING_SETADD_SUBSET_IDEAL ring_setadd_subset_ideal
RING_SETADD_SUPERSET_LEFT ring_setadd_superset_left
RING_SETADD_SUPERSET_RIGHT ring_setadd_superset_right
RING_SETADD_SYM ring_setadd_sym
RING_SETMUL ring_setmul_v1
RING_SETMUL_AC ring_setmul_ac
RING_SETMUL_ASSOC ring_setmul_assoc
RING_SETMUL_COSETS ring_setmul_cosets
RING_SETMUL_EQ_EMPTY ring_setmul_eq_empty
RING_SETMUL_IDEAL_GENERATED_SING ring_setmul_ideal_generated_sing
RING_SETMUL_IDEAL_LEFT ring_setmul_ideal_left
RING_SETMUL_IDEAL_RIGHT ring_setmul_ideal_right
RING_SETMUL_LID ring_setmul_lid
RING_SETMUL_MONO ring_setmul_mono
RING_SETMUL_RID ring_setmul_rid
RING_SETMUL_SING ring_setmul_sing
RING_SETMUL_SUBRING ring_setmul_subring
RING_SETMUL_SUBSET_IDEAL ring_setmul_subset_ideal
RING_SETMUL_SYM ring_setmul_sym
RING_SETNEG ring_setneg_v1
RING_SETNEG_COSET ring_setneg_coset
RING_SETNEG_EQ_EMPTY ring_setneg_eq_empty
RING_SETNEG_IDEAL ring_setneg_ideal
RING_SETNEG_MONO ring_setneg_mono
RING_SETNEG_SETADD ring_setneg_setadd
RING_SETNEG_SING ring_setneg_sing
RING_SETNEG_SUBRING ring_setneg_subring
RING_SETNEG_SUBRING_GENERATED ring_setneg_subring_generated
RING_SQUAREFREE ring_squarefree_v1
RING_SQUAREFREE_0 ring_squarefree_0
RING_SQUAREFREE_1 ring_squarefree_1
RING_SQUAREFREE_ALT ring_squarefree_alt
RING_SQUAREFREE_ASSOCIATES ring_squarefree_associates
RING_SQUAREFREE_COPRIME ring_squarefree_coprime
RING_SQUAREFREE_COPRIME_DIVISORS ring_squarefree_coprime_divisors
RING_SQUAREFREE_DECOMPOSITION ring_squarefree_decomposition
RING_SQUAREFREE_DIVIDES ring_squarefree_divides
RING_SQUAREFREE_DIVIDES_SQUARE ring_squarefree_divides_square
RING_SQUAREFREE_DIVISOR ring_squarefree_divisor
RING_SQUAREFREE_DIVPOW ring_squarefree_divpow
RING_SQUAREFREE_DIVPOW_EQ ring_squarefree_divpow_eq
RING_SQUAREFREE_GCD ring_squarefree_gcd
RING_SQUAREFREE_IMP_NONZERO ring_squarefree_imp_nonzero
RING_SQUAREFREE_IMP_NO_PRIME_SQUARE ring_squarefree_imp_no_prime_square
RING_SQUAREFREE_IN_CARRIER ring_squarefree_in_carrier
RING_SQUAREFREE_MUL_EQ ring_squarefree_mul_eq
RING_SQUAREFREE_MUL_IMP ring_squarefree_mul_imp
RING_SQUAREFREE_POW ring_squarefree_pow
RING_SQUAREFREE_PRIME_DIVISOR_EQ ring_squarefree_prime_divisor_eq
RING_SQUAREFREE_PRIME_EQ ring_squarefree_prime_eq
RING_SQUAREFREE_PRODUCT ring_squarefree_product
RING_SUB ring_sub_v1
RING_SUBRING_INTER_IDEAL ring_subring_inter_ideal
RING_SUB_EQ_0 ring_sub_eq_0
RING_SUB_LDISTRIB ring_sub_ldistrib
RING_SUB_LZERO ring_sub_lzero
RING_SUB_RDISTRIB ring_sub_rdistrib
RING_SUB_REFL ring_sub_refl
RING_SUB_RZERO ring_sub_rzero
RING_SUB_SUBRING_GENERATED ring_sub_subring_generated
RING_SUB_TELESCOPE ring_sub_telescope
RING_SUM ring_sum_v1
RING_SUM_0 ring_sum_0
RING_SUM_ADD ring_sum_add
RING_SUM_CASES ring_sum_cases
RING_SUM_CLAUSES ring_sum_clauses
RING_SUM_CLAUSES_LEFT ring_sum_clauses_left
RING_SUM_CLAUSES_NUMSEG ring_sum_clauses_numseg
RING_SUM_CLAUSES_NUMSEG_ALT ring_sum_clauses_numseg_alt
RING_SUM_CLAUSES_RIGHT ring_sum_clauses_right
RING_SUM_CLOSED ring_sum_closed
RING_SUM_CONST ring_sum_const
RING_SUM_DELETE ring_sum_delete
RING_SUM_DELTA ring_sum_delta
RING_SUM_DIFF ring_sum_diff
RING_SUM_DIFFS ring_sum_diffs
RING_SUM_DIFFS_ALT ring_sum_diffs_alt
RING_SUM_EQ ring_sum_eq
RING_SUM_EQ_0 ring_sum_eq_0
RING_SUM_EQ_GENERAL_INVERSES ring_sum_eq_general_inverses
RING_SUM_IMAGE ring_sum_image
RING_SUM_IMAGE_GEN ring_sum_image_gen
RING_SUM_INCL_EXCL ring_sum_incl_excl
RING_SUM_LMUL ring_sum_lmul
RING_SUM_NEG ring_sum_neg
RING_SUM_OFFSET ring_sum_offset
RING_SUM_PRODUCT_RING ring_sum_product_ring
RING_SUM_REFLECT ring_sum_reflect
RING_SUM_RELATED ring_sum_related
RING_SUM_RESTRICT ring_sum_restrict
RING_SUM_RESTRICT_SET ring_sum_restrict_set
RING_SUM_RMUL ring_sum_rmul
RING_SUM_SING ring_sum_sing
RING_SUM_SUB ring_sum_sub
RING_SUM_SUBRING_GENERATED ring_sum_subring_generated
RING_SUM_SUBRING_GENERATED_GEN ring_sum_subring_generated_gen
RING_SUM_SUM_PRODUCT ring_sum_sum_product
RING_SUM_SUPERSET ring_sum_superset
RING_SUM_SUPPORT ring_sum_support
RING_SUM_SWAP ring_sum_swap
RING_SUM_TRIVIAL ring_sum_trivial
RING_SUM_UNION ring_sum_union
RING_TAC ring_tac
RING_UNIT_0 ring_unit_0
RING_UNIT_1 ring_unit_1
RING_UNIT_DIV ring_unit_div
RING_UNIT_DIVIDES ring_unit_divides
RING_UNIT_DIVIDES_ALL ring_unit_divides_all
RING_UNIT_DIVIDES_ANY ring_unit_divides_any
RING_UNIT_DIVISOR ring_unit_divisor
RING_UNIT_FRACTIONATE ring_unit_fractionate
RING_UNIT_FRACTION_RING ring_unit_fraction_ring
RING_UNIT_GCD ring_unit_gcd
RING_UNIT_HOMOMORPHIC_IMAGE ring_unit_homomorphic_image
RING_UNIT_IDEMPOTENT_EQ_1 ring_unit_idempotent_eq_1
RING_UNIT_IMP_REGULAR ring_unit_imp_regular
RING_UNIT_IMP_SQUAREFREE ring_unit_imp_squarefree
RING_UNIT_INV ring_unit_inv
RING_UNIT_IN_CARRIER ring_unit_in_carrier
RING_UNIT_ISOMORPHIC_IMAGE_EQ ring_unit_isomorphic_image_eq
RING_UNIT_LOCALEQUIV ring_unit_localequiv
RING_UNIT_LOCALEQUIV_EQ ring_unit_localequiv_eq
RING_UNIT_LOCALIZATION ring_unit_localization
RING_UNIT_MUL ring_unit_mul
RING_UNIT_MUL_EQ ring_unit_mul_eq
RING_UNIT_NEG ring_unit_neg
RING_UNIT_NEG_EQ ring_unit_neg_eq
RING_UNIT_NILPOTENT_CLAUSES ring_unit_nilpotent_clauses
RING_UNIT_NILPOTENT_CLAUSES_1 ring_unit_nilpotent_clauses_1
RING_UNIT_NOT_IN_PRIME_IDEAL ring_unit_not_in_prime_ideal
RING_UNIT_POLY_CONST ring_unit_poly_const
RING_UNIT_POLY_DOMAIN ring_unit_poly_domain
RING_UNIT_POLY_RECIP ring_unit_poly_recip
RING_UNIT_POLY_RECIP_EQ ring_unit_poly_recip_eq
RING_UNIT_POLY_RING ring_unit_poly_ring
RING_UNIT_POLY_RING_1 ring_unit_poly_ring_1
RING_UNIT_POLY_VAR ring_unit_poly_var
RING_UNIT_POW ring_unit_pow
RING_UNIT_POWSER_RING ring_unit_powser_ring
RING_UNIT_POW_EQ ring_unit_pow_eq
RING_UNIT_PRODUCT ring_unit_product
RING_ZERODIVISOR_0 ring_zerodivisor_0
RING_ZERODIVISOR_1 ring_zerodivisor_1
RING_ZERODIVISOR_FRACTION_RING ring_zerodivisor_fraction_ring
RING_ZERODIVISOR_IMP_NONUNIT ring_zerodivisor_imp_nonunit
RING_ZERODIVISOR_IN_CARRIER ring_zerodivisor_in_carrier
RING_ZERODIVISOR_ISOMORPHIC_IMAGE_EQ ring_zerodivisor_isomorphic_image_eq
RING_ZERODIVISOR_LMUL ring_zerodivisor_lmul
RING_ZERODIVISOR_MONOMORPHIC_IMAGE ring_zerodivisor_monomorphic_image
RING_ZERODIVISOR_MUL ring_zerodivisor_mul
RING_ZERODIVISOR_NEG ring_zerodivisor_neg
RING_ZERODIVISOR_NEG_EQ ring_zerodivisor_neg_eq
RING_ZERODIVISOR_NILPOTENT_CLAUSES ring_zerodivisor_nilpotent_clauses
RING_ZERODIVISOR_POW ring_zerodivisor_pow
RING_ZERODIVISOR_PRODUCT_RING ring_zerodivisor_product_ring
RING_ZERODIVISOR_PROD_RING ring_zerodivisor_prod_ring
RING_ZERODIVISOR_RMUL ring_zerodivisor_rmul
SECOND_RING_ISOMORPHISM_THEOREM second_ring_isomorphism_theorem
SINGLETON_RING singleton_ring_v1
SUBRINGS_GENERATED_EQ subrings_generated_eq
SUBRING_GENERATED subring_generated_v1
SUBRING_GENERATED_BY_HOMOMORPHIC_IMAGE subring_generated_by_homomorphic_image
SUBRING_GENERATED_BY_SUBRING_GENERATED subring_generated_by_subring_generated
SUBRING_GENERATED_BY_SUBRING_GENERATED_IDEMPOT subring_generated_by_subring_generated_idempot
SUBRING_GENERATED_EQ subring_generated_eq
SUBRING_GENERATED_FINITARY subring_generated_finitary
SUBRING_GENERATED_IDEMPOT subring_generated_idempot
SUBRING_GENERATED_IDEMPOT_GEN subring_generated_idempot_gen
SUBRING_GENERATED_INC subring_generated_inc
SUBRING_GENERATED_INC_GEN subring_generated_inc_gen
SUBRING_GENERATED_INDUCT subring_generated_induct
SUBRING_GENERATED_INDUCT_STRONG subring_generated_induct_strong
SUBRING_GENERATED_INSERT_ZERO subring_generated_insert_zero
SUBRING_GENERATED_MINIMAL subring_generated_minimal
SUBRING_GENERATED_MINIMAL_EQ subring_generated_minimal_eq
SUBRING_GENERATED_MONO subring_generated_mono
SUBRING_GENERATED_PRIME_SUBRING subring_generated_prime_subring
SUBRING_GENERATED_REFL subring_generated_refl
SUBRING_GENERATED_RESTRICT subring_generated_restrict
SUBRING_GENERATED_RING_CARRIER subring_generated_ring_carrier
SUBRING_GENERATED_SUBRING_GENERATED subring_generated_subring_generated
SUBRING_GENERATED_SUBSET_CARRIER subring_generated_subset_carrier
SUBRING_GENERATED_SUBSET_CARRIER_SUBSET subring_generated_subset_carrier_subset
SUBRING_GENERATED_SUPERSET subring_generated_superset
SUBRING_GENERATED_UNION subring_generated_union
SUBRING_GENERATED_UNION_LEFT subring_generated_union_left
SUBRING_GENERATED_UNION_RIGHT subring_generated_union_right
SUBRING_IMP_MONOMORPHIC_PROPERTY subring_imp_monomorphic_property
SUBRING_MONOMORPHISM_EPIMORPHISM subring_monomorphism_epimorphism
SUBRING_OF_EPIMORPHIC_PREIMAGE subring_of_epimorphic_preimage
SUBRING_OF_FIXPOINTS subring_of_fixpoints
SUBRING_OF_HOMOMORPHIC_EQUALITIES subring_of_homomorphic_equalities
SUBRING_OF_HOMOMORPHIC_IMAGE subring_of_homomorphic_image
SUBRING_OF_HOMOMORPHIC_PREIMAGE subring_of_homomorphic_preimage
SUBRING_OF_IMP_NONEMPTY subring_of_imp_nonempty
SUBRING_OF_IMP_SUBSET subring_of_imp_subset
SUBRING_OF_INTER subring_of_inter
SUBRING_OF_INTERS subring_of_inters
SUBRING_OF_SETWISE subring_of_setwise
SUBRING_OF_SUBRING_GENERATED subring_of_subring_generated
SUBRING_OF_SUBRING_GENERATED_EQ subring_of_subring_generated_eq
SUBRING_OF_SUBRING_GENERATED_REV subring_of_subring_generated_rev
SUBRING_OF_SUBRING_GENERATED_SUBRING_EQ subring_of_subring_generated_subring_eq
SUBRING_OF_UNIONS subring_of_unions
SUBRING_POLY_INTO_SUBRING subring_poly_into_subring
SUBRING_POWSER_INTO_SUBRING subring_powser_into_subring
SUBRING_RING_IMAGE subring_ring_image
SUBRING_SETADD_LEFT subring_setadd_left
SUBRING_SETADD_RIGHT subring_setadd_right
SUBRING_SUBRING_GENERATED subring_subring_generated
SUBSET_CARRIER_SUBRING_GENERATED subset_carrier_subring_generated
SUBSET_IDEALS_GENERATED_SING subset_ideals_generated_sing
SUBSET_SUBRING_GENERATED_FINITARY subset_subring_generated_finitary
THIRD_RING_ISOMORPHISM_THEOREM third_ring_isomorphism_theorem
TOSET_MONOMIAL_LE toset_monomial_le
TRIVIAL_FRACTION_RING trivial_fraction_ring
TRIVIAL_IMP_BOOLEAN_RING trivial_imp_boolean_ring
TRIVIAL_IMP_FINITE_RING trivial_imp_finite_ring
TRIVIAL_INTEGER_MOD_RING trivial_integer_mod_ring
TRIVIAL_POLY_RING trivial_poly_ring
TRIVIAL_POWSER_RING trivial_powser_ring
TRIVIAL_PRODUCT_RING trivial_product_ring
TRIVIAL_PROD_RING trivial_prod_ring
TRIVIAL_QUOTIENT_RING trivial_quotient_ring
TRIVIAL_RING trivial_ring_v1
TRIVIAL_RING_10 trivial_ring_10
TRIVIAL_RING_ALT trivial_ring_alt
TRIVIAL_RING_HAS_SIZE_1 trivial_ring_has_size_1
TRIVIAL_RING_HOMOMORPHIC_IMAGE trivial_ring_homomorphic_image
TRIVIAL_RING_IDEAL trivial_ring_ideal
TRIVIAL_RING_LOCALIZATION trivial_ring_localization
TRIVIAL_RING_MONOMORPHIC_IMAGE_EQ trivial_ring_monomorphic_image_eq
TRIVIAL_RING_MONOMORPHIC_PREIMAGE trivial_ring_monomorphic_preimage
TRIVIAL_RING_POLY_0 trivial_ring_poly_0
TRIVIAL_RING_POWSER_0 trivial_ring_powser_0
TRIVIAL_RING_SINGLETON_RING trivial_ring_singleton_ring
TRIVIAL_RING_SUBRING_GENERATED trivial_ring_subring_generated
TRIVIAL_RING_SUBSET trivial_ring_subset
UFD ufd
UFD_COPRIME ufd_coprime
UFD_DIVIDES_GCD ufd_divides_gcd
UFD_DIVIDES_GCD_EQ ufd_divides_gcd_eq
UFD_EQ_ACCP ufd_eq_accp
UFD_EQ_ATOMIC ufd_eq_atomic
UFD_EQ_ATOMIC_NONUNIT ufd_eq_atomic_nonunit
UFD_EQ_PRIMEFACT ufd_eq_primefact
UFD_EQ_PRIMEFACT_NONUNIT ufd_eq_primefact_nonunit
UFD_EQ_UNIQUE_FACTORIZATION ufd_eq_unique_factorization
UFD_IMP_GCD_EXISTS ufd_imp_gcd_exists
UFD_IMP_INTEGRAL_DOMAIN ufd_imp_integral_domain
UFD_INTEGER_RING ufd_integer_ring
UFD_IRREDUCIBLE_EQ_PRIME ufd_irreducible_eq_prime
UFD_LOCALIZATION ufd_localization
UFD_POLY_RING ufd_poly_ring
UFD_PRIME_FACTOR_EXISTS ufd_prime_factor_exists
UFD_PRIME_FACTOR_INDUCT ufd_prime_factor_induct
UNIONS_MAXIMAL_IDEALS unions_maximal_ideals
UNIONS_PRIME_IDEALS unions_prime_ideals
UNIONS_PROPER_IDEALS unions_proper_ideals
UNIONS_RING_COSETS unions_ring_cosets
UNIQUE_PRIME_IDEAL unique_prime_ideal
UNIQUE_PRIME_IDEAL_IMP_LOCAL_RING unique_prime_ideal_imp_local_ring
VNREGULAR_DOMAIN vnregular_domain
VNREGULAR_FRACTION_RING vnregular_fraction_ring
VNREGULAR_IMP_BEZOUT_RING vnregular_imp_bezout_ring
VNREGULAR_IMP_REDUCED_RING vnregular_imp_reduced_ring
VNREGULAR_INTEGER_MOD_RING vnregular_integer_mod_ring
VNREGULAR_PRODUCT_RING vnregular_product_ring
VNREGULAR_PROD_RING vnregular_prod_ring
VNREGULAR_QUOTIENT_RING vnregular_quotient_ring
VNREGULAR_RING vnregular_ring_v1
VNREGULAR_RING_ALT vnregular_ring_alt
VNREGULAR_RING_EPIMORPHIC_IMAGE vnregular_ring_epimorphic_image
VNREGULAR_RING_FINITELY_GENERATED_IDEALS vnregular_ring_finitely_generated_ideals
VNREGULAR_RING_IDEAL_IDEMPOT vnregular_ring_ideal_idempot
VNREGULAR_RING_LOCALIZATION vnregular_ring_localization
VNREGULAR_RING_NILPOTENT vnregular_ring_nilpotent
VNREGULAR_RING_PRINCIPAL_IDEALS vnregular_ring_principal_ideals
VNREGULAR_RING_REGULAR vnregular_ring_regular
WF_COMPATIBLE_MONOMIAL_ORDER wf_compatible_monomial_order
WF_MONOMIAL_LT wf_monomial_lt
WOSET_COMPATIBLE_MONOMIAL_ORDER woset_compatible_monomial_order
WOSET_MONOMIAL_LE woset_monomial_le
WQOSET_COMPATIBLE_MONOMIAL_ORDER wqoset_compatible_monomial_order
bezout_ring bezout_ring
bool_ring bool_ring
boolean_ring boolean_ring
coeff coeff
euclidean_ring euclidean_ring
field field
finitely_generated_ideal finitely_generated_ideal
fraction_ring fraction_ring
ideal_generated ideal_generated
integer_mod_ring integer_mod_ring
integer_ring integer_ring
integral_domain integral_domain
isomorphic_ring isomorphic_ring
local_ring local_ring
maximal_ideal maximal_ideal
monic monic
monomial monomial
monomial_1 monomial_1
monomial_deg monomial_deg
monomial_div monomial_div
monomial_divides monomial_divides
monomial_le monomial_le
monomial_lt monomial_lt
monomial_mul monomial_mul
monomial_restrict monomial_restrict
monomial_var monomial_var
monomial_vars monomial_vars
noetherian_ring noetherian_ring
poly_0 poly_0
poly_1 poly_1
poly_add poly_add
poly_const poly_const
poly_deg poly_deg
poly_deriv poly_deriv
poly_div poly_div
poly_eval poly_eval
poly_evaluate poly_evaluate
poly_extend poly_extend
poly_mul poly_mul
poly_neg poly_neg
poly_pow poly_pow
poly_recip poly_recip
poly_reindex poly_reindex
poly_rem poly_rem
poly_ring poly_ring
poly_sub poly_sub
poly_var poly_var
poly_vars poly_vars
powser_ring powser_ring
prime_ideal prime_ideal
principal_ideal principal_ideal
prod_ring prod_ring
product_ring product_ring
proper_ideal proper_ideal
quotient_ring quotient_ring
radical radical
real_ring real_ring
ring_0 ring_0
ring_1 ring_1
ring_add ring_add
ring_associates ring_associates
ring_automorphism ring_automorphism
ring_carrier ring_carrier
ring_coprime ring_coprime
ring_coset ring_coset
ring_div ring_div
ring_divides ring_divides
ring_endomorphism ring_endomorphism
ring_epimorphism ring_epimorphism
ring_fractionate ring_fractionate
ring_gcd ring_gcd
ring_homomorphism ring_homomorphism
ring_ideal ring_ideal
ring_image ring_image
ring_inv ring_inv
ring_irreducible ring_irreducible
ring_isomorphism ring_isomorphism
ring_isomorphisms ring_isomorphisms
ring_kernel ring_kernel
ring_localequiv ring_localequiv
ring_localization ring_localization
ring_monomorphism ring_monomorphism
ring_mul ring_mul
ring_multsys ring_multsys
ring_neg ring_neg
ring_nilpotent ring_nilpotent
ring_of_int ring_of_int
ring_of_num ring_of_num
ring_polynomial ring_polynomial
ring_pow ring_pow
ring_powerseries ring_powerseries
ring_prime ring_prime
ring_product ring_product
ring_regular ring_regular
ring_ring_cofactors_universal ring_ring_cofactors_universal
ring_setadd ring_setadd
ring_setmul ring_setmul
ring_setneg ring_setneg
ring_squarefree ring_squarefree
ring_sub ring_sub
ring_sum ring_sum
ring_tybij ring_tybij
ring_unit ring_unit
ring_zerodivisor ring_zerodivisor
singleton_ring singleton_ring
subring_generated subring_generated
subring_of subring_of
trivial_ring trivial_ring
vnregular_ring vnregular_ring
