# Generated by tools/translator: qualified upstream name -> MoonBit name.
ALGEBRAICALLY_CLOSED_FIELD_DECOMPOSE algebraically_closed_field_decompose
ALGEBRAICALLY_CLOSED_FIELD_EQ_IRREDUCIBLES algebraically_closed_field_eq_irreducibles
ALGEBRAICALLY_CLOSED_FIELD_EQ_SPLITS algebraically_closed_field_eq_splits
ALGEBRAICALLY_CLOSED_FIELD_EQ_SPLITS_ALT algebraically_closed_field_eq_splits_alt
ALGEBRAICALLY_CLOSED_FIELD_IMP_FIELD algebraically_closed_field_imp_field
ALGEBRAICALLY_CLOSED_FIELD_IMP_INFINITE algebraically_closed_field_imp_infinite
ALGEBRAICALLY_CLOSED_FIELD_ISOMORPHIC_IMAGE algebraically_closed_field_isomorphic_image
ALGEBRAICALLY_CLOSED_FIELD_NO_PROPER_ALGEBRAIC_EXTENSION algebraically_closed_field_no_proper_algebraic_extension
ALGEBRAICALLY_CLOSED_FIELD_SPLITS algebraically_closed_field_splits
ALGEBRAICALLY_DEPENDENT_ALT algebraically_dependent_alt
ALGEBRAICALLY_DEPENDENT_FINITARY algebraically_dependent_finitary
ALGEBRAICALLY_DEPENDENT_FROM_INSERT algebraically_dependent_from_insert
ALGEBRAICALLY_DEPENDENT_IMP_SUBSET algebraically_dependent_imp_subset
ALGEBRAICALLY_DEPENDENT_INSERT algebraically_dependent_insert
ALGEBRAICALLY_DEPENDENT_MONO algebraically_dependent_mono
ALGEBRAICALLY_DEPENDENT_MONOMORPHIC_IMAGE algebraically_dependent_monomorphic_image
ALGEBRAICALLY_DEPENDENT_OVER_ALGEBRAIC_EXTENSION algebraically_dependent_over_algebraic_extension
ALGEBRAICALLY_DEPENDENT_OVER_SUBRING_GENERATED_MONO algebraically_dependent_over_subring_generated_mono
ALGEBRAICALLY_DEPENDENT_SING algebraically_dependent_sing
ALGEBRAICALLY_DEPENDENT_SPAN algebraically_dependent_span
ALGEBRAICALLY_INDEPENDENT_CARD_LE_SPANNING algebraically_independent_card_le_spanning
ALGEBRAICALLY_INDEPENDENT_EMPTY algebraically_independent_empty
ALGEBRAICALLY_INDEPENDENT_IMP_DISJOINT algebraically_independent_imp_disjoint
ALGEBRAICALLY_INDEPENDENT_IMP_SUBSET algebraically_independent_imp_subset
ALGEBRAICALLY_INDEPENDENT_IMP_TRANSCENDENTAL algebraically_independent_imp_transcendental
ALGEBRAICALLY_INDEPENDENT_INSERT algebraically_independent_insert
ALGEBRAICALLY_INDEPENDENT_MONO algebraically_independent_mono
ALGEBRAICALLY_INDEPENDENT_OVER_ALGEBRAIC_EXTENSION algebraically_independent_over_algebraic_extension
ALGEBRAICALLY_INDEPENDENT_OVER_SUBRING_GENERATED_MONO algebraically_independent_over_subring_generated_mono
ALGEBRAICALLY_INDEPENDENT_SING algebraically_independent_sing
ALGEBRAICALLY_INDEPENDENT_SPAN algebraically_independent_span
ALGEBRAICALLY_INDEPENDENT_TRANS algebraically_independent_trans
ALGEBRAICALLY_SPANNING algebraically_spanning_v1
ALGEBRAICALLY_SPANNING_CONTAINS_TRANSCENDENCE_BASIS algebraically_spanning_contains_transcendence_basis
ALGEBRAICALLY_SPANNING_OVER_ALGEBRAIC_EXTENSION algebraically_spanning_over_algebraic_extension
ALGEBRAICALLY_SPANNING_SPAN algebraically_spanning_span
ALGEBRAICALLY_SPANNING_TRANS algebraically_spanning_trans
ALGEBRAIC_CLOSURE_EXISTS algebraic_closure_exists
ALGEBRAIC_CLOSURE_EXISTS_ID algebraic_closure_exists_id
ALGEBRAIC_CLOSURE_EXTEND_HOMOMORPHISM algebraic_closure_extend_homomorphism
ALGEBRAIC_CLOSURE_UNIQUE algebraic_closure_unique
ALGEBRAIC_CLOSURE_UNIQUE_EXPLICIT algebraic_closure_unique_explicit
ALGEBRAIC_EXTENSION algebraic_extension_v1
ALGEBRAIC_EXTENSION_ALT algebraic_extension_alt
ALGEBRAIC_EXTENSION_EQ algebraic_extension_eq
ALGEBRAIC_EXTENSION_ISOMORPHISM algebraic_extension_isomorphism
ALGEBRAIC_EXTENSION_REFL algebraic_extension_refl
ALGEBRAIC_EXTENSION_SUBFIELDS_GENERATED algebraic_extension_subfields_generated
ALGEBRAIC_EXTENSION_SUBFIELD_GENERATED_ALGEBRAIC algebraic_extension_subfield_generated_algebraic
ALGEBRAIC_EXTENSION_SUBRING_GENERATED_ALGEBRAIC algebraic_extension_subring_generated_algebraic
ALGEBRAIC_EXTENSION_TRANS algebraic_extension_trans
ALGEBRAIC_EXTENSION_TRANS_EQ algebraic_extension_trans_eq
ALGEBRAIC_FROM_SUBRING_GENERATED algebraic_from_subring_generated
ALGEBRAIC_IMP_FIELD_EXTENSION algebraic_imp_field_extension
ALGEBRAIC_MATROID algebraic_matroid_v1
ALGEBRAIC_MATROID_BASIS algebraic_matroid_basis
ALGEBRAIC_MATROID_DEPENDENT algebraic_matroid_dependent
ALGEBRAIC_MATROID_INDEPENDENT algebraic_matroid_independent
ALGEBRAIC_MATROID_SPANNING algebraic_matroid_spanning
ALGEBRAIC_OVER algebraic_over_v1
ALGEBRAIC_OVER_0 algebraic_over_0
ALGEBRAIC_OVER_1 algebraic_over_1
ALGEBRAIC_OVER_ADD algebraic_over_add
ALGEBRAIC_OVER_ALGEBRAIC_EXTENSION algebraic_over_algebraic_extension
ALGEBRAIC_OVER_ALT algebraic_over_alt
ALGEBRAIC_OVER_DIV algebraic_over_div
ALGEBRAIC_OVER_EQ algebraic_over_eq
ALGEBRAIC_OVER_EQ_EQ algebraic_over_eq_eq
ALGEBRAIC_OVER_FIELD_EXTENSION algebraic_over_field_extension
ALGEBRAIC_OVER_FROM_MONOMORPHIC_IMAGE algebraic_over_from_monomorphic_image
ALGEBRAIC_OVER_IMAGE algebraic_over_image
ALGEBRAIC_OVER_IMAGE_GEN algebraic_over_image_gen
ALGEBRAIC_OVER_IMAGE_SUBSET algebraic_over_image_subset
ALGEBRAIC_OVER_INV algebraic_over_inv
ALGEBRAIC_OVER_IN_CARRIER algebraic_over_in_carrier
ALGEBRAIC_OVER_ISOMORPHIC_IMAGE algebraic_over_isomorphic_image
ALGEBRAIC_OVER_MONOMORPHIC_IMAGE algebraic_over_monomorphic_image
ALGEBRAIC_OVER_MUL algebraic_over_mul
ALGEBRAIC_OVER_NEG algebraic_over_neg
ALGEBRAIC_OVER_NONMONOMORPHISM algebraic_over_nonmonomorphism
ALGEBRAIC_OVER_POW algebraic_over_pow
ALGEBRAIC_OVER_RANGE algebraic_over_range
ALGEBRAIC_OVER_REFL algebraic_over_refl
ALGEBRAIC_OVER_SUB algebraic_over_sub
ALGEBRAIC_OVER_SUBFIELD_GENERATED algebraic_over_subfield_generated
ALGEBRAIC_OVER_SUBFIELD_GENERATED_ALGEBRAIC algebraic_over_subfield_generated_algebraic
ALGEBRAIC_OVER_SUBFIELD_SUBRING_GENERATED algebraic_over_subfield_subring_generated
ALGEBRAIC_OVER_SUBRING_GENERATED algebraic_over_subring_generated
ALGEBRAIC_OVER_SUBRING_GENERATED_MONO algebraic_over_subring_generated_mono
ALGEBRAIC_OVER_TRANS algebraic_over_trans
ALGEBRAIC_SPAN algebraic_span_v1
ALGEBRAIC_SPAN_EMPTY algebraic_span_empty
ALGEBRAIC_SPAN_EXCHANGE algebraic_span_exchange
ALGEBRAIC_SPAN_FIELD algebraic_span_field
ALGEBRAIC_SPAN_FINITARY algebraic_span_finitary
ALGEBRAIC_SPAN_MONO algebraic_span_mono
ALGEBRAIC_SPAN_MONOMORPHIC_IMAGE algebraic_span_monomorphic_image
ALGEBRAIC_SPAN_OVER_ALGEBRAIC_EXTENSION algebraic_span_over_algebraic_extension
ALGEBRAIC_SPAN_RANGE algebraic_span_range
ALGEBRAIC_SPAN_RESTRICT algebraic_span_restrict
ALGEBRAIC_SPAN_SPAN algebraic_span_span
ALGEBRAIC_SPAN_SUBSET algebraic_span_subset
ALGEBRAIC_SPAN_SUPERSET algebraic_span_superset
CARD_EQ_ALGEBRAIC_EXTENSION card_eq_algebraic_extension
CARD_FINITE_EXTENSION card_finite_extension
CARD_LE_ALGEBRAIC_EXTENSION card_le_algebraic_extension
CARRIER_SUBFIELD_GENERATED_FIELD carrier_subfield_generated_field
CARRIER_SUBFIELD_GENERATED_SUBFIELD carrier_subfield_generated_subfield
CARRIER_SUBFIELD_OF carrier_subfield_of
COPRIME_POLY_NO_COMMON_ROOT coprime_poly_no_common_root
COPRIME_POLY_NO_COMMON_ROOT_I coprime_poly_no_common_root_i
FIELD_ALGEBRAIC_EXTENSION field_algebraic_extension
FIELD_ALGEBRAIC_OVER field_algebraic_over
FIELD_EXTENSION_CARRIER field_extension_carrier
FIELD_EXTENSION_EQ field_extension_eq
FIELD_EXTENSION_FROM_PRIME_SUBRING field_extension_from_prime_subring
FIELD_EXTENSION_FROM_SUBRING_GENERATED field_extension_from_subring_generated
FIELD_EXTENSION_IMP_HOMOMORPHISM field_extension_imp_homomorphism
FIELD_EXTENSION_IMP_MONOMORPHISM field_extension_imp_monomorphism
FIELD_EXTENSION_IMP_SUBSET field_extension_imp_subset
FIELD_EXTENSION_INTO_SUBFIELD_GENERATED field_extension_into_subfield_generated
FIELD_EXTENSION_INTO_SUBRING_GENERATED field_extension_into_subring_generated
FIELD_EXTENSION_ISOMORPHISM field_extension_isomorphism
FIELD_EXTENSION_REFL field_extension_refl
FIELD_EXTENSION_SUBRING_GENERATED field_extension_subring_generated
FIELD_EXTENSION_TOWER_LAW field_extension_tower_law
FIELD_EXTENSION_TRANS field_extension_trans
FIELD_EXTENSION_TRANS_I field_extension_trans_i
FIELD_SIMPLE_ALGEBRAIC_EXTENSION field_simple_algebraic_extension
FIELD_SIMPLE_ALGEBRAIC_EXTENSION_EQ field_simple_algebraic_extension_eq
FIELD_SIMPLE_ALGEBRAIC_EXTENSION_GEN field_simple_algebraic_extension_gen
FIELD_SUBFIELD_GENERATED field_subfield_generated
FIELD_SUBFIELD_GENERATED_ALT field_subfield_generated_alt
FIELD_SUBFIELD_GENERATED_EQ field_subfield_generated_eq
FIELD_SUBFIELD_GENERATED_MONO field_subfield_generated_mono
FIELD_SUBFIELD_GENERATED_UNITS field_subfield_generated_units
FINITELY_GENERATED_ALGEBRAICALLY_INDEPENDENT_IMP_FINITE finitely_generated_algebraically_independent_imp_finite
FINITELY_GENERATED_EXTENSION finitely_generated_extension_v1
FINITELY_GENERATED_EXTENSION_TRANS finitely_generated_extension_trans
FINITELY_GENERATED_EXTENSION_TRANS_EQ finitely_generated_extension_trans_eq
FINITELY_GENERATED_IMP_FIELD_EXTENSION finitely_generated_imp_field_extension
FINITE_EQ_FIELD_EXTENSION finite_eq_field_extension
FINITE_EQ_FINITELY_GENERATED_ALGEBRAIC_EXTENSION finite_eq_finitely_generated_algebraic_extension
FINITE_EXTENSION finite_extension_v1
FINITE_EXTENSION_ANY finite_extension_any
FINITE_EXTENSION_BASIS finite_extension_basis
FINITE_EXTENSION_ISOMORPHISM finite_extension_isomorphism
FINITE_EXTENSION_RING_MATROID finite_extension_ring_matroid
FINITE_EXTENSION_SPANNING finite_extension_spanning
FINITE_EXTENSION_TRANS finite_extension_trans
FINITE_EXTENSION_TRANS_EQ finite_extension_trans_eq
FINITE_FINITELY_GENERATED_ALGEBRAIC_EXTENSION finite_finitely_generated_algebraic_extension
FINITE_FINITE_FIELD_EXTENSION finite_finite_field_extension
FINITE_IMP_ALGEBRAIC_EXTENSION finite_imp_algebraic_extension
FINITE_IMP_ALGEBRAIC_EXTENSION_EXPLICIT finite_imp_algebraic_extension_explicit
FINITE_IMP_FIELD_EXTENSION finite_imp_field_extension
FINITE_IMP_FINITELY_GENERATED_EXTENSION finite_imp_finitely_generated_extension
FINITE_INTEGRAL_DOMAIN_SIZE finite_integral_domain_size
FINITE_SIMPLE_ALGEBRAIC_EXTENSION finite_simple_algebraic_extension
FINITE_SUBFIELD_GENERATED finite_subfield_generated
FINITE_SUBSET_SUBFIELD_GENERATED_DENOMINATOR finite_subset_subfield_generated_denominator
FROBENIUS_FIXED_FIELD frobenius_fixed_field
HAS_SIZE_FINITE_EXTENSION has_size_finite_extension
IN_SUBFIELD_0 in_subfield_0
IN_SUBFIELD_1 in_subfield_1
IN_SUBFIELD_ADD in_subfield_add
IN_SUBFIELD_GENERATED_FINITARY in_subfield_generated_finitary
IN_SUBFIELD_INV in_subfield_inv
IN_SUBFIELD_LINV in_subfield_linv
IN_SUBFIELD_MUL in_subfield_mul
IN_SUBFIELD_NEG in_subfield_neg
IN_SUBFIELD_POW in_subfield_pow
IN_SUBFIELD_PRODUCT in_subfield_product
IN_SUBFIELD_RINV in_subfield_rinv
IN_SUBFIELD_SUB in_subfield_sub
IN_SUBFIELD_SUM in_subfield_sum
IRREDUCIBLE_ALGEBRAICALLY_CLOSED_FIELD irreducible_algebraically_closed_field
ISOMORPHIC_RING_ALGEBRAICALLY_CLOSED_FIELD isomorphic_ring_algebraically_closed_field
KRONECKER_FIELD_EXTENSION kronecker_field_extension
KRONECKER_SIMPLE_FIELD_EXTENSION kronecker_simple_field_extension
POLY_CONST_SUBFIELD_GENERATED poly_const_subfield_generated
POLY_OVER_SUBFIELD_GENERATED_DENOMINATOR poly_over_subfield_generated_denominator
POLY_SQUAREFREE_EXPLICIT_EQ poly_squarefree_explicit_eq
POLY_SQUAREFREE_ROOT_COUNT poly_squarefree_root_count
POLY_SQUAREFREE_ROOT_COUNT_EQ poly_squarefree_root_count_eq
POLY_SQUAREFREE_ROOT_COUNT_EXPLICIT poly_squarefree_root_count_explicit
POLY_SUBFIELD_GENERATED_CLAUSES poly_subfield_generated_clauses
PRIME_SUBFIELD_EQ_SUBRING prime_subfield_eq_subring
PRIME_SUBFIELD_MINIMAL prime_subfield_minimal
RING_0_IN_SUBFIELD_GENERATED ring_0_in_subfield_generated
RING_1_IN_SUBFIELD_GENERATED ring_1_in_subfield_generated
RING_ADD_IN_SUBFIELD_GENERATED ring_add_in_subfield_generated
RING_AUTOMORPHISM_FROBENIUS_GEN ring_automorphism_frobenius_gen
RING_AUTOMORPHISM_OF_ALGEBRAIC_EXTENSION ring_automorphism_of_algebraic_extension
RING_BASES_CARD_EQ ring_bases_card_eq
RING_BASIS_EXISTS ring_basis_exists
RING_BASIS_IMP_SUBSET ring_basis_imp_subset
RING_BASIS_TRANS ring_basis_trans
RING_CARRIER_SUBFIELD_GENERATED_SUBRING_QUOTIENTS ring_carrier_subfield_generated_subring_quotients
RING_CARRIER_SUBFIELD_GENERATED_SUBSET ring_carrier_subfield_generated_subset
RING_CHAR_SUBFIELD_GENERATED ring_char_subfield_generated
RING_DEPENDENT_FINITARY ring_dependent_finitary
RING_DEPENDENT_FINITE ring_dependent_finite
RING_DEPENDENT_IMP_SUBSET ring_dependent_imp_subset
RING_DEPENDENT_MONO ring_dependent_mono
RING_DEPENDENT_SPAN_IMAGE ring_dependent_span_image
RING_DIV_IN_SUBFIELD_GENERATED ring_div_in_subfield_generated
RING_INDEPENDENT_CARD_LE_SPANNING ring_independent_card_le_spanning
RING_INDEPENDENT_EMPTY ring_independent_empty
RING_INDEPENDENT_FINITARY ring_independent_finitary
RING_INDEPENDENT_FINITE ring_independent_finite
RING_INDEPENDENT_FINITE_EQ ring_independent_finite_eq
RING_INDEPENDENT_IMP_SUBSET ring_independent_imp_subset
RING_INDEPENDENT_INSERT ring_independent_insert
RING_INDEPENDENT_LE_SPAN ring_independent_le_span
RING_INDEPENDENT_MONO ring_independent_mono
RING_INDEPENDENT_NONZERO ring_independent_nonzero
RING_INDEPENDENT_PRODUCTS ring_independent_products
RING_INDEPENDENT_TRANS ring_independent_trans
RING_INV_IN_SUBFIELD_GENERATED ring_inv_in_subfield_generated
RING_INV_SUBFIELD_GENERATED ring_inv_subfield_generated
RING_INV_SUBRING_GENERATED ring_inv_subring_generated
RING_MATROID ring_matroid_v1
RING_MATROID_BASIS ring_matroid_basis
RING_MATROID_FINITE_DIMENSIONAL ring_matroid_finite_dimensional
RING_MATROID_INDEPENDENT ring_matroid_independent
RING_MATROID_SPANNING ring_matroid_spanning
RING_MONOMORPHISM_POLY_EXTEND ring_monomorphism_poly_extend
RING_MUL_IN_SUBFIELD_GENERATED ring_mul_in_subfield_generated
RING_NEG_IN_SUBFIELD_GENERATED ring_neg_in_subfield_generated
RING_OF_INT_SUBFIELD_GENERATED ring_of_int_subfield_generated
RING_OF_NUM_SUBFIELD_GENERATED ring_of_num_subfield_generated
RING_POW_IN_SUBFIELD_GENERATED ring_pow_in_subfield_generated
RING_POW_SUBFIELD_GENERATED ring_pow_subfield_generated
RING_SIMPLE_ALGEBRAIC_EXTENSION_SPAN ring_simple_algebraic_extension_span
RING_SIMPLE_EXTENSION_SPAN ring_simple_extension_span
RING_SPANNING_ALT ring_spanning_alt
RING_SPANNING_CONTAINS_BASIS ring_spanning_contains_basis
RING_SPANNING_IMP_NONEMPTY ring_spanning_imp_nonempty
RING_SPANNING_IMP_SUBSET ring_spanning_imp_subset
RING_SPANNING_TRANS ring_spanning_trans
RING_SPAN_0 ring_span_0
RING_SPAN_ADD ring_span_add
RING_SPAN_EMPTY ring_span_empty
RING_SPAN_EXCHANGE ring_span_exchange
RING_SPAN_FINITARY ring_span_finitary
RING_SPAN_FINITE ring_span_finite
RING_SPAN_HOMOMORPHIC_IMAGE ring_span_homomorphic_image
RING_SPAN_INC ring_span_inc
RING_SPAN_MONO ring_span_mono
RING_SPAN_MUL ring_span_mul
RING_SPAN_NEG ring_span_neg
RING_SPAN_NONEMPTY ring_span_nonempty
RING_SPAN_RESTRICT ring_span_restrict
RING_SPAN_SELF ring_span_self
RING_SPAN_SING ring_span_sing
RING_SPAN_SPAN ring_span_span
RING_SPAN_SUB ring_span_sub
RING_SPAN_SUBSET ring_span_subset
RING_SPAN_SUBSET_ALGEBRAIC_SPAN ring_span_subset_algebraic_span
RING_SPAN_SUBSET_SUBFIELD_GENERATED ring_span_subset_subfield_generated
RING_SPAN_SUBSET_SUBRING_GENERATED ring_span_subset_subring_generated
RING_SPAN_SUM ring_span_sum
RING_SPAN_SUPERSET ring_span_superset
RING_SPAN_SUPERSET_EQ ring_span_superset_eq
RING_SPAN_SUPERSET_GEN ring_span_superset_gen
RING_SPAN_UNION ring_span_union
RING_SUB_SUBFIELD_GENERATED ring_sub_subfield_generated
SIMPLE_ALGEBRAIC_EXTEND_HOMOMORPHISM simple_algebraic_extend_homomorphism
SUBFIELDS_GENERATED_EQ subfields_generated_eq
SUBFIELD_GENERATED subfield_generated_v1
SUBFIELD_GENERATED_BY_MONOMORPHIC_IMAGE subfield_generated_by_monomorphic_image
SUBFIELD_GENERATED_BY_SUBFIELD_GENERATED subfield_generated_by_subfield_generated
SUBFIELD_GENERATED_EQ subfield_generated_eq
SUBFIELD_GENERATED_IDEMPOT subfield_generated_idempot
SUBFIELD_GENERATED_INC subfield_generated_inc
SUBFIELD_GENERATED_INC_GEN subfield_generated_inc_gen
SUBFIELD_GENERATED_INDUCT subfield_generated_induct
SUBFIELD_GENERATED_MINIMAL subfield_generated_minimal
SUBFIELD_GENERATED_MINIMAL_EQ subfield_generated_minimal_eq
SUBFIELD_GENERATED_MONO subfield_generated_mono
SUBFIELD_GENERATED_QUOTIENTS subfield_generated_quotients
SUBFIELD_GENERATED_REFL subfield_generated_refl
SUBFIELD_GENERATED_RESTRICT subfield_generated_restrict
SUBFIELD_GENERATED_RING_CARRIER subfield_generated_ring_carrier
SUBFIELD_GENERATED_SUBFIELD_GENERATED subfield_generated_subfield_generated
SUBFIELD_GENERATED_SUBRING_QUOTIENTS subfield_generated_subring_quotients
SUBFIELD_GENERATED_SUBSET_CARRIER subfield_generated_subset_carrier
SUBFIELD_GENERATED_SUBSET_CARRIER_SUBSET subfield_generated_subset_carrier_subset
SUBFIELD_GENERATED_SUPERSET subfield_generated_superset
SUBFIELD_GENERATED_TRIVIAL subfield_generated_trivial
SUBFIELD_GENERATED_UNION subfield_generated_union
SUBFIELD_GENERATED_UNION_LEFT subfield_generated_union_left
SUBFIELD_GENERATED_UNION_RIGHT subfield_generated_union_right
SUBFIELD_IMP_SUBRING_OF subfield_imp_subring_of
SUBFIELD_OF_ALGEBRAIC_EXTENSION subfield_of_algebraic_extension
SUBFIELD_OF_ALGEBRAIC_OVER subfield_of_algebraic_over
SUBFIELD_OF_FIELD_INV subfield_of_field_inv
SUBFIELD_OF_FIXPOINTS subfield_of_fixpoints
SUBFIELD_OF_HOMOMORPHIC_EQUALITIES subfield_of_homomorphic_equalities
SUBFIELD_OF_IMP_10 subfield_of_imp_10
SUBFIELD_OF_IMP_NONTRIVIAL subfield_of_imp_nontrivial
SUBFIELD_OF_IMP_SUBSET subfield_of_imp_subset
SUBFIELD_OF_INTER subfield_of_inter
SUBFIELD_OF_INTERS subfield_of_inters
SUBFIELD_OF_MONOMORPHIC_IMAGE subfield_of_monomorphic_image
SUBFIELD_OF_MONOMORPHIC_PREIMAGE subfield_of_monomorphic_preimage
SUBFIELD_OF_SUBFIELD_GENERATED subfield_of_subfield_generated
SUBFIELD_OF_SUBFIELD_GENERATED_EQ subfield_of_subfield_generated_eq
SUBFIELD_OF_SUBFIELD_GENERATED_REV subfield_of_subfield_generated_rev
SUBFIELD_OF_SUBFIELD_GENERATED_SUBFIELD_EQ subfield_of_subfield_generated_subfield_eq
SUBFIELD_OF_SUBRING_QUOTIENTS subfield_of_subring_quotients
SUBFIELD_SUBFIELD_GENERATED subfield_subfield_generated
SUBFIELD_SUBFIELD_GENERATED_ALT subfield_subfield_generated_alt
SUBFIELD_SUBFIELD_GENERATED_EQ subfield_subfield_generated_eq
SUBRING_EQ_SUBFIELD_GENERATED subring_eq_subfield_generated
SUBRING_GENERATED_BY_SUBFIELD_GENERATED subring_generated_by_subfield_generated
SUBRING_GENERATED_SUBFIELD_GENERATED subring_generated_subfield_generated
SUBRING_OF_ALGEBRAIC_OVER subring_of_algebraic_over
SUBRING_OF_SUBFIELD_GENERATED_EQ subring_of_subfield_generated_eq
SUBRING_SUBFIELD_ALGEBRAIC_OVER subring_subfield_algebraic_over
SUBRING_SUBFIELD_GENERATED subring_subfield_generated
SUBRING_SUBSET_SUBFIELD_GENERATED subring_subset_subfield_generated
SUBSET_CARRIER_SUBFIELD_GENERATED subset_carrier_subfield_generated
SUBSET_RING_SPAN subset_ring_span
TOTALLY_TRANSCENDENTAL_EXTENSION totally_transcendental_extension
TOTALLY_TRANSCENDENTAL_EXTENSION_ALT totally_transcendental_extension_alt
TRANSCENDENCE_BASES_CARD_EQ transcendence_bases_card_eq
TRANSCENDENCE_BASIS_CARD_LE_LEFT transcendence_basis_card_le_left
TRANSCENDENCE_BASIS_CARD_LE_RIGHT transcendence_basis_card_le_right
TRANSCENDENCE_BASIS_EXISTS transcendence_basis_exists
TRANSCENDENCE_BASIS_IMP_ALGEBRAICALLY_INDEPENDENT transcendence_basis_imp_algebraically_independent
TRANSCENDENCE_BASIS_IMP_ALGEBRAICALLY_SPANNING transcendence_basis_imp_algebraically_spanning
TRANSCENDENCE_BASIS_IMP_SUBSET transcendence_basis_imp_subset
TRANSCENDENCE_BASIS_OVER_ALGEBRAIC_EXTENSION transcendence_basis_over_algebraic_extension
TRANSCENDENCE_BASIS_TOWER_LAW transcendence_basis_tower_law
TRANSCENDENCE_BASIS_TRANS transcendence_basis_trans
TRANSCENDENTAL_OVER_IN_CARRIER transcendental_over_in_carrier
TRIVIAL_RING_SUBFIELD_GENERATED trivial_ring_subfield_generated
algebraic_extension algebraic_extension
algebraic_matroid algebraic_matroid
algebraic_over algebraic_over
algebraic_span algebraic_span
algebraically_closed_field algebraically_closed_field
algebraically_dependent algebraically_dependent
algebraically_independent algebraically_independent
algebraically_spanning algebraically_spanning
field_extension field_extension
finite_extension finite_extension
finitely_generated_extension finitely_generated_extension
ring_basis ring_basis
ring_dependent ring_dependent
ring_independent ring_independent
ring_matroid ring_matroid
ring_span_CASES ring_span_cases
ring_span_INDUCT ring_span_induct
ring_span_RULES ring_span_rules
ring_spanning ring_spanning
subfield_generated subfield_generated
subfield_of subfield_of
transcendence_basis transcendence_basis
transcendental_over transcendental_over
