ring

📁 Source: MathlibTest/ring.lean

Statistics

Metric	Count
Definitions ring, ring, ring, ring, ring, ring, ring, ring, ring, ring, ring, ring, ring, ring, ring, ring, ring, ring, ring, ring, ring, ring	22
Theorems	0
Total	22

AddMonoidAlgebra

Definitions

Name	Category	Theorems
ring 📖	CompOp	110 math math: MonomialOrder.monic_X_sub_C, Polynomial.toFinsupp_zsmul, Algebra.Generators.toAlgHom_ofComp_localizationAway, Algebra.Presentation.localizationAway_relation, StandardEtalePresentation.toPresentation_algebra_smul, MvPolynomial.vars_sub_of_disjoint, MonomialOrder.degree_sub_le, WittVector.mul_polyOfInterest_aux2, Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp, Algebra.PreSubmersivePresentation.ofHasCoeffs_σ', Algebra.Presentation.quotientEquiv_symm, Polynomial.ofFinsupp_sub, Algebra.Generators.naive_val, instIsIntegralMvPolynomial, Algebra.Generators.compLocalizationAwayAlgHom_X_inl, MvPolynomial.transcendental_polynomial_aeval_X_iff, StandardEtalePair.equivMvPolynomialQuotient_symm_apply, xInTermsOfW_eq, MvPolynomial.transcendental_supported_X_iff, Algebra.SubmersivePresentation.jacobianRelations_spec, WeierstrassCurve.Projective.polynomialZ_eq, MvPolynomial.IsHomogeneous.sub, MvPolynomial.quotient_map_C_eq_zero, MvPolynomial.vars_sub_subset, IsLocalization.Away.mvPolynomialQuotientEquiv_apply, WittVector.mul_polyOfInterest_aux4, Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom, WittVector.bind₁_wittMulN_wittPolynomial, MonomialOrder.degree_X_sub_C, xInTermsOfW_aux, MvPolynomial.degreeOf_sub_le, MvPolynomial.combinatorial_nullstellensatz_exists_linearCombination, wittStructureRat_rec, WittVector.mul_polyOfInterest_vars, MonomialOrder.sPolynomial_def, MvPolynomial.mk_eq_eval₂, MvPolynomial.degrees_sub_le, wittStructureRat_rec_aux, Algebra.Generators.ker_localizationAway, MvPolynomial.mkₐ_eq_aeval, instIsAlgebraicMvPolynomialOfNoZeroDivisors, Algebra.Generators.comp_localizationAway_ker, MvPolynomial.mul_esymm_eq_sum, MvPolynomial.universalFactorizationMapPresentation_relation, WeierstrassCurve.Projective.polynomialX_eq, MvPolynomial.eval₂_sub, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul, WittVector.frobeniusPolyAux_eq, Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul, Algebra.Generators.cMulXSubOneCotangent_eq, MvPolynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing, Algebra.SubmersivePresentation.sum_jacobianRelationsOfHasCoeffs_mul_relationOfHasCoeffs, WeierstrassCurve.Jacobian.polynomialZ_eq, toDirectSum_intCast, MvPolynomial.ker_eval₂Hom_universalFactorizationMap, WittVector.mul_polyOfInterest_aux1, MvPolynomial.quotientEquivQuotientMvPolynomial_leftInverse, MvPolynomial.quotient_mk_comp_C_injective, AlgebraicClosure.Monics.map_eq_prod, MvPolynomial.eval_sub, MvPolynomial.totalDegree_sub, StandardEtalePresentation.toPresentation_σ', MvPolynomial.isIntegral_iff_isIntegral_coeff, WittVector.bind₁_verschiebungPoly_wittPolynomial, Algebra.Presentation.relation_comp_localizationAway_inl, MonoidAlgebra.Submodule.instIsSemisimpleRingAddMonoidAlgebra, MvPolynomial.coeff_sub, Algebra.SubmersivePresentation.exists_sum_eq_σ_jacobian_mul_σ_jacobian_inv_sub_one, DirectSum.toAddMonoidAlgebra_intCast, MvPolynomial.transcendental_polynomial_aeval_X, WittVector.polyOfInterest_vars_eq, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul, instIsAlgebraicMvPolynomialOfNoZeroDivisors_1, KaehlerDifferential.mvPolynomialBasis_repr_D, WeierstrassCurve.Jacobian.polynomialX_eq, MvPolynomial.transcendental_X, MvPolynomial.psum_eq_mul_esymm_sub_sum, KaehlerDifferential.mvPolynomialBasis_repr_comp_D, Polynomial.toFinsupp_sub, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, MvPolynomial.support_sub, StandardEtalePresentation.toPresentation_val, Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero, Polynomial.homogenize_sub, MvPolynomial.degreeOf_sub_lt, Polynomial.ofFinsupp_zsmul, MvPolynomial.totalDegree_sub_C_le, MonomialOrder.leadingCoeff_sub_of_lt, Algebra.Presentation.quotientEquiv_mk, WittVector.mul_polyOfInterest_aux5, MonomialOrder.degree_sub_leadingTerm_lt_degree, MvPolynomial.transcendental_supported_polynomial_aeval_X_iff, StandardEtalePresentation.toPresentation_relation, Algebra.PreSubmersivePresentation.ofHasCoeffs_val, MvPolynomial.C_sub, MvPolynomial.quotientEquivQuotientMvPolynomial_rightInverse, WittVector.mul_polyOfInterest_aux3, MvPolynomial.universalFactorizationMapPresentation_jacobiMatrix, Polynomial.toFinsupp_intCast, MvPolynomial.transcendental_supported_X, C_p_pow_dvd_bind₁_rename_wittPolynomial_sub_sum, MvPolynomial.IsSymmetric.sub, WittVector.wittSub_zero, MonomialOrder.degree_sub_of_lt, MonomialOrder.degree_sub_leadingTerm_lt_iff, MonomialOrder.degree_sub_leadingTerm_le, Polynomial.ofFinsupp_intCast, Algebra.Generators.C_mul_X_sub_one_mem_ker, MvPolynomial.transcendental_supported_polynomial_aeval_X, Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val

CauSeq

Definitions

Name	Category	Theorems
ring 📖	CompOp	—

CauSeq.Completion.Cauchy

Definitions

Name	Category	Theorems
ring 📖	CompOp	1 math math: CauSeq.Completion.ofRatRingHom_apply

ContMDiffMap

Definitions

Name	Category	Theorems
ring 📖	CompOp	—

ContinuousLinearMap

Definitions

Name	Category	Theorems
ring 📖	CompOp	34 math math: mulLeftRight_isBoundedBilinear, DoubleCentralizer.intCast_snd, intCast_apply, CStarMatrix.norm_def', mulLeftRight_apply, CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM, hasFDerivAt_ringInverse, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe, RKHS.posSemidef_tfae, fderiv_inverse, fderivWithin_inv', LinearMap.IsSymmetric.coe_toSelfAdjoint, IsCompactOperator.hasEigenvalue_or_mem_resolventSet, NonUnitalAlgHom.coe_Lmul, LinearMap.IsSymmetric.toSelfAdjoint_apply, opNorm_mulLeftRight_apply_le, PositiveLinearMap.gnsStarAlgHom_apply, hasStrictFDerivAt_ringInverse, spectrum.hasFDerivAt_resolvent, opNorm_mulLeftRight_apply_apply_le, spectralRadius_eq_nnnorm, spectrum_eq, IsPositive.spectrumRestricts, DoubleCentralizer.natCast_toProd, hasStrictFDerivAt_inv', opNorm_mulLeftRight_le, DoubleCentralizer.intCast_fst, VonNeumannAlgebra.instSubringClass, hasFDerivAt_inv', RKHS.posSemidef_kernel, DoubleCentralizer.intCast_toProd, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply, IsCompactOperator.hasEigenvalue_iff_mem_spectrum, fderiv_inv'

DirectSum

Definitions

Name	Category	Theorems
ring 📖	CompOp	4 math math: AddMonoidAlgebra.toDirectSum_intCast, toAddMonoidAlgebra_intCast, of_intCast, TensorProduct.tmul_of_gradedMul_of_tmul

DirectSum.GradeZero

Definitions

Name	Category	Theorems
ring 📖	CompOp	—

Equiv

Definitions

Name	Category	Theorems
ring 📖	CompOp	—

FirstOrder.Language

Definitions

Name	Category	Theorems
ring 📖	CompOp	37 math math: FirstOrder.Ring.realize_neg, FirstOrder.Field.modelField_of_modelACF, FirstOrder.Field.realize_genericMonicPolyHasRoot, FirstOrder.ACF_models_genericPolyMapSurjOnOfInjOn_of_prime, FirstOrder.Field.realize_eqZero, FirstOrder.Field.ACF_categorical, FirstOrder.Field.ACF_zero_realize_iff_finite_ACF_prime_not_realize, FirstOrder.ACF_models_genericPolyMapSurjOnOfInjOn_of_prime_or_zero, FirstOrder.Ring.realize_termOfFreeCommRing, FirstOrder.Ring.mul_def, FirstOrder.Field.instModelACFOfCharPOfIsAlgClosed, FirstOrder.Ring.neg_def, FirstOrder.Ring.CompatibleRing.funMap_mul, FirstOrder.Field.finite_ACF_prime_not_realize_of_ACF_zero_realize, FirstOrder.Ring.realize_add, FirstOrder.Field.FieldAxiom.realize_toSentence_iff_toProp, FirstOrder.Ring.CompatibleRing.funMap_one, FirstOrder.Field.ACF_zero_realize_iff_infinite_ACF_prime_realize, FirstOrder.Ring.CompatibleRing.funMap_add, FirstOrder.Ring.realize_mul, FirstOrder.Field.ACF_isSatisfiable, FirstOrder.Ring.realize_zero, FirstOrder.Ring.realize_one, FirstOrder.Field.instModelField, FirstOrder.realize_genericPolyMapSurjOnOfInjOn, FirstOrder.Ring.CompatibleRing.funMap_neg, FirstOrder.Field.model_hasChar_of_charP, FirstOrder.Ring.one_def, FirstOrder.Field.instModelFieldOfCharOfACF, FirstOrder.Ring.CompatibleRing.funMap_zero, FirstOrder.Ring.add_def, FirstOrder.Ring.mvPolynomial_zeroLocus_definable, FirstOrder.Ring.zero_def, FirstOrder.Field.model_fieldOfChar_of_charP, FirstOrder.Ring.card_ring, FirstOrder.Field.ACF_isComplete, FirstOrder.Field.charP_iff_model_fieldOfChar

FreeAbelianGroup

Definitions

Name	Category	Theorems
ring 📖	CompOp	4 math math: liftMonoid_coe_addMonoidHom, liftMonoid_coe, ofMulHom_coe, liftMonoid_symm_coe

Function.Injective

Definitions

Name	Category	Theorems
ring 📖	CompOp	—

Function.Surjective

Definitions

Name	Category	Theorems
ring 📖	CompOp	—

Ideal.Quotient

Definitions

Name	Category	Theorems
ring 📖	CompOp	385 math math: PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_apply, Ideal.quotientEquivAlgOfEq_coe_eq_factorₐ, IsLocalization.surjective_quotientMap_of_maximal_of_localization, PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply, DoubleQuot.liftSupQuotQuotMkₐ_toRingHom, IsAdicComplete.StrictMono.mk_liftRingHom, Int.quotientSpanEquivZMod_comp_Quotient_mk, StandardEtalePair.inv_aeval_X_g, Algebra.TensorProduct.quotIdealMapEquivQuotTensor_mk, IsLocalization.AtPrime.equivQuotientMapOfIsMaximal_apply_mk, RingTheory.Sequence.isWeaklyRegular_cons_iff', Ideal.quotientEquiv_symm_apply, Perfection.mk_comp_teichmuller₀, AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_symm_mk, Ideal.algebraMap_quotient_injective, DoubleQuot.coe_quotQuotEquivQuotOfLEₐ_symm, Ring.coe_jacobson_quotient, Polynomial.fiberEquivQuotient_tmul, Ideal.quotientMap_comp_mk, RingHom.quotientKerEquivOfSurjective_symm_apply, factor_comp_mk, Ideal.comap_cotangentIdeal, DoubleQuot.coe_quotQuotMkₐ, factorₐ_comp_mk, AdjoinRoot.quotMapOfEquivQuotMapCMapMk_mk, Int.quotientSpanNatEquivZMod_comp_Quotient_mk, StandardEtalePresentation.toPresentation_algebra_smul, Ideal.quotient_map_C_eq_zero, AlgHom.IsArithFrobAt.mk_apply, Ideal.map_mk_comap_factor, WittVector.factorPowSucc_comp_fontaineThetaModPPow, PowerBasis.quotientEquivQuotientMinpolyMap_apply, Ideal.quotientInfToPiQuotient_inj, Ideal.torsionMapQuot_apply, algEquivOfEqMap_apply, factor_mk, Ideal.algebraMap_quotient_residueField_mk, Ideal.quotientInfToPiQuotient_surj, AlgEquiv.prodQuotientOfIsIdempotentElem_apply, DoubleQuot.quotQuotEquivQuotOfLEₐ_symm_toRingEquiv, Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp, Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown, DoubleQuot.quotQuotEquivComm_symmₐ, WittVector.factorPowSucc_fontaineThetaModPPow_eq, coe_factorₐ, factor_comp_apply, Ideal.quotientEquivAlg_mk, Ring.jacobson_quotient_of_le, Ideal.quotientEquivAlgOfEq_coe_eq_factor, RingHom.quotientKerEquivOfSurjective_symm_comp, factorₐ_apply_mk, instIsPrimeQuotientMapRingHomAlgebraMapMkOfLiesOver, AdjoinRoot.quotEquivQuotMap_symm_apply_mk, IsLocalRing.basisQuotient_repr, algebraMap_quotient_of_ramificationIdx_neZero, AlgEquiv.quotientBot_mk, RingEquiv.quotientBot_symm_mk, Ideal.quotEquivOfEq_mk, Ideal.injective_quotient_le_comap_map, algebraMap_quotient_map_quotient, Perfection.mk_teichmuller, PreTilt.mk_comp_untilt_eq_coeff_zero, DoubleQuot.quotQuotEquivComm_comp_quotQuotMk, Algebra.PreSubmersivePresentation.ofHasCoeffs_σ', Algebra.Presentation.quotientEquiv_symm, DoubleQuot.quotQuotEquivComm_quotQuotMk, Polynomial.Monic.quotient_isIntegral, exists_inv, WittVector.mk_pow_fontaineTheta, Ideal.ker_Pi_Quotient_mk, Algebra.Generators.naive_val, factorₐ_apply, Ideal.powQuotSuccInclusion_apply_coe, IsAdicComplete.StrictMono.factorPow_comp_eq_of_factorPow_comp_succ_eq', PowerBasis.quotientEquivQuotientMinpolyMap_apply_mk, Module.IsTorsionBySet.mk_smul, IsAdicComplete.StrictMono.mk_comp_liftRingHom, DoubleQuot.quotQuotToQuotSupₐ_toRingHom, Algebra.Generators.compLocalizationAwayAlgHom_X_inl, lift_surjective_of_surjective, Submodule.factor_eq_factor, factorₐ_refl, IsLocalization.AtPrime.equivQuotientMapOfIsMaximal_symm_apply_mk, Ideal.kerLiftAlg_injective, Polynomial.modByMonic_eq_zero_iff_quotient_eq_zero, AdicCompletion.mkₐ_apply_coe, StandardEtalePair.equivMvPolynomialQuotient_symm_apply, Ideal.map_mk_comap_factorPow, span_singleton_one, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk, Ideal.map_mk_eq_bot_of_le, IsLocalRing.residue_def, Polynomial.Monic.quotient_isIntegralElem, Algebra.FormallySmooth.comp_lift, RingQuot.idealQuotientToRingQuot_apply, Ideal.height_le_height_add_of_liesOver, Ideal.height_le_height_add_one_of_mem, mkₐ_toRingHom, RingEquiv.quotientBot_mk, KaehlerDifferential.End_equiv_aux, Algebra.PreSubmersivePresentation.ofHasCoeffs_algebra_algebraMap_apply, MvPolynomial.quotient_map_C_eq_zero, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk, Ideal.comp_quotientMap_eq_of_comp_eq, eq_zero_iff_dvd, Module.Quotient.mk_smul_mk, Algebra.FormallySmooth.exists_mkₐ_comp_eq_of_isAdicComplete, liftOfDerivationToSquareZero_mk_apply, isDomain_iff_prime, Ideal.quotientEquiv_symm_mk, Perfection.mk_comp_teichmuller', isStronglyTranscendental_mk_radical_conductor, mk_singleton_self, IsLocalization.Away.mvPolynomialQuotientEquiv_apply, Ideal.quotientToQuotientRangePowQuotSucc_mk, Ideal.quotientKerAlgEquivOfRightInverse_symm_apply, PowerSeries.IsWeierstrassDivisorAt.mod'_mk_eq_mod, Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom, DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMkₐ, mk_bijective_iff_eq_bot, Algebra.FormallySmooth.mk_lift, RingHom.lift_injective_of_ker_le_ideal, Ideal.mem_quotient_iff_mem, QuotientRing.isOpenMap_coe, AdicCompletion.factorₐ_evalₐ_one, TensorProduct.tensorQuotEquivQuotSMul_tmul_mk, QuotientRing.isQuotientMap_coe_coe, Ideal.quotientKerAlgEquivOfRightInverse_apply, Perfection.coeff_quotientMulEquiv, mk_span_range, Polynomial.quotientSpanXSubCAlgEquiv_mk, DoubleQuot.ker_quotQuotMk, AdicCompletion.mk_ofAlgEquiv_symm, AdicCompletion.mk_smul_mk, DoubleQuot.coe_quotQuotEquivQuotSupₐ, Ideal.quotientMulEquivQuotientProd_snd, Ideal.isPrime_map_quotientMk_of_isPrime, algebraMap_mk, stabilizerHom_apply, AdjoinRoot.quotMapOfEquivQuotMapCMapMk_symm_mk, torsionBy_eq_span_singleton, ModP.preVal_mk, Ideal.map_quotient_self, tensorKaehlerQuotKerSqEquiv_symm_tmul_D, Ideal.mk_mem_cotangentIdeal, Int.quotientSpanEquivZMod_comp_castRingHom, MvPolynomial.mk_eq_eval₂, isUnit_mk_pow_iff_isUnit_mk, Ideal.quotientMap_mk, quotAdjoinEquivQuotMap_apply_mk, lift_mk, Ideal.quotientToQuotientRangePowQuotSucc_surjective, WittVector.ker_map_le_ker_mk_comp_ghostComponent, Algebra.FormallyUnramified.comp_injective, WittVector.fontaineThetaModPPow_teichmuller, factor_surjective, RingTheory.Sequence.isWeaklyRegular_append_iff', Valuation.supp_quot, Ideal.kerLiftAlg_toRingHom, DoubleQuot.coe_quotQuotEquivQuotSupₐ_symm, MvPolynomial.mkₐ_eq_aeval, eq_zero_iff_mem, tensorKaehlerQuotKerSqEquiv_tmul_D, derivationToSquareZeroEquivLift_symm_apply_apply_coe, WittVector.ghostComponentModPPow_teichmuller_coeff, algEquivOfEqComap_apply, Ideal.quotEquivOfEq_eq_factor, Ideal.quotientKerAlgEquivOfSurjective_apply, DoubleQuot.quotQuotMkₐ_toRingHom, Ideal.ker_quotient_lift, Polynomial.quotient_mk_comp_C_isIntegral_of_isJacobsonRing, algebraMap_quotient_pow_ramificationIdx, RingHom.prod_bijective_of_isIdempotentElem, DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mkₐ, RingHom.quotientKerEquivOfRightInverse.Symm.apply, IsLocalization.AtPrime.equivQuotMaximalIdeal_apply_mk, AdicCompletion.Ideal.mk_eq_mk, AdjoinRoot.quotEquivQuotMap_apply_mk, Ideal.comap_map_quotientMk, Algebra.FormallySmooth.exists_lift, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_tmul, Ideal.minimalPrimes_eq_comap, Submodule.torsionBy.mk_ideal_smul, mkₐ_ker, mk_surjective, eq, Ideal.quotientEquivAlgOfEq_mk, RingHom.quotientKerEquivOfSurjective_apply_mk, Perfection.mk_comp_teichmuller, Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul, Ideal.injective_lift_iff, factor_ker, AlgebraicGeometry.Scheme.IdealSheafData.isLocalization_away, DoubleQuot.ker_quotLeftToQuotSup, Algebra.FormallySmooth.comp_surjective, IsAdicComplete.mk_liftAlgHom, Algebra.FormallyEtale.iff_comp_bijective, Ideal.quotientEquiv_apply, AdjoinRoot.Polynomial.quotQuotEquivComm_mk, Ideal.quotientInfEquivQuotientProd_snd, IsAdicComplete.mkₐ_comp_liftAlgHom, Ring.DirectLimit.quotientMk_of, IsSemiprimaryRing.isSemisimpleRing, Ideal.comap_map_mk, DoubleQuot.coe_quotQuotEquivQuotOfLEₐ, Ideal.quotientToQuotientRangePowQuotSucc_injective, ringHom_ext_iff, RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply, RingHom.kerLift_injective, isDomain, MvPolynomial.quotientEquivQuotientMvPolynomial_leftInverse, AdicCompletion.evalOneₐ_of, IsFractionRing.stabilizerHom_apply_apply_mk, mk_out, instIsArtinianRingQuotientIdeal, Algebra.trace_quotient_mk, Ideal.polynomialQuotientEquivQuotientPolynomial_symm_mk, Polynomial.IsDistinguishedAt.algEquivQuotient_symm_apply, MvPolynomial.quotient_mk_comp_C_injective, AdicCompletion.mk_smul_top_ofAlgEquiv_symm, Ideal.quotientMap_injective', IsAdicComplete.mk_liftRingHom, Algebra.TensorProduct.tensorQuotientEquiv_symm_apply_tmul, Ideal.quotientEquivAlg_symm, Algebra.TensorProduct.quotIdealMapEquivTensorQuot_symm_tmul, IsLocalRing.quotient_span_eq_top_iff_span_eq_top, DividedPowers.Quotient.isDPMorphism, Ideal.quotientMulEquivQuotientProd_fst, DoubleQuot.quotQuotEquivQuotOfLEₐ_comp_mkₐ, Ideal.rank_pow_quot_aux, mkₐ_eq_mk, Ideal.rootsOfUnityMapQuot_apply, StandardEtalePresentation.toPresentation_σ', Module.IsTorsionBySet.isScalarTower, AlgEquiv.prodQuotientOfIsIdempotentElem_apply_snd, Ideal.rank_pow_quot, AdicCompletion.mk_ofAlgEquiv_symm_eq_evalOneₐ, Ideal.map_height_le_one_of_mem_minimalPrimes, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk, DoubleQuot.quotQuotEquivQuotSup_quotQuotMk, Module.IsTorsionBySet.isSemisimpleModule_iff, Ideal.quotientKerAlgEquivOfSurjective_symm_apply, Ideal.quotientKerAlgEquivOfSurjective_mk, Ideal.mem_quotient_iff_mem_sup, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk_symm_quotQuotMk, DoubleQuot.quotQuotEquivCommₐ_toRingEquiv, DoubleQuot.coe_quotQuotToQuotSupₐ, norm_mk_lt, AlgEquiv.quotientBot_symm_mk, IsLocalRing.basisQuotient_apply, IsPrimitiveRoot.idealQuotient_mk, isUnit_mk_pow_iff_notMem, trace_quotient_eq_trace_localization_quotient, mk_eq_mk_iff_sub_mem, Ideal.quotientEquiv_mk, Ideal.quotientMap_surjective, Ideal.ker_quotientMap_mk, AdjoinRoot.Polynomial.quotQuotEquivComm_symm_mk_mk, Ideal.powQuotSuccInclusion_injective, DoubleQuot.quotQuotEquivQuotSupₐ_toRingEquiv, Algebra.trace_quotient_eq_of_isDedekindDomain, Ideal.quotient_map_comp_mkₐ, StandardEtalePair.aeval_X_g_mul_mk_X, AdicCompletion.transitionMap_ideal_mk, Algebra.Presentation.tensorModelOfHasCoeffsEquiv_symm_tmul, smulCommClass', AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk_mk, Ideal.quotientInfToPiQuotient_mk', AlgEquiv.prodQuotientOfIsIdempotentElem_apply_fst, mk_eq_mk, Ideal.quotEquivOfEq_symm, Perfection.mk_teichmuller₀, instRingHomSurjectiveQuotientMk, Algebra.TensorProduct.quotIdealMapEquivTensorQuot_mk, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, isLocalHom_of_le_jacobson_bot, Ideal.quotientInfToPiQuotient_mk, derivationToSquareZeroEquivLift_apply_coe_apply, AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_mk, liftOfDerivationToSquareZero_mk_apply', Ideal.quotientInfEquivQuotientProd_fst, Ideal.quotientMap_algebraMap, DoubleQuot.quotQuotEquivQuotOfLEₐ_toRingEquiv, Algebra.FormallyUnramified.iff_comp_injective, WittVector.quotEquivOfEq_ghostComponentModPPow, AdicCompletion.evalₐ_of, StandardEtalePresentation.toPresentation_val, Ideal.height_le_height_add_encard_of_subset, DividedPowers.Quotient.dpow_apply, Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero, mk_eq_one_iff_sub_mem, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk, Ideal.quotientMap_injective, AdicCompletion.factor_evalₐ_eq_eval, isStronglyTranscendental_mk_of_mem_minimalPrimes, Ideal.cotangentEquivIdeal_symm_apply, smulCommClass, RingHom.quotientKerEquivOfRightInverse.apply, liftₐ_apply, PowerSeries.IsWeierstrassDivisorAt.mk_mod'_eq_self, idealFactorsFunOfQuotHom_coe_coe, AdicCompletion.evalₐ_mk, DoubleQuot.quotQuotEquivComm_comp_quotQuotMkₐ, Ideal.KerLift.map_smul, IsLocalization.AtPrime.equivQuotientMapMaximalIdeal_apply_mk, DoubleQuot.quotQuotEquivComm_mk_mk, AlgHom.IsArithFrobAt.restrict_mk, AdicCompletion.evalₐ_mkₐ, Algebra.Presentation.quotientEquiv_mk, isSemiprimaryRing_iff, DoubleQuot.quotQuotEquivQuotOfLE_symm_comp_mk, quotient_ring_saturate, DoubleQuot.quotQuotEquivQuotSup_symm_quotQuotMk, factorₐ_comp, Ideal.mk_ker, Ideal.height_le_height_add_spanFinrank_of_le, Submodule.torsionBySet.mk_smul, factor_comp, Algebra.TensorProduct.tensorQuotientEquiv_apply_tmul, mk_comp_algebraMap, DoubleQuot.coe_quotQuotEquivCommₐ, Algebra.PreSubmersivePresentation.ofHasCoeffs_val, Ideal.polynomialQuotientEquivQuotientPolynomial_map_mk, IsDedekindDomain.exists_representative_mod_finset, MvPolynomial.quotientEquivQuotientMvPolynomial_rightInverse, DoubleQuot.quotQuotEquivQuotSup_quot_quot_algebraMap, IsLocalization.AtPrime.equivQuotMaximalIdeal_symm_apply_mk, Ideal.quotient_mk_maps_eq, DoubleQuot.quotQuotEquivQuotOfLE_symm_mk, isIntegral_quotientMap_iff, lift_comp_mk, SModEq.idealQuotientMk, PreTilt.mk_untilt_eq_coeff_zero, eq_factor_of_eq_factor_succ, AlgHom.kerSquareLift_mk, factor_eq, WittVector.mk_fontaineTheta, IsNilpotent.isUnit_quotient_mk_iff, IsAdicComplete.mk_comp_liftRingHom, norm_mk_le, Ideal.quotientToQuotientRangePowQuotSuccAux_mk, Ideal.bot_quotient_isMaximal_iff, Ideal.Factors.piQuotientEquiv_mk, Ideal.quotient_map_mkₐ, RingHom.kerLift_mk, Perfection.teichmuller₀_mapMonoidHom_idealQuotientMk, QuotientRing.isOpenQuotientMap_mk, Ideal.quotientEquivAlgOfEq_symm, DoubleQuot.quotQuotEquivQuotSupₐ_symm_toRingEquiv, isScalarTower_right, Polynomial.IsDistinguishedAt.algEquivQuotient_apply, liftₐ_comp, mk_smul_mk_quotient_map_quotient, AddValuation.supp_quot, mkₐ_surjective, IsDedekindDomain.quotientEquivPiFactors_mk, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of, Ring.jacobson_quotient_jacobson, Module.IsTorsionBy.mk_smul, RingTheory.Sequence.isRegular_cons_iff', ValuationSubring.coe_unitGroupToResidueFieldUnits_apply, DoubleQuot.coe_liftSupQuotQuotMkₐ, AdicCompletion.evalOneₐ_liftAlgHom, DoubleQuot.quotQuotEquivQuotOfLE_comp_quotQuotMk, Algebra.FormallyEtale.comp_bijective, Int.quotientSpanNatEquivZMod_comp_castRingHom, Submodule.torsionBy.mk_smul, WittVector.ghostComponentModPPow_map_mk, Algebra.FormallySmooth.iff_comp_surjective, Ideal.kerLiftAlg_mk, Ideal.pi_quotient_surjective, DoubleQuot.quotQuotEquivQuotOfLE_quotQuotMk, DoubleQuot.quotQuotEquivComm_symm, Ideal.Factors.piQuotientEquiv_map, TensorProduct.quotTensorEquivQuotSMul_mk_tmul, derivationQuotKerSq_mk, noZeroDivisors, Ideal.eq_zero_of_polynomial_mem_map_range, DoubleQuot.quotQuotEquivComm_algebraMap, mk_algebraMap, Algebra.FormallyUnramified.iff_comp_injective_of_small, algebraMap_mk_of_liesOver, RingQuot.ringQuotToIdealQuotient_apply, Algebra.Presentation.tensorModelOfHasCoeffsInv_aeval_val, KummerDedekind.quotMapEquivQuotQuotMap_symm_apply

Mathlib.Tactic.RingNF

Definitions

Name	Category	Theorems
ring 📖	CompOp	—

MonoidAlgebra

Definitions

Name	Category	Theorems
ring 📖	CompOp	14 math math: Representation.IsIrreducible.instIsSimpleModuleMonoidAlgebraAsModule, Rep.instIsEquivalenceModuleCatMonoidAlgebraOfModuleMonoidAlgebra, Rep.instIsEquivalenceModuleCatMonoidAlgebraToModuleMonoidAlgebra, Rep.ofModuleMonoidAlgebra_obj_coe, Representation.isSemisimpleRepresentation_iff_isSemisimpleModule_asModule, Representation.isSimpleModule_iff_irreducible_ofModule, Rep.ofModuleMonoidAlgebra_obj_ρ, RootPairing.isSimpleModule_weylGroupRootRep, RootPairing.isSimpleModule_weylGroupRootRep_iff, Rep.unit_iso_comm, Submodule.instIsSemisimpleModule, Representation.irreducible_iff_isSimpleModule_asModule, Representation.is_simple_module_iff_irreducible_ofModule, Representation.isSemisimpleModule_iff_isSemisimpleRepresentation_ofModule

Pi

Definitions

Name	Category	Theorems
ring 📖	CompOp	12 math math: Function.update_exp, spectrum_eq, LieRing.lie_apply, Matrix.exp_diagonal, CFC.rpow_eq_rpow_pi, instIsSemisimpleRingForallOfFinite, Matrix.exp_blockDiagonal, cfc_map_pi, CFC.rpow_map_pi, Matrix.exp_blockDiagonal', exp_def, coe_exp

Polynomial

Definitions

Name	Category	Theorems
ring 📖	CompOp	122 math math: PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_apply, PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply, Sequence.span_degreeLE, transcendental, Sequence.basis_natDegree_strictMono, Monic.free_quotient, StandardEtalePair.inv_aeval_X_g, Differential.implicitDeriv_C, AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_symm_mk, Sequence.span, fiberEquivQuotient_tmul, cyclotomic_dvd_geom_sum_of_dvd, descPochhammer_succ_comp_X_sub_one, AdjoinRoot.quotMapOfEquivQuotMapCMapMk_mk, Sequence.basis_eq_self, StandardEtalePresentation.toPresentation_algebra_smul, Ideal.quotient_map_C_eq_zero, RatFunc.mk_smul, WeierstrassCurve.Affine.Y_sub_negPolynomial, finrank_quotient_span_eq_natDegree', notMem_map_range, Ideal.jacobson_bot_polynomial_le_sInf_map_maximal, WeierstrassCurve.Affine.C_addPolynomial, instIsAlgebraicPolynomialOfNoZeroDivisors_1, AdjoinRoot.quotEquivQuotMap_symm_apply_mk, AdjoinRoot.evalEval_apply, instIsIntegralPolynomial, evalEval_intCast, Transcendental.of_aeval, Ideal.injective_quotient_le_comap_map, Monic.quotient_isIntegral, PowerBasis.quotientEquivQuotientMinpolyMap_apply_mk, WeierstrassCurve.φ_three, RatFunc.mk_def, RatFunc.mk_eq_div', RatFunc.ofFractionRing_div, mem_span_C_X_sub_C_X_sub_C_iff_eval_eval_eq_zero, modByMonic_eq_zero_iff_quotient_eq_zero, MvPolynomial.transcendental_polynomial_aeval_X_iff, StandardEtalePair.equivMvPolynomialQuotient_symm_apply, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk, Monic.quotient_isIntegralElem, WeierstrassCurve.Affine.CoordinateRing.C_addPolynomial, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_add_eq, transcendental_X, finrank_quotient_span_eq_natDegree, WeierstrassCurve.Ψ_neg, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_symm_quotQuotMk, Differential.coeff_mapCoeffs, adjSylvester_comp_sylveserMap, WeierstrassCurve.Affine.C_addPolynomial_slope, transcendental_aeval_iff, quotientSpanXSubCAlgEquiv_mk, det_taylorLinearEquiv_toLinearMap, WeierstrassCurve.C_Ψ₂Sq, evalEval_sub, AdjoinRoot.quotMapOfEquivQuotMapCMapMk_symm_mk, Differential.mapCoeffs_monomial, WeierstrassCurve.ψ_even, Differential.mapCoeffs_C, RatFunc.div_smul, WeierstrassCurve.Affine.Y_sub_polynomialY, Differential.deriv_aeval_eq_implicitDeriv, RatFunc.instIsScalarTowerPolynomial, quotient_mk_comp_C_isIntegral_of_isJacobsonRing, instIsAlgebraicPolynomialOfNoZeroDivisors, AdjoinRoot.quotEquivQuotMap_apply_mk, Differential.mapCoeffs_X, Monic.finite_quotient, Bivariate.pderiv_zero_equivMvPolynomial, AdjoinRoot.Polynomial.quotQuotEquivComm_mk, RatFunc.ofFractionRing_sub, WeierstrassCurve.ψ_odd, WeierstrassCurve.Ψ_even, RatFunc.ofFractionRing_neg, RingOfIntegers.ZModXQuotSpanEquivQuotSpan_mk_apply, Bivariate.Polynomial.Bivariate.pderiv_zero_equivMvPolynomial, mem_closure_X_union_C, Ideal.polynomialQuotientEquivQuotientPolynomial_symm_mk, IsDistinguishedAt.algEquivQuotient_symm_apply, WeierstrassCurve.ψ_neg, mem_map_range, StandardEtalePresentation.toPresentation_σ', evalEval_neg, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_symm_mk_mk, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk_symm_quotQuotMk, Differential.deriv_aeval_eq, AdjoinRoot.Polynomial.quotQuotEquivComm_symm_mk_mk, det_taylorLinearEquiv, WeierstrassCurve.Affine.CoordinateRing.coe_norm_smul_basis, StandardEtalePair.aeval_X_g_mul_mk_X, isIntegral_iff_isIntegral_coeff, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk_mk, RatFunc.neg_def, lifts_iff_liftsRing, Ideal.jacobson_bot_polynomial_of_jacobson_bot, StandardEtalePresentation.toPresentation_algebra_algebraMap_apply, AdjoinRoot.quotMapOfEquivQuotMapCMapSpanMk_mk, sum_modByMonic_coeff, StandardEtalePresentation.toPresentation_val, Differential.implicitDeriv_X, AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapSpanMk_mk, WeierstrassCurve.φ_four, RatFunc.sub_def, cyclotomic_prime, RatFunc.div_def, WeierstrassCurve.φ_two, MvPolynomial.transcendental_supported_polynomial_aeval_X_iff, StandardEtalePresentation.toPresentation_relation, Ideal.polynomialQuotientEquivQuotientPolynomial_map_mk, Sequence.linearIndependent, Ideal.quotient_mk_maps_eq, instFiniteDimensionalQuotientPolynomialIdealSpanSingletonSetSmithCoeffs, Sequence.basis_degree_strictMono, sylveserMap_comp_adjSylvester, IsDistinguishedAt.algEquivQuotient_apply, Sequence.span_degreeLT, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of, WeierstrassCurve.Ψ_odd, Ideal.eq_zero_of_polynomial_mem_map_range, isIntegral_isLocalization_polynomial_quotient, KummerDedekind.quotMapEquivQuotQuotMap_symm_apply

PreLp

Definitions

Name	Category	Theorems
ring 📖	CompOp	—

RingCat

Definitions

Name	Category	Theorems
ring 📖	CompOp	183 math math: PresheafOfModules.Monoidal.tensorObj_obj, PresheafOfModules.Sheafify.app_eq_of_isLocallyInjective, CommRingCat.forget₂Ring_preservesLimitsOfSize, AlgebraicGeometry.StructureSheaf.instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf, CommRingCat.instFullRingCatForget₂RingHomCarrierCarrier, PresheafOfModules.ofPresheaf_obj_isModule, FilteredColimits.instPreservesFilteredColimitsAddCommGrpCatForget₂RingHomCarrierAddMonoidHomCarrier, PresheafOfModules.add_app, PresheafOfModules.Sheafify.add_smul, PresheafOfModules.restrictScalars_map_app, PresheafOfModules.epi_iff_surjective, PresheafOfModules.evaluation_preservesColimitsOfShape, PresheafOfModules.comp_app, SheafOfModules.evaluationPreservesLimit, Colimits.cocone_naturality_components, SheafOfModules.forgetToSheafModuleCat_map_hom, PresheafOfModules.pushforward_map_app_apply, PresheafOfModules.limitPresheafOfModules_map, PresheafOfModules.sections_property, forget₂AddCommGroup_preservesLimits, PresheafOfModules.toSheafify_app_apply', PresheafOfModules.instPreservesLimitsOfShapeModuleCatCarrierObjOppositeRingCatEvaluation, PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct, PresheafOfModules.Derivation.d_map, PresheafOfModules.free_map_app, forget₂_map, PresheafOfModules.congr_map_apply, hom_comp, PresheafOfModules.freeYonedaEquiv_symm_app, PresheafOfModules.restrictScalarsObj_map, PresheafOfModules.forgetToPresheafModuleCatObj_map, inv_hom_apply, SheafOfModules.evaluationPreservesLimitsOfShape, PresheafOfModules.pushforward₀_obj_obj_carrier, PresheafOfModules.id_app, PresheafOfModules.restrictScalarsObj_obj, PresheafOfModules.Derivation.postcomp_d_apply, forget_map_apply, PresheafOfModules.Derivation.d_one, PresheafOfModules.sectionsMap_coe, PresheafOfModules.Sheafify.map_smul_eq, PresheafOfModules.map_comp_apply, PresheafOfModules.pushforward_map_app_apply', PresheafOfModules.Derivation.d_mul, SheafOfModules.evaluationPreservesLimitsOfSize, PresheafOfModules.unit_map_one, PresheafOfModules.zsmul_app, PresheafOfModules.toPresheaf_obj_coe, AlgCat.forget₂Ring_preservesLimitsOfSize, PresheafOfModules.isoMk_hom_app, PresheafOfModules.map_smul, PresheafOfModules.Monoidal.tensorObj_map_tmul, PresheafOfModules.instPreservesLimitsOfSizeModuleCatCarrierObjOppositeRingCatEvaluation, of_carrier, SheafOfModules.pushforwardComp_inv_app_val_app, forget₂SemiRing_preservesLimitsOfSize, PresheafOfModules.pushforward₀_obj_obj_isAddCommGroup, PresheafOfModules.mono_iff_surjective, PresheafOfModules.freeObj_map, SheafOfModules.instSmallElemForallObjCompModuleCatCarrierOppositeRingCatObjFunctorIsSheafPresheafOfModulesForgetEvaluationForgetLinearMapIdCarrierSections, PresheafOfModules.limitCone_π_app_app, PresheafOfModules.instEpiModuleCatCarrierObjOppositeRingCatApp, PresheafOfModules.presheaf_map_apply_coe, PresheafOfModules.Derivation.congr_d, PresheafOfModules.forgetToPresheafModuleCatObjMap_apply, SheafOfModules.pushforwardCongr_hom_app_val_app, FilteredColimits.forget_preservesFilteredColimits, CategoryTheory.Iso.ringCatIsoToRingEquiv_toRingHom, PresheafOfModules.toFreeYonedaCoproduct_fromFreeYonedaCoproduct_assoc, PresheafOfModules.surjective_of_epi, PresheafOfModules.injective_of_mono, PresheafOfModules.isoMk_inv_app, PresheafOfModules.pushforward_obj_map_apply, forget_preservesLimitsOfSize, PresheafOfModules.forgetToPresheafModuleCatObjObj_coe, ofHom_apply, PresheafOfModules.unitHomEquiv_apply_coe, PresheafOfModules.freeObj_obj, SheafOfModules.pushforwardCongr_inv_app_val_app, CommRingCat.forgetToRingCat_obj, moduleCatRestrictScalarsPseudofunctor_mapId, PresheafOfModules.freeAdjunctionUnit_app, SheafOfModules.pushforwardPushforwardAdj_unit_app_val_app, PresheafOfModules.evaluation_preservesLimit, PresheafOfModules.presheaf_obj_coe, PresheafOfModules.homMk_app, PresheafOfModules.toPresheaf_map_app_apply, PresheafOfModules.Derivation'.d_app, PresheafOfModules.neg_app, PresheafOfModules.map_comp, moduleCatRestrictScalarsPseudofunctor_map, PresheafOfModules.evaluation_preservesColimitsOfSize, SheafOfModules.pushforwardComp_hom_app_val_app, PresheafOfModules.evaluation_preservesFiniteLimits, SheafOfModules.Presentation.map_relations_I, PresheafOfModules.sub_app, PresheafOfModules.colimitPresheafOfModules_map, PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map_d, PresheafOfModules.Elements.fromFreeYoneda_app_apply, PresheafOfModules.pushforward_obj_obj, SheafOfModules.Presentation.mapRelations_mapGenerators, SheafOfModules.relationsOfIsCokernelFree_I, CommRingCat.forget₂Ring_preservesLimits, forgetReflectIsos, PresheafOfModules.instAdditiveModuleCatCarrierObjOppositeRingCatEvaluation, PresheafOfModules.Hom.naturality_assoc, PresheafOfModules.ofPresheaf_obj_carrier, CommRingCat.FilteredColimits.forget₂Ring_preservesFilteredColimits, PresheafOfModules.restriction_app, PresheafOfModules.ι_fromFreeYonedaCoproduct_apply, PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_obj, PresheafOfModules.Derivation.d_app, PresheafOfModules.forgetToPresheafModuleCat_obj, SheafOfModules.unitToPushforwardObjUnit_val_app_apply, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓUnitOpensCarrierCarrierCommRingCatRingCatSheaf, PresheafOfModules.forgetToPresheafModuleCatObj_obj, PresheafOfModules.Monoidal.tensorHom_app, instFullSemiRingCatForget₂RingHomCarrierCarrier, PresheafOfModules.DifferentialsConstruction.relativeDifferentials'_map, moduleCatRestrictScalarsPseudofunctor_obj, PresheafOfModules.instMonoModuleCatCarrierObjOppositeRingCatApp, PresheafOfModules.Derivation'.app_apply, AlgebraicGeometry.StructureSheaf.instIsLocalizedModuleCarrierStalkAbPresheafOpensCarrierTopModuleStructurePresheafPrimeComplAsIdealToStalkₗ, SheafOfModules.Presentation.mapRelations_mapGenerators_assoc, hom_id, moduleCatRestrictScalarsPseudofunctor_mapComp, PresheafOfModules.instHasLimitModuleCatCarrierObjOppositeRingCatCompEvaluationRestrictScalarsHomMap, forget₂SemiRing_preservesLimits, CategoryTheory.Limits.IsColimit.ι_smul, comp_apply, SheafOfModules.pushforwardNatTrans_app_val_app, PresheafOfModules.Sheafify.one_smul, forget₂AddCommGroup_preservesLimitsOfSize, PresheafOfModules.instHasColimitModuleCatCarrierObjOppositeRingCatCompEvaluationRestrictScalarsHomMap, PresheafOfModules.map_id, ofHom_hom, SheafOfModules.pushforwardPushforwardEquivalence_unit_app_val_app, SheafOfModules.relationsOfIsCokernelFree_s, SheafOfModules.forgetToSheafModuleCat_obj_obj, PresheafOfModules.pushforward_obj_map_apply', PresheafOfModules.Hom.naturality, AlgCat.forget₂Ring_preservesLimits, forget_preservesLimits, PresheafOfModules.HasDifferentials.exists_universal_derivation, SheafOfModules.pushforwardPushforwardAdj_counit_app_val_app, CategoryTheory.Presieve.FamilyOfElements.isCompatible_map_smul_aux, PresheafOfModules.freeYonedaEquiv_comp, PresheafOfModules.Sheafify.zero_smul, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, SheafOfModules.Presentation.IsFinite.finite_relations, SheafOfModules.pushforwardNatTrans_app_val_app_apply, PresheafOfModules.colimitCocone_ι_app_app, PresheafOfModules.colimitPresheafOfModules_obj, PresheafOfModules.Finite.evaluation_preservesFiniteColimits, PresheafOfModules.limitPresheafOfModules_obj, hom_inv_apply, PresheafOfModules.ofPresheaf_map, CommRingCat.forgetToRingCat_map_hom, PresheafOfModules.germ_ringCat_smul, PresheafOfModules.naturality_apply, PresheafOfModules.fromFreeYonedaCoproduct_app_mk, PresheafOfModules.Sheafify.map_smul, PresheafOfModules.germ_smul, PresheafOfModules.toSheafify_app_apply, PresheafOfModules.pushforward₀_obj_obj_isModule, id_apply, PresheafOfModules.evaluation_obj, forget_obj, FilteredColimits.forget₂SemiRing_preservesFilteredColimits, PresheafOfModules.ofPresheaf_obj_isAddCommGroup, SheafOfModules.pushforwardPushforwardEquivalence_counit_app_val_app, PresheafOfModules.evaluation_map, PresheafOfModules.freeObjDesc_app, PresheafOfModules.Sheafify.mul_smul, AlgebraicGeometry.instIsIsoModulesSpecOfCarrierFromTildeΓFreeOpensCarrierCarrierCommRingCat, PresheafOfModules.zero_app, PresheafOfModules.map_comp_assoc, PresheafOfModules.Sheafify.SMulCandidate.h, PresheafOfModules.evaluation_preservesColimit, PresheafOfModules.forgetToPresheafModuleCat_map, SheafOfModules.Finite.evaluationPreservesFiniteLimits, forget_map, SheafOfModules.unitHomEquiv_apply_coe

TrivSqZeroExt

Definitions

Name	Category	Theorems
ring 📖	CompOp	14 math math: exp_inr, fst_exp, hasSum_snd_expSeries_of_smul_comm, fst_expSeries, eq_smul_exp_of_ne_zero, snd_exp, DualNumber.exp_eps, exp_def, hasSum_expSeries_of_smul_comm, exp_inl, DualNumber.exp_smul_eps, exp_def_of_smul_comm, snd_expSeries_of_smul_comm, eq_smul_exp_of_invertible

ULift

Definitions

Name	Category	Theorems
ring 📖	CompOp	—

UniformSpace.Completion

Definitions

Name	Category	Theorems
ring 📖	CompOp	50 math math: mapRingHom_id, Padic.withValUniformEquiv_norm_le_one_iff, Valued.valuedCompletion_surjective_iff, Isometry.extensionHom_coe, PadicComplex.valuation_extends, PadicComplex.charZero, NumberField.instIsRankOneDiscreteWithZeroMultiplicativeIntAdicCompletionV, IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, NumberField.HeightOneSpectrum.rankOne_hom'_def, Valuation.IsEquiv.valuedCompletion_le_one_iff, PadicComplex.coe_natCast, extensionHom_coe, Valued.exists_coe_eq_v, mapRingHom_apply, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, FunctionField.valuedFqtInfty.def, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', PadicComplex.valuation_p, continuous_coeRingHom, Valued.closure_coe_completion_v_lt, algebraMap_def, Valued.closure_coe_completion_v_mul_v_lt, Valued.valuedCompletion_apply, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, AbsoluteValue.Completion.isClosedEmbedding_extensionEmbedding_of_comp, AbsoluteValue.Completion.isometry_extensionEmbedding_of_comp, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective, Isometry.isometry_mapRingHom, Valued.extensionValuation_apply_coe, mapRingHom_coe, PadicComplex.RankOne.hom_eq_embedding, LaurentSeries.valuation_compare, LaurentSeries.tendsto_valuation, coe_mapRingHom, IsDedekindDomain.HeightOneSpectrum.adicCompletion_valueGroup_eq, LaurentSeries.comparePkg_eq_extension, instNonarchimedeanRingCompletion, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, mapRingHom_comp, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, AbsoluteValue.Completion.extensionEmbedding_dist_eq_of_comp, AbsoluteValue.Completion.extensionEmbedding_of_comp_coe, Isometry.mapRingHom_coe, PadicComplexInt.integers, NumberField.FinitePlace.norm_def, topologicalRing, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers, Valued.extensionValuation_toFun

---

← Back to Index