TheoremsquotientBot_mk, quotientBot_symm_mk, liftOfSurjective_apply, liftOfSurjective_comp, liftOfSurjective_surjective, coe_liftSupQuotQuotMkₐ, coe_quotLeftToQuotSupₐ, coe_quotQuotEquivCommₐ, coe_quotQuotEquivQuotOfLEₐ, coe_quotQuotEquivQuotOfLEₐ_symm, coe_quotQuotEquivQuotSupₐ, coe_quotQuotEquivQuotSupₐ_symm, coe_quotQuotMkₐ, coe_quotQuotToQuotSupₐ, ker_quotLeftToQuotSup, ker_quotQuotMk, liftSupQuotQuotMkₐ_toRingHom, quotLeftToQuotSupₐ_toRingHom, quotQuotEquivComm_algebraMap, quotQuotEquivComm_comp_quotQuotMk, quotQuotEquivComm_comp_quotQuotMkₐ, quotQuotEquivComm_mk_mk, quotQuotEquivComm_quotQuotMk, quotQuotEquivComm_symm, quotQuotEquivComm_symmₐ, quotQuotEquivCommₐ_toRingEquiv, quotQuotEquivQuotOfLE_comp_quotQuotMk, quotQuotEquivQuotOfLE_comp_quotQuotMkₐ, quotQuotEquivQuotOfLE_quotQuotMk, quotQuotEquivQuotOfLE_symm_comp_mk, quotQuotEquivQuotOfLE_symm_comp_mkₐ, quotQuotEquivQuotOfLE_symm_mk, quotQuotEquivQuotOfLEₐ_comp_mkₐ, quotQuotEquivQuotOfLEₐ_symm_toRingEquiv, quotQuotEquivQuotOfLEₐ_toRingEquiv, quotQuotEquivQuotSup_quotQuotMk, quotQuotEquivQuotSup_quot_quot_algebraMap, quotQuotEquivQuotSup_symm_quotQuotMk, quotQuotEquivQuotSupₐ_symm_toRingEquiv, quotQuotEquivQuotSupₐ_toRingEquiv, quotQuotMkₐ_toRingHom, quotQuotToQuotSupₐ_toRingHom, map_smul, algHom_ext, alg_map_eq, algebraMap_eq, coe_factorₐ, factorₐ_apply, factorₐ_apply_mk, factorₐ_comp, factorₐ_comp_mk, factorₐ_refl, isScalarTower, liftₐ_apply, liftₐ_comp, mk_algebraMap, mk_bijective_iff_eq_bot, mk_comp_algebraMap, mkₐ_eq_mk, mkₐ_ker, mkₐ_surjective, mkₐ_toRingHom, smul_top, span_singleton_one, algebraMap_quotient_injective, bot_quotient_isMaximal_iff, comap_map_mk, comap_map_quotientMk, comp_quotientMap_eq_of_comp_eq, exists_forall_sub_mem_ideal, fst_comp_quotientInfEquivQuotientProd, fst_comp_quotientMulEquivQuotientProd, injective_lift_iff, isPrime_map_quotientMk_of_isPrime, kerLiftAlg_injective, kerLiftAlg_mk, kerLiftAlg_toRingHom, ker_Pi_Quotient_mk, ker_quotientMap_mk, ker_quotient_lift, map_mk_eq_bot_of_le, map_quotient_self, mem_quotient_iff_mem, mem_quotient_iff_mem_sup, mk_ker, pi_mkQ_surjective, pi_quotient_surjective, quotientEquivAlgOfEq_coe_eq_factor, quotientEquivAlgOfEq_coe_eq_factorₐ, quotientEquivAlgOfEq_mk, quotientEquivAlgOfEq_symm, quotientEquivAlg_mk, quotientEquivAlg_symm, quotientEquiv_apply, quotientEquiv_mk, quotientEquiv_symm_apply, quotientEquiv_symm_mk, quotientInfEquivQuotientProd_fst, quotientInfEquivQuotientProd_snd, quotientInfToPiQuotient_inj, quotientInfToPiQuotient_mk, quotientInfToPiQuotient_mk', quotientInfToPiQuotient_surj, quotientKerAlgEquivOfRightInverse_apply, quotientKerAlgEquivOfRightInverse_symm_apply, quotientKerAlgEquivOfSurjective_apply, quotientKerAlgEquivOfSurjective_mk, quotientKerAlgEquivOfSurjective_symm_apply, quotientMap_algebraMap, quotientMap_comp_mk, quotientMap_injective, quotientMap_injective', quotientMap_mk, quotientMap_surjective, quotientMulEquivQuotientProd_fst, quotientMulEquivQuotientProd_snd, quotient_map_comp_mkₐ, quotient_map_mkₐ, snd_comp_quotientInfEquivQuotientProd, snd_comp_quotientMulEquivQuotientProd, quotientBot_mk, quotientBot_symm_mk, kerLift_injective, kerLift_mk, lift_injective_of_ker_le_ideal, apply, apply, quotientKerEquivOfSurjective_apply_mk, quotientKerEquivOfSurjective_symm_apply, quotientKerEquivOfSurjective_symm_comp | 130 |