TheoremsisAdjoinRootMonic_toAdjoinRoot, isAdjoinRoot_map_eq_mkₐ, isAdjoinRoot_root_eq_root, powerBasis'_minpoly_gen, adjoinRootAlgEquiv_apply_eq_map, adjoinRootAlgEquiv_apply_mk, adjoinRootAlgEquiv_apply_root, adjoinRootAlgEquiv_symm_apply_eq_mk, adjoinRootAlgEquiv_symm_apply_root, adjoin_root_eq_top, aeval_root_eq_map, aeval_root_self, algEquiv_algEquiv, algEquiv_apply_map, algEquiv_def, algEquiv_map, algEquiv_ofAlgEquiv, algEquiv_root, algEquiv_self, algEquiv_symm, algEquiv_trans, algebraMap_apply, apply_eq_lift, coe_liftHom, eq_lift, eq_liftHom, eval₂_repr_eq_eval₂_of_map_eq, ext, ext_iff, ext_map, isAlgebraic_root, ker_map, liftHom_algEquiv, liftHom_map, liftHom_root, lift_algEquiv, lift_algebraMap, lift_algebraMap_apply, lift_map, lift_root, lift_self, lift_self_apply, map_X, map_eq_zero_iff, map_repr, map_self, map_surjective, mem_ker_map, mkOfAdjoinEqTop_root, ofAlgEquiv_algEquiv, ofAlgEquiv_map_apply, ofAlgEquiv_root, primitive_element_root, repr_add_sub_repr_add_repr_mem_span, repr_zero_mem_span, subsingleton, basis_apply, basis_one, basis_repr, coeff_algebraMap, coeff_apply, coeff_apply_coe, coeff_apply_le, coeff_apply_lt, coeff_injective, coeff_one, coeff_root, coeff_root_pow, deg_ne_zero, deg_pos, ext_elem, ext_elem_iff, finite, finrank, isIntegral_root, liftPolyₗ_apply, map_modByMonic, map_modByMonicHom, minpoly_eq, modByMonicHom_map, modByMonicHom_root, modByMonicHom_root_pow, modByMonic_repr_map, monic, powerBasis_basis, powerBasis_dim, powerBasis_gen, finrank_quotient_span_eq_natDegree' | 88 |