TheoremsisAlgebraic, isAlgebraic_iff, algEquivEquivAlgHom_apply, algEquivEquivAlgHom_symm_apply, algHom_bijective, algHom_bijective₂, bijective_of_isScalarTower, bijective_of_isScalarTower', exists_smul_eq_mul, extendScalars, faithfulSMul_tower_top, injective_tower_top, nontrivial, of_injective, of_ringHom_of_comp_eq, ringHom_of_comp_eq, tower_bot, tower_bot_of_injective, tower_top, infinite, of_ringHom_of_comp_eq, ringHom_of_comp_eq, injective_of_transcendental, isAlgebraic_of_not_injective, isAlgebraic_ringHom_iff_of_comp_eq, transcendental_of_subsingleton, transcendental_ringHom_iff_of_comp_eq, algHom, algebraMap, exists_nonzero_coeff_and_aeval_eq_zero, exists_nonzero_dvd, exists_nonzero_eq_adjoin_mul, exists_smul_eq_mul, extendScalars, inv, invOf, invOf_iff, inv_iff, nontrivial, of_aeval, of_aeval_of_transcendental, of_pow, of_ringHom_of_comp_eq, ringHom_of_comp_eq, tower_top, tower_top_of_subalgebra_le, isAlgebraic, transcendental, transcendental_X, algebra_isAlgebraic_bot_left_iff, algebra_isAlgebraic_bot_right, algebra_isAlgebraic_of_algebra_isAlgebraic_bot_left, inv_mem_of_algebraic, inv_mem_of_root_of_coeff_zero_ne_zero, isAlgebraic_bot_iff, isAlgebraic_iff_isAlgebraic_val, isAlgebraic_of_isAlgebraic_bot, isField_of_algebraic, aeval, aeval_of_transcendental, infinite, of_aeval, of_ringHom_of_comp_eq, of_tower_top, of_tower_top_of_subalgebra_le, pow, restrictScalars, ringHom_of_comp_eq, inv_eq_of_aeval_divX_ne_zero, inv_eq_of_root_of_coeff_zero_ne_zero, isAlgebraic_algHom_iff, isAlgebraic_algebraMap, isAlgebraic_algebraMap_iff, isAlgebraic_iff_not_injective, isAlgebraic_int, isAlgebraic_nat, isAlgebraic_of_mem_rootSet, isAlgebraic_one, isAlgebraic_rat, isAlgebraic_ringHom_iff_of_comp_eq, isAlgebraic_zero, is_transcendental_of_subsingleton, transcendental_algebraMap_iff, transcendental_iff_injective, transcendental_iff_ker_eq_bot, transcendental_ringHom_iff_of_comp_eq | 86 |