TheoremsisDomain_of_adjoin_range, isTranscendenceBasis_of_le_trdeg, isTranscendenceBasis_of_le_trdeg_of_finite, isTranscendenceBasis_of_lift_le_trdeg, isTranscendenceBasis_of_lift_le_trdeg_of_finite, trdeg_le_cardinalMk, instFinitaryMatroid, isAlgebraic_adjoin_iff_of_matroid_isBasis, isTranscendenceBasis_iff, isTranscendenceBasis_iff_isAlgebraic, isTranscendenceBasis_of_lift_trdeg_le, isTranscendenceBasis_of_lift_trdeg_le_of_finite, isTranscendenceBasis_of_trdeg_le, isTranscendenceBasis_of_trdeg_le_of_finite, matroid_cRank_eq, matroid_closure_eq, matroid_closure_of_subsingleton, matroid_e, matroid_indep_iff, matroid_isBase_iff, matroid_isBasis_iff, matroid_isBasis_iff_of_subsingleton, matroid_isFlat_iff, matroid_isFlat_of_subsingleton, matroid_spanning_iff, matroid_spanning_iff_of_subsingleton, algebraMap_comp, cardinalMk_eq, cardinalMk_eq_trdeg, isAlgebraic, isAlgebraic_field, isAlgebraic_iff, isEmpty_iff_isAlgebraic, lift_cardinalMk_eq, lift_cardinalMk_eq_trdeg, mvPolynomial, mvPolynomial', nonempty_iff_transcendental, of_isAlgebraic_adjoin_image_compl, of_isAlgebraic_adjoin_insert_diff, polynomial, sumElim_comp, trdeg_of_isDomain, trdeg_of_isDomain, exists_isTranscendenceBasis, exists_isTranscendenceBasis', exists_isTranscendenceBasis_between, exists_isTranscendenceBasis_subset, exists_isTranscendenceBasis_superset, isAlgebraic_iff_exists_isTranscendenceBasis_subset, isTranscendenceBasis_iff_algebraicIndependent_isAlgebraic, lift_trdeg_add_eq, trdeg_add_eq, trdeg_eq_iSup_cardinalMk_isTranscendenceBasis, trdeg_lt_aleph0 | 55 |