| Name | Category | Theorems |
|---|
copy 📖 | CompOp | 4 mathmath: copy_toSubsemiring, LocalSubring.range_toSubring, coe_copy, copy_eq
|
instPartialOrder 📖 | CompOp | 43 mathmath: toAddSubgroup_mono, op_le_op_iff, le_op_iff, exists_le_valuationSubring_of_isIntegrallyClosedIn, Subfield.mk_le_mk, toSubmonoid_mono, toSubsemiring_mono, integralClosure_subring_le_iff, closure_mono, LocalSubring.toSubring_mono, Ideal.image_subset_nonunits_valuationSubring, closure_le_centralizer_centralizer, centralizer_le, pointwise_smul_subset_iff, prod_mono_left, Subfield.subring_closure_le, instCovariantClassHSMulLe, unop_le_unop_iff, toSubsemiring_strictMono, le_pointwise_smul_iff₀, op_le_iff, le_topologicalClosure, LocalSubring.le_ofPrime, toAddSubgroup_strictMono, closure_preimage_le, gc_map_comap, pointwise_smul_le_pointwise_smul_iff, integralClosure_le_iff, pointwise_smul_le_iff₀, mk_le_mk, toSubmonoid_strictMono, pointwise_smul_le_pointwise_smul_iff₀, AlgebraicGeometry.Proj.valuativeCriterion_existence_aux, opEquiv_apply, opEquiv_symm_apply, subset_pointwise_smul_iff, map_le_iff_le_comap, eq_iInf_of_isIntegrallyClosedIn, AlgebraicGeometry.exists_lift_of_germInjective_aux, closure_le, center_le_centralizer, prod_mono_right, RingHom.closure_preimage_le
|
instSetLike 📖 | CompOp | 304 mathmath: mem_center_iff, ValuationRing.mem_integer_iff, coe_sSup_of_directedOn, coe_unop, LocalSubring.isLocalRing, orderedSubtype_coe, Valuation.ltIdeal_le_leIdeal, coe_subtype, coe_comap, center.smulCommClass_right, NumberField.canonicalEmbedding.mem_span_latticeBasis, PadicInt.mem_subring_iff, Valuation.mem_leSubmodule_iff, zero_mem, ValuationSubring.mem_toSubring, IsPurelyInseparable.inseparable', IsPurelyInseparable.elemExponent_min', Subfield.mem_toSubring, instCanLiftSetCoeAndMemOfNatForallForallForallForallHAddForallForallForallForallHMulForallForallNeg, RingHom.rangeRestrict_surjective, Polynomial.Splits.mem_range_of_isRoot, instSMulCommClassSubtypeMemCenter, addEquivOp_apply_coe, centralizer_eq_top_iff_subset, Polynomial.monic_restriction, coe_op, Valued.integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField, mem_sSup_of_directedOn, Valuation.mem_ltIdeal_iff, center.coe_div, coe_inclusion, Valuation.leSubmodule_monotone, IsPurelyInseparable.elemExponent_min, Algebra.coe_algebraMap_ofSubring, instIsDiscreteValuationRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation, IsPurelyInseparable.elemExponent_def', coe_toSubsemiring, IsPurelyInseparable.hasExponent_iff, Polynomial.eval₂_restriction, center.coe_inv, Polynomial.Monic.eq_X_pow_char_pow_sub_C_pow_of_natSepDegree_eq_one, centerCongr_apply_coe, RingEquiv.ofLeftInverse_symm_apply, ExpChar.expChar_center_iff, instIsIntegrallyClosedInSubtypeMemSubringToSubringIntegralClosure, isLocalRing_top, RingCon.comapQuotientEquivRange_symm_mk, Algebra.mem_adjoin_iff, RingEquiv.ofLeftInverse_apply, Polynomial.restriction_one, Algebra.toSubring_bot, mem_pointwise_smul_iff_inv_smul_mem, IsNonarchimedeanLocalField.instIsDiscreteValuationRingSubtypeMemSubringIntegerValueGroupWithZeroValuation, IsPurelyInseparable.exists_pow_mem_range_tensorProduct, mem_pointwise_smul_iff_inv_smul_mem₀, RingHom.ker_rangeRestrict, RingHom.mem_range, ext_iff, coe_iSup_of_directed, Valuation.Integers.mem_of_integral, Valuation.leIdeal_map_algebraMap_eq_leSubmodule_min, mopRingEquivOp_apply_coe, coe_mk', coe_matrix, IsDedekindDomain.HeightOneSpectrum.mem_integers_of_valuation_le_one, Valued.integer.exists_norm_lt_one, Polynomial.degree_restriction, CharP.charP_center_iff, Subfield.mem_closure_iff, mem_closure, coe_toAddSubgroup, coe_pointwise_smul, eq_top_iff', RingHom.mem_range_self, CharP.subring', card_top, NumberField.canonicalEmbedding.integerLattice.inter_ball_finite, instFaithfulSMulSubtypeMem, mem_inf, iInf_valuationSubring_superset, HahnSeries.mem_cardSuppLTSubring, Rat.HeightOneSpectrum.adicCompletion.padicEquiv_bijOn, mem_toSubsemiring, mem_perfectClosure_iff_pow_mem, Algebra.SubmersivePresentation.HasCoeffs.coeffs_subset_range, RingCon.comapQuotientEquivRange_mk, Valuation.integer.integers, minpoly.two_le_natDegree_iff, coe_mul, Valuation.Integers.isIntegrallyClosed_integers, Ideal.image_subset_nonunits_valuationSubring, closure_eq, coe_inf, IsPurelyInseparable.HasExponent.has_exponent, closure_le_centralizer_centralizer, Polynomial.restriction_zero, is_noetherian_subring_closure, mem_prod, instSubringClass, mem_inv_pointwise_smul_iff, isPurelyInseparable_iff_pow_mem, TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst, LocalSubring.instAtPrimeSubtypeMemSubringToSubringOfPrime, centerToMulOpposite_symm_apply_coe, mem_closure_iff, isNoetherianRing_range, Valuation.pow_Uniformizer_is_pow_generator, subtype_injective, mem_map, topEquiv_apply, CharP.subring, coe_set_mk, smulCommClass_right, mopRingEquivOp_symm_apply, mem_top, Polynomial.coeff_ofSubring, PadicInt.Coe.ringHom_apply, mem_subalgebraOfSubring, coe_map, mem_smul_pointwise_iff_exists, LocalSubring.map_maximalIdeal_eq_top_of_isMax, mem_perfectClosure_iff, IsPurelyInseparable.exponent_def', mem_map_equiv, RingHom.eqOn_set_closure, mem_bot, Valued.integer.norm_le_one, subset_closure, mem_range_of_deriv_eq_zero, IsNonarchimedeanLocalField.instFiniteResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation, Subfield.coe_set_mk, Valuation.ltSubmodule_monotone, FractionalIdeal.mem_dual, minpoly.mem_range_of_degree_eq_one, topEquiv_symm_apply_coe, mem_unop, RingCon.coe_comapQuotientEquivRange_mk, coe_eq_zero_iff, mem_op, Valuation.HasExtension.val_algebraMap, instIsTopologicalRing, centerToMulOpposite_apply_coe, instIsDomainSubtypeMem, IsNonarchimedeanLocalField.instCompactSpaceSubtypeMemSubringIntegerValueGroupWithZeroValuation, IntermediateField.isPurelyInseparable_adjoin_iff_pow_mem, Valued.isClosed_integer, IsLocalRing.exists_factor_valuationRing, Algebra.algebraMap_ofSubring, IsSimpleRing.isField_center, smul_mem_pointwise_smul_iff₀, Valued.integer.properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField, TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd, Valuation.HasExtension.instIsLocalHomValuationInteger, Polynomial.filter_roots_map_range_eq_map_roots, Valued.integer.coe_span_singleton_eq_closedBall, Polynomial.map_restriction, Valued.isClopen_integer, coe_top, IsInvariantSubring.coe_subtypeHom', Valuation.HasExtension.instIsTorsionFreeInteger, mem_iSup_of_directed, Subfield.mem_mk, IsFractionRing.ringHom_fieldRange_eq_of_comp_eq, Valued.integer.isDiscreteValuationRing_of_compactSpace, isClosed_topologicalClosure, Valuation.ltSubmodule_le_leSubmodule, Valuation.leIdeal_mono, Valued.integer.norm_unit, Valuation.leIdeal_zero, integralClosure_le_iff, minpoly.ofSubring, Polynomial.mem_closure_X_union_C, LaurentSeries.powerSeriesEquivSubring_apply, mem_comap, coe_intCast, isIntegral_iff_isIntegral_closure_finite, mem_carrier, centerCongr_symm_apply_coe, isPurelyInseparable_iff, subtype_apply, Valued.integer.exists_nnnorm_lt_one, Subfield.coe_toSubring, Valued.integer.properSpace_iff_compactSpace_integer, ringEquivOpMop_symm_apply_coe, Polynomial.mem_map_range, coe_toSubmonoid, minpoly.degree_eq_one_iff, continuousSMul, coe_zero, IsPurelyInseparable.pow_mem, NumberField.mem_span_integralBasis, Polynomial.coeff_restriction, LaurentSeries.powerSeriesEquivSubring_coe_apply, isArtinianRing_range, TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd, Valuation.integers_nontrivial, TopCat.Sheaf.objSupIsoProdEqLocus_inv_eq_iff, center.smulCommClass_left, LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent, Valuation.Integer.not_isUnit_iff_valuation_lt_one, coe_neg, minpoly.natSepDegree_eq_one_iff_pow_mem, smul_def, Valuation.exists_pow_Uniformizer, Submodule.mem_traceDual, Polynomial.toSubring_zero, Valued.isOpen_integer, Valued.integer.finite_quotient_maximalIdeal_pow_of_finite_residueField, IsPurelyInseparable.exponent_min, Valuation.integer.coe_span_singleton_eq_setOf_le_v_coe, Valued.integer.mem_iff, Polynomial.lifts_iff_liftsRing, LocalSubring.instIsScalarTowerSubtypeMemSubringToSubringOfPrime, Polynomial.Monic.eq_X_pow_char_pow_sub_C_of_natSepDegree_eq_one_of_irreducible, mem_centralizer_iff, instNontrivialSubtypeMem, instCharPLinearMapSubtypeMemSubringCenterId, mem_toAddSubgroup, instNoZeroDivisorsSubtypeMem, TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst, Valued.integer.isUnit_iff_norm_eq_one, mem_closure_of_mem, Valued.integer.isPrincipalIdealRing_of_compactSpace, coe_prod, IsPurelyInseparable.hasExponent_iff', instIsLocalRingSubtypeMemSubringMapOfNontrivial, IsIntegral.mem_range_algebraMap_of_minpoly_splits, Valuation.mem_ltSubmodule_iff, LocalSubring.le_def, Polynomial.natDegree_restriction, mem_mk, minpoly.instIsScalarTowerSubtypeMemSubringSubalgebraIntegralClosure, minpoly.natDegree_eq_one_iff, mem_iInf, Valued.toNormedField.setOf_mem_integer_eq_closedBall, ValuationRing.instValuationRingInteger, IsPurelyInseparable.exponent_min', Valuation.mem_leIdeal_iff, instSMulCommClassSubtypeMemCenter_1, bijective_rangeRestrict_comp_of_valuationRing, coe_bot, Polynomial.coeff_restriction', Valued.integer.totallyBounded_iff_finite_residueField, Valuation.Uniformizer.is_generator, instExpCharLinearMapSubtypeMemSubringCenterId, coe_center, mem_sInf, Polynomial.support_restriction, IsFractionRing.lift_fieldRange, coe_ofClass, LinearMap.commute_transvections_iff_of_basis, mem_toSubmonoid, Subalgebra.mem_toSubring, coe_equivMapOfInjective_apply, Valuation.ltIdeal_mono, range_subtype, coe_add, ValuationRing.coe_equivInteger_apply, Algebra.algebraMap_ofSubring_apply, RootPairing.toLinearMap_apply_apply_mem_range_algebraMap, Valuation.leSubmodule_zero, Valuation.mem_integer_iff, Valued.integer.norm_coe_unit, closure_le, Subalgebra.coe_toSubring, coe_pow, IsNonarchimedeanLocalField.instCompleteSpaceSubtypeMemSubringIntegerValueGroupWithZeroValuation, IsPurelyInseparable.exponent_def, Valuation.leSubmodule_comap_algebraMap_eq_leIdeal, smul_mem_pointwise_smul_iff, instIsPrincipalIdealRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation, coe_centralizer, IsPurelyInseparable.exists_pow_pow_mem_range_tensorProduct_of_expChar, ringEquivOpMop_apply, LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent_of_basis, JacobsonNoether.exists_separable_and_not_isCentral, instIsIntegrallyClosedSubtypeMemSubring, FixedPoints.minpoly.eval₂, Polynomial.coeffs_ofSubring, Valuation.Uniformizer.valuation_gt_one, mem_mk', Differential.ContainConstants.mem_range_of_deriv_eq_zero, coe_sInf, IsPurelyInseparable.inseparable, mem_inv_pointwise_smul_iff₀, Valued.integer.exists_norm_coe_lt_one, coe_iInf, instIsScalarTowerSubtypeMem, smulCommClass_left, one_mem, RingHom.coe_range, coe_one, coe_natCast, RingHom.coe_rangeRestrict, addEquivOp_symm_apply_coe, Valuation.HasExtension.algebraMap_injective, ValuationRing.instIsFractionRingInteger, IsInvariantSubring.coe_subtypeHom, IsPurelyInseparable.elemExponent_def, RingHom.mem_eqLocus, IntermediateField.isPurelyInseparable_adjoin_simple_iff_pow_mem, Valuation.HasExtension.instIsScalarTowerInteger, Valuation.HasExtension.val_smul, Polynomial.toSubring_one
|
mk' 📖 | CompOp | 4 mathmath: coe_mk', mk'_toSubmonoid, mk'_toAddSubgroup, mem_mk'
|
ofClass 📖 | CompOp | 2 mathmath: integralClosure_subring_le_iff, coe_ofClass
|
subtype 📖 | CompOp | 15 mathmath: orderedSubtype_coe, coe_subtype, Polynomial.eval₂_restriction, Ideal.image_subset_nonunits_valuationSubring, subtype_injective, MvPowerSeries.map_toSubring, Algebra.algebraMap_ofSubring, IsInvariantSubring.coe_subtypeHom', subtype_apply, Subfield.toSubring_subtype_eq_subtype, Subalgebra.toSubring_subtype, Polynomial.map_toSubring, range_subtype, PowerSeries.map_toSubring, FixedPoints.minpoly.eval₂
|
toAddSubgroup 📖 | CompOp | 12 mathmath: toAddSubgroup_mono, toAddSubgroup_lt_toAddSubgroup, coe_toAddSubgroup, pointwise_smul_toAddSubgroup, toAddSubgroup_strictMono, sInf_toAddSubgroup, toAddSubgroup_le_toAddSubgroup, mem_toAddSubgroup, toAddSubgroup_eq_top, mk'_toAddSubgroup, toAddSubgroup_injective, toAddSubgroup_top
|
toCommRing 📖 | CompOp | 27 mathmath: Irreducible.maximalIdeal_eq_setOf_le_v_coe, Valued.integer.compactSpace_iff_completeSpace_and_isDiscreteValuationRing_and_finite_residueField, instIsDiscreteValuationRingSubtypeMemSubringIntegerWithZeroMultiplicativeIntValuation, instIsIntegrallyClosedInSubtypeMemSubringToSubringIntegralClosure, Algebra.toSubring_bot, IsNonarchimedeanLocalField.instIsDiscreteValuationRingSubtypeMemSubringIntegerValueGroupWithZeroValuation, iInf_valuationSubring_superset, Valuation.integer.integers, Valuation.Integers.isIntegrallyClosed_integers, TopCat.Sheaf.objSupIsoProdEqLocus_hom_fst, IsNonarchimedeanLocalField.instFiniteResidueFieldSubtypeMemSubringIntegerValueGroupWithZeroValuation, Valued.integer.properSpace_iff_completeSpace_and_isDiscreteValuationRing_integer_and_finite_residueField, TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd, Valued.integer.isDiscreteValuationRing_of_compactSpace, minpoly.ofSubring, LaurentSeries.powerSeriesEquivSubring_apply, isIntegral_iff_isIntegral_closure_finite, LaurentSeries.powerSeriesEquivSubring_coe_apply, TopCat.Sheaf.objSupIsoProdEqLocus_hom_snd, TopCat.Sheaf.objSupIsoProdEqLocus_inv_eq_iff, Valued.integer.finite_quotient_maximalIdeal_pow_of_finite_residueField, TopCat.Sheaf.objSupIsoProdEqLocus_inv_fst, minpoly.instIsScalarTowerSubtypeMemSubringSubalgebraIntegralClosure, ValuationRing.instValuationRingInteger, Irreducible.maximalIdeal_pow_eq_setOf_le_v_coe_pow, ValuationRing.coe_equivInteger_apply, instIsIntegrallyClosedSubtypeMemSubring
|
toNonUnitalSubring 📖 | CompOp | 4 mathmath: one_mem_toNonUnitalSubring, ValuationSubring.nonunits_le, toNonUnitalSubring_toSubring, NonUnitalSubring.toSubring_toNonUnitalSubring
|
toRing 📖 | CompOp | 93 mathmath: PowerSeries.coeff_toSubring, Valuation.leSubmodule_v_le_of_mem, orderedSubtype_coe, Valuation.ltIdeal_le_leIdeal, coe_subtype, Valuation.mem_leSubmodule_iff, RingHom.rangeRestrict_surjective, addEquivOp_apply_coe, Polynomial.monic_toSubring, Polynomial.monic_restriction, Valuation.mem_ltIdeal_iff, coe_inclusion, Valuation.leSubmodule_monotone, Polynomial.eval₂_restriction, RingEquiv.ofLeftInverse_symm_apply, ExpChar.expChar_center_iff, RingCon.comapQuotientEquivRange_symm_mk, RingEquiv.ofLeftInverse_apply, Polynomial.restriction_one, RingHom.ker_rangeRestrict, Valuation.ltIdeal_v_le_of_mem, mopRingEquivOp_apply_coe, Polynomial.degree_restriction, CharP.charP_center_iff, CharP.subring', RingCon.comapQuotientEquivRange_mk, Polynomial.natDegree_toSubring, coe_mul, Ideal.image_subset_nonunits_valuationSubring, Polynomial.restriction_zero, isNoetherianRing_range, subtype_injective, topEquiv_apply, CharP.subring, mopRingEquivOp_symm_apply, Polynomial.coeff_ofSubring, LocalSubring.map_maximalIdeal_eq_top_of_isMax, Polynomial.coeff_toSubring, Valuation.ltSubmodule_monotone, topEquiv_symm_apply_coe, RingCon.coe_comapQuotientEquivRange_mk, Valuation.HasExtension.val_algebraMap, instIsTopologicalRing, MvPowerSeries.map_toSubring, instIsDomainSubtypeMem, Valuation.leIdeal_v_le_of_mem, MvPowerSeries.constantCoeff_toSubring, MvPowerSeries.order_toSubring, Polynomial.support_toSubring, IsInvariantSubring.coe_subtypeHom', Valuation.HasExtension.instIsTorsionFreeInteger, Valuation.ltSubmodule_le_leSubmodule, Valuation.leIdeal_mono, Valuation.leIdeal_zero, coe_intCast, subtype_apply, ringEquivOpMop_symm_apply_coe, Valuation.ltSubmodule_v_le_of_mem, Polynomial.coeff_restriction, isArtinianRing_range, MvPowerSeries.coeff_toSubring, Polynomial.toSubring_zero, Polynomial.coeff_toSubring', PowerSeries.order_toSubring, Polynomial.degree_toSubring, instNoZeroDivisorsSubtypeMem, Valuation.HasExtension.mk_smul_mk, Valuation.mem_ltSubmodule_iff, LocalSubring.le_def, PowerSeries.constantCoeff_toSubring, Polynomial.natDegree_restriction, Valuation.mem_leIdeal_iff, bijective_rangeRestrict_comp_of_valuationRing, Polynomial.coeff_restriction', Polynomial.map_toSubring, Polynomial.support_restriction, MvPowerSeries.weightedOrder_toSubring, coe_equivMapOfInjective_apply, Valuation.ltIdeal_mono, range_subtype, coe_add, Valuation.leSubmodule_zero, ringEquivOpMop_apply, PowerSeries.map_toSubring, FixedPoints.minpoly.eval₂, coe_natCast, RingHom.coe_rangeRestrict, addEquivOp_symm_apply_coe, Valuation.HasExtension.algebraMap_injective, IsInvariantSubring.coe_subtypeHom, Valuation.HasExtension.instIsScalarTowerInteger, Valuation.HasExtension.val_smul, Polynomial.toSubring_one
|
toSubsemiring 📖 | CompOp | 42 mathmath: copy_toSubsemiring, toSubsemiring_inj, centralizer_toSubsemiring, toSubsemiring_injective, addEquivOp_apply_coe, Subsemiring.toSubring_toSubsemiring, coe_toSubsemiring, toSubmonoid_mono, toSubsemiring_mono, toSubsemiring_lt_toSubsemiring, Subalgebra.toSubring_toSubsemiring, mopRingEquivOp_apply_coe, coe_matrix, mem_toSubsemiring, mk'_toSubmonoid, toSubsemiring_le_toSubsemiring, toSubsemiring_top, mopRingEquivOp_symm_apply, ValuationSubring.mem_carrier, center_toSubsemiring, subalgebraOfSubring_toSubsemiring, toSubsemiring_strictMono, Subfield.coe_inf, op_toSubsemiring, ValuationSubring.mem_or_inv_mem', mem_carrier, toSubmonoid_strictMono, ringEquivOpMop_symm_apply_coe, coe_toSubmonoid, unop_toSubsemiring, Subfield.mem_toSubmonoid, sInf_toSubmonoid, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, mem_toSubmonoid, ringEquivOpMop_apply, toSubsemiring_eq_top, pointwise_smul_toSubsemiring, Subfield.mem_carrier, Subfield.coe_toSubmonoid, addEquivOp_symm_apply_coe, toSubmonoid_injective, centralizer_toSubmonoid
|