Subsemiring 📖 | CompData | 351 mathmath: RingCone.coe_set_mk, Subsemiring.mem_sumSq, Subring.range_snd, Subsemiring.mem_toNonUnitalSubsemiring, Subsemiring.mem_sSup_of_directedOn, Subsemiring.mem_top, Subsemiring.coe_subtype, Subsemiring.comap_iInf, Polynomial.mem_lifts_iff_mem_alg, Subsemiring.closure_le, Subsemiring.centralizer_le, Subsemiring.eq_top_iff', Subsemiring.isClosed_topologicalClosure, RingPreordering.mem_mk, Subsemiring.coe_pow, Subsemiring.mem_carrier, Subsemiring.closure_mono, Subsemiring.op_injective, Polynomial.IsPrimitive.map_mul_mem_lifts_iff, IsGaloisGroup.algebraMap_ringEquivFixedPoints_symm_apply, Subring.toSubsemiring_injective, Subsemiring.mem_iInf, Polynomial.monomial_mem_lifts, CentroidHom.star_centerToCentroidCenter, Subsemiring.mem_closure, Polynomial.X_mem_lifts, RingHom.rangeS_eq_top, Subsemiring.toIsOrderedRing, Subsemiring.map_sup, Subsemiring.topologicalClosure_mono, Subsemiring.mem_smul_pointwise_iff_exists, Subsemiring.op_eq_bot, StarSubsemiring.mem_toSubsemiring, RingPreordering.toSubsemiring_strictMono, Subsemiring.gc_map_comap, Subsemiring.smul_mem_pointwise_smul_iff, Subsemiring.op_eq_top, Algebra.toSubsemiring_eq_top, Subring.coe_toSubsemiring, Subsemiring.center_eq_top, RingPreordering.toSubsemiring_lt_toSubsemiring, Subsemiring.op_sup, Subsemiring.mem_bot, Subsemiring.nontrivial, Subsemiring.op_le_op_iff, IsGaloisGroup.ringEquivFixedPoints_apply_coe, Subsemiring.homogeneousCore_mono, Subsemiring.le_op_iff, Subsemiring.map_iInf, Subsemiring.semitopologicalSemiring, Submonoid.subsemiringClosure_coe, Subsemiring.map_bot, RingHom.rangeSRestrict_surjective, Subsemiring.centerCongr_symm_apply_coe, IsScalarTower.subsemiring, mem_subalgebraOfSubsemiring, Polynomial.Splits.mem_lift_of_roots_mem_range, Subsemiring.coe_prod, RingEquiv.ofLeftInverseS_symm_apply, Subsemiring.op_sInf, Subsemiring.addEquivOp_apply_coe, Subring.toSubsemiring_mono, RingHom.rangeS_toSubmonoid, Subsemiring.isScalarTower, Subsemiring.smul_mem_pointwise_smul, Subring.toSubsemiring_lt_toSubsemiring, Subring.mopRingEquivOp_apply_coe, Subsemiring.pointwise_smul_toAddSubmonoid, Subsemiring.prod_top, RingCon.comapQuotientEquivRangeS_symm_mk, RingHom.coe_rangeSRestrict, Subsemiring.mem_iSup_of_directed, Subsemiring.smul_def, Subsemiring.coe_iSup_of_directed, Subsemiring.smul_bot, Subsemiring.coe_equivMapOfInjective_apply, Subalgebra.mopAlgEquivOp_symm_apply, Subsemiring.unop_le_unop_iff, Algebra.sInf_toSubsemiring, Subsemiring.coe_sInf, Subsemiring.toIsStrictOrderedRing, Subsemiring.coe_add, Subsemiring.coe_one, isArtinianRing_rangeS, Subring.mem_toSubsemiring, StarSubsemiring.toSubsemiring_le_iff, Polynomial.C_mem_lifts, Subsemiring.mem_inf, Subsemiring.unop_eq_top, RingCone.mem_mk, Subsemiring.prod_mono_right, Subsemiring.op_iSup, Subsemiring.mem_mk', Subsemiring.opEquiv_apply, RingPreordering.toSubsemiring_mono, Subsemiring.unop_sup, Subsemiring.coe_toSubmonoid, Subsemiring.subset_closure, Subring.toSubsemiring_le_toSubsemiring, StarSubsemiring.toSubsemiring_injective, Subsemiring.centerCongr_apply_coe, Algebra.sup_toSubsemiring, Subsemiring.toSubmonoid_mono, Subsemiring.one_mem, StarSubsemiring.coe_toSubsemiring, Subsemiring.closure_le_centralizer_centralizer, Subring.toSubsemiring_top, Polynomial.mem_lifts, Subsemiring.op_le_iff, Subsemiring.unop_sInf, Subsemiring.noZeroDivisors, Subsemiring.pointwise_central_scalar, Subalgebra.linearEquivOp_apply_coe, Subsemiring.mem_map_equiv, Polynomial.lifts_iff_ringHom_rangeS, Subsemiring.closure_singleton_one, Subring.topEquiv_apply, RingEquiv.subsemiringMap_apply_coe, Subsemiring.mem_op, Subring.coe_set_mk, Subsemiring.top_prod_top, Algebra.iSup_toSubsemiring, HomogeneousSubsemiring.mem_iff, Subring.mopRingEquivOp_symm_apply, Subsemiring.sInf_toAddSubmonoid, Subsemiring.comap_top, Subsemiring.centerToMulOpposite_symm_apply_coe, RingPreordering.toSubsemiring_le_toSubsemiring, IsHomogeneous.subsemiringClosure, Subsemiring.addEquivOp_symm_apply_coe, Polynomial.IsPrimitive.mul_map_mem_lifts_iff, Subsemiring.coe_carrier_toSubmonoid, Subsemiring.closure_singleton_natCast, Polynomial.C'_mem_lifts, Subsemiring.smul_mem_pointwise_smul_iff₀, Subsemiring.map_comap_eq, Polynomial.smul_mem_lifts, Subsemiring.mem_centralizer_iff, Subsemiring.centerToMulOpposite_apply_coe, Subsemiring.isHomogeneous_iff_subset_iInter, Subsemiring.pointwise_smul_subset_iff, RingPreordering.coe_toSubsemiring, Subsemiring.coe_copy, IsLocalRing.of_subring', Algebra.sSup_toSubsemiring, RingEquiv.subsemiringMap_symm_apply_coe, RingCon.comapQuotientEquivRangeS_mk, Subsemiring.toSubmonoid_strictMono, Subring.topEquiv_symm_apply_coe, Subsemiring.closure_iUnion, Subsemiring.ext_iff, Subsemiring.nsmul_mem, Subsemiring.center.smulCommClass_right, RingCon.coe_quotientKerEquivRangeS_mk, Subsemiring.rangeS_subtype, Subsemiring.comap_toSubmonoid, RingHom.rangeS_eq_map, Subsemiring.coe_sumSq, Subsemiring.range_fst, Subsemiring.mem_inv_pointwise_smul_iff₀, RingHom.mem_rangeS, RingHom.rangeS_top_iff_surjective, Subsemiring.closure_sUnion, Subsemiring.opEquiv_symm_apply, Algebra.iInf_toSubsemiring, Subalgebra.mem_mk, Subsemiring.closure_eq, Subsemiring.mem_comap, Subsemiring.map_inf, Algebra.top_toSubsemiring, Subsemiring.unop_injective, StarSubsemiring.coe_mk, Subring.toSubsemiring_strictMono, Subsemiring.pointwise_smul_def, Subsemiring.inclusion_injective, RingHom.sclosure_preimage_le, Subalgebra.coe_toSubsemiring, StarSubalgebra.rangeS_le, CharP.subsemiring, Subsemiring.mopRingEquivOp_apply_coe, Subsemiring.op_inf, IsLocalization.scaleRoots_commonDenom_mem_lifts, Subsemiring.zero_mem, Subsemiring.instSMulCommClassSubtypeMemCenter_1, RingHom.rangeS_top_of_surjective, Subsemiring.pointwise_smul_le_pointwise_smul_iff, Subsemiring.comap_inf, Subsemiring.coe_inf, Subsemiring.instSubsemiringClass, Subsemiring.coe_toNonUnitalSubsemiring, Subsemiring.isHomogeneous_iff_forall_subset, Subsemiring.coe_top, Subsemiring.unop_inf, Subalgebra.coe_valA, Subsemiring.unop_top, RingHom.mem_rangeS_self, Subsemiring.range_snd, IsLocalRing.of_subring, Subalgebra.toSubsemiring_injective, Subsemiring.smulCommClass_left, Subsemiring.toSubsemiring_homogeneousCore_le, Subalgebra.algEquivOpMop_apply, Polynomial.lifts_iff_coeff_lifts, Subsemiring.mem_toSubmonoid, Subsemiring.instCovariantClassHSMulLe, Subsemiring.map_iSup, Subsemiring.coe_centralizer, Subsemiring.toNonUnitalSubsemiring_injective, Subsemiring.topologicalClosure_minimal, Subsemiring.prod_mem, Subring.mk_le_mk, Subsemiring.op_sSup, Subsemiring.coe_pointwise_smul, Subring.ringEquivOpMop_symm_apply_coe, Subalgebra.mem_toSubsemiring, Subsemiring.mul_mem, Subsemiring.mem_closure_iff_exists_list, Subsemiring.mem_toAddSubmonoid, Subsemiring.map_toSubmonoid, isNoetherianRing_rangeS, RingPreordering.mem_toSubsemiring, Subsemiring.topologicalSemiring, Subsemiring.list_prod_mem, Algebra.algebraMap_ofSubsemiring, Subsemiring.ringEquivOpMop_symm_apply_coe, DirectSum.SetLike.IsHomogeneous.mem_iff, Subsemiring.instSMulCommClassSubtypeMemCenter, Polynomial.X_pow_mem_lifts, HomogeneousSubsemiring.toSubsemiring_injective, Subsemiring.coe_closure_eq, Subsemiring.topologicalClosure_coe, Subsemiring.mem_pointwise_smul_iff_inv_smul_mem, Subsemiring.closure_empty, Subsemiring.mem_map, NonUnitalNonAssocSemiring.mem_center_iff, Subsemiring.toAddSubmonoid_mono, HomogeneousSubsemiring.is_homogeneous', Subsemiring.coe_ofClass, Subsemiring.closure_univ, Subsemiring.coe_sSup_of_directedOn, Subsemiring.closure_union, Subsemiring.coe_matrix, Subsemiring.prod_mono_left, Subsemiring.subset_pointwise_smul_iff, Subsemiring.toAddSubmonoid_injective, Polynomial.lifts_iff_liftsRing, Subsemiring.mem_mk, Subsemiring.prod_bot_sup_bot_prod, Subsemiring.topEquiv_symm_apply_coe, Subsemiring.coe_op, Subsemiring.coe_zero, Polynomial.notMem_map_rangeS, Subsemiring.unop_bot, Subsemiring.list_sum_mem, Subsemiring.coe_set_mk, Subsemiring.centralizer_eq_top_iff_subset, CentroidHom.centerToCentroidCenter_apply, Subsemiring.pow_mem, Subsemiring.coe_mk', Subalgebra.linearEquivOp_symm_apply_coe, RingCon.rangeS_mk', Subsemiring.le_topologicalClosure, Subsemiring.smul_sup, Subring.mem_mk, IntermediateField.mem_mk, Subring.range_fst, Subsemiring.map_le_iff_le_comap, Subsemiring.ringEquivOpMop_apply, Subsemiring.subtype_apply, Subsemiring.toAddSubmonoid_strictMono, Subsemiring.isMulCommutative_closure, Subsemiring.pointwise_smul_le_pointwise_smul_iff₀, RingEquiv.ofLeftInverseS_apply, Subsemiring.instIsMulCommutative_closure, Subsemiring.top_prod, Subalgebra.pointwise_smul_toSubsemiring, Submonoid.subsemiringClosure_mem, Subsemiring.op_top, Subsemiring.unop_iInf, Subsemiring.continuousSMul, Subsemiring.subtype_injective, Subsemiring.unop_sSup, Subsemiring.unop_eq_bot, Subsemiring.sInf_toSubmonoid, Subsemiring.coe_toAddSubmonoid, Polynomial.lifts_iff_set_range, Subsemiring.multiset_prod_mem, Subalgebra.mem_perfectClosure_iff, Polynomial.erase_mem_lifts, Subsemiring.smulCommClass_right, Subsemiring.smul_closure, Subsemiring.le_centralizer_centralizer, Subsemiring.pointwise_smul_le_iff₀, Subsemiring.closure_singleton_zero, Polynomial.base_mul_mem_lifts, Subsemiring.mopRingEquivOp_symm_apply, Subsemiring.coe_iInf, Subsemiring.coe_center, Algebra.IsInvariant.charpoly_mem_lifts, Subsemiring.topEquiv_apply, Subsemiring.multiset_sum_mem, Subsemiring.coe_map, Subsemiring.toSubmonoid_injective, Module.End.mem_subsemiringCenter_iff, Subsemiring.mem_closure_of_mem, Subsemiring.instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMul, RingHom.mem_eqLocusS, Subsemiring.coe_mul, Subsemiring.mem_center_iff, Subalgebra.mopAlgEquivOp_apply_coe, Subalgebra.coe_mk, Subsemiring.faithfulSMul, RingHom.eqOn_sclosure, Subalgebra.algEquivOpMop_symm_apply_coe, Subalgebra.rangeS_le, Subring.ringEquivOpMop_apply, Subring.toSubsemiring_eq_top, Subsemiring.mem_pointwise_smul_iff_inv_smul_mem₀, Subring.pointwise_smul_toSubsemiring, Subsemiring.unop_iSup, Algebra.inf_toSubsemiring, Subsemiring.mem_prod, Subsemiring.mem_nonneg, Subsemiring.mem_unop, IsHomogeneous.subsemiringClosure_of_isHomogeneousElem, Polynomial.mem_lift_of_splits_of_roots_mem_range, integralClosure.mem_lifts_of_monic_of_dvd_map, Subsemiring.isLocalRing_of_unit, Polynomial.lifts_iff_coeffs_subset_range, Subsemiring.mem_closure_iff, Polynomial.mem_map_rangeS, Subsemiring.add_mem, Subalgebra.coe_valA', Subsemiring.mem_inv_pointwise_smul_iff, Subsemiring.coe_nonneg, RingHom.coe_rangeS, Subsemiring.coe_unop, Subsemiring.op_iInf, Subsemiring.mem_sInf, RingHom.eqLocusS_same, Subsemiring.sum_mem, RingPreordering.toSubsemiring_injective, Subsemiring.coe_comap, Subsemiring.le_pointwise_smul_iff₀, RingHom.ker_rangeSRestrict, Subsemiring.coe_bot, Subsemiring.prod_mono, Subsemiring.op_bot, RingPreordering.coe_set_mk, Subsemiring.center_le_centralizer, Subsemiring.center.smulCommClass_left
|