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, ring, ring	24
Theorems	0
Total	24

AddMonoidAlgebra

Definitions

Name	Category	Theorems
ring 📖	CompOp	9 math math: Polynomial.toFinsupp_zsmul, Polynomial.ofFinsupp_sub, toDirectSum_intCast, MonoidAlgebra.Submodule.instIsSemisimpleRingAddMonoidAlgebra, DirectSum.toAddMonoidAlgebra_intCast, Polynomial.toFinsupp_sub, Polynomial.ofFinsupp_zsmul, Polynomial.toFinsupp_intCast, Polynomial.ofFinsupp_intCast

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	27 math math: mulLeftRight_isBoundedBilinear, DoubleCentralizer.intCast_snd, intCast_apply, CStarMatrix.norm_def', mulLeftRight_apply, CStarMatrix.toCLMNonUnitalAlgHom_eq_toCLM, hasFDerivAt_ringInverse, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe, fderiv_inverse, fderivWithin_inv', LinearMap.IsSymmetric.coe_toSelfAdjoint, NonUnitalAlgHom.coe_Lmul, LinearMap.IsSymmetric.toSelfAdjoint_apply, opNorm_mulLeftRight_apply_le, PositiveLinearMap.gnsStarAlgHom_apply, hasStrictFDerivAt_ringInverse, opNorm_mulLeftRight_apply_apply_le, IsPositive.spectrumRestricts, DoubleCentralizer.natCast_toProd, hasStrictFDerivAt_inv', opNorm_mulLeftRight_le, DoubleCentralizer.intCast_fst, VonNeumannAlgebra.instSubringClass, hasFDerivAt_inv', DoubleCentralizer.intCast_toProd, PositiveLinearMap.gnsNonUnitalStarAlgHom_apply, 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	36 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.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	373 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, Int.quotientSpanEquivZMod_comp_Quotient_mk, StandardEtalePair.inv_aeval_X_g, IsLocalization.AtPrime.equivQuotientMapOfIsMaximal_apply_mk, RingTheory.Sequence.isWeaklyRegular_cons_iff', Ideal.quotientEquiv_symm_apply, 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, Int.quotientSpanNatEquivZMod_comp_Quotient_mk, StandardEtalePresentation.toPresentation_algebra_smul, Ideal.quotient_map_C_eq_zero, Polynomial.IsDistinguishedAt.map_eq_X_pow, 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, Polynomial.IsDistinguishedAt.degree_eq_coe_lift_order_map, 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, 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, PowerBasis.quotientEquivQuotientMinpolyMap_apply_mk, Module.IsTorsionBySet.mk_smul, 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, PowerSeries.IsWeierstrassDivisionAt.degree_lt, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply_mk, Ideal.map_mk_eq_bot_of_le, IsLocalRing.residue_def, Polynomial.Monic.quotient_isIntegralElem, PowerSeries.IsWeierstrassFactorizationAt.natDegree_eq_toNat_order_map_of_ne_top, 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, isStronglyTranscendental_mk_radical_conductor, mk_singleton_self, IsLocalization.Away.mvPolynomialQuotientEquiv_apply, Ideal.quotientToQuotientRangePowQuotSucc_mk, AdjoinRoot.quotEquivQuotMap_apply, 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, KummerDedekind.emultiplicity_factors_map_eq_emultiplicity, 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, 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, torsionBy_eq_span_singleton, ModP.preVal_mk, Ideal.map_quotient_self, tensorKaehlerQuotKerSqEquiv_symm_tmul_D, Ideal.mk_mem_cotangentIdeal, Int.quotientSpanEquivZMod_comp_castRingHom, 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, PowerSeries.IsWeierstrassDivisorAt.isUnit_shift, RingTheory.Sequence.isWeaklyRegular_append_iff', Valuation.supp_quot, Ideal.kerLiftAlg_toRingHom, DoubleQuot.coe_quotQuotEquivQuotSupₐ_symm, 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, PowerBasis.quotientEquivQuotientMinpolyMap_symm_apply, 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, Algebra.Presentation.tensorModelOfHasCoeffsHom_tmul, Ideal.injective_lift_iff, factor_ker, AlgebraicGeometry.Scheme.IdealSheafData.isLocalization_away, DoubleQuot.ker_quotLeftToQuotSup, Algebra.FormallySmooth.comp_surjective, Algebra.FormallyEtale.iff_comp_bijective, Ideal.quotientEquiv_apply, AdjoinRoot.Polynomial.quotQuotEquivComm_mk, Ideal.quotientInfEquivQuotientProd_snd, 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, mk_out, instIsArtinianRingQuotientIdeal, Algebra.trace_quotient_mk, Ideal.polynomialQuotientEquivQuotientPolynomial_symm_mk, Polynomial.IsDistinguishedAt.algEquivQuotient_symm_apply, MvPolynomial.quotient_mk_comp_C_injective, AlgebraicClosure.Monics.map_eq_prod, AdicCompletion.mk_smul_top_ofAlgEquiv_symm, Ideal.quotientMap_injective', 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, DoubleQuot.quotQuotEquivCommₐ_toRingEquiv, DoubleQuot.coe_quotQuotToQuotSupₐ, norm_mk_lt, AlgEquiv.quotientBot_symm_mk, IsLocalRing.basisQuotient_apply, 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', Ideal.quotientInfToPiQuotient_mk', AlgEquiv.prodQuotientOfIsIdempotentElem_apply_fst, mk_eq_mk, Ideal.quotEquivOfEq_symm, instRingHomSurjectiveQuotientMk, Algebra.TensorProduct.quotIdealMapEquivTensorQuot_mk, PrimeSpectrum.range_comap_algebraMap_localization_compl_eq_range_comap_quotientMk, 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, PowerSeries.IsWeierstrassFactorizationAt.degree_eq_coe_lift_order_map_of_ne_top, Ideal.quotientMap_algebraMap, DoubleQuot.quotQuotEquivQuotOfLEₐ_toRingEquiv, Algebra.FormallyUnramified.iff_comp_injective, WittVector.quotEquivOfEq_ghostComponentModPPow, AdicCompletion.evalₐ_of, AdjoinRoot.quotEquivQuotMap_symm_apply, PowerSeries.isWeierstrassDivisionAt_iff, 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, KummerDedekind.normalizedFactors_ideal_map_eq_normalizedFactors_min_poly_mk_map, 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, 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, PreTilt.mk_untilt_eq_coeff_zero, AlgHom.kerSquareLift_mk, factor_eq, WittVector.mk_fontaineTheta, IsNilpotent.isUnit_quotient_mk_iff, norm_mk_le, Ideal.quotientToQuotientRangePowQuotSuccAux_mk, PowerSeries.IsWeierstrassDivisorAt.seq_one, Ideal.bot_quotient_isMaximal_iff, Ideal.Factors.piQuotientEquiv_mk, Ideal.quotient_map_mkₐ, RingHom.kerLift_mk, QuotientRing.isOpenQuotientMap_mk, Ideal.quotientEquivAlgOfEq_symm, DoubleQuot.quotQuotEquivQuotSupₐ_symm_toRingEquiv, isScalarTower_right, Polynomial.IsDistinguishedAt.algEquivQuotient_apply, Ideal.eval₂_C_mk_eq_zero, 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ₐ, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, 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, Polynomial.IsDistinguishedAt.coe_natDegree_eq_order_map, Ideal.kerLiftAlg_mk, Ideal.pi_quotient_surjective, DoubleQuot.quotQuotEquivQuotOfLE_quotQuotMk, DoubleQuot.quotQuotEquivComm_symm, Ideal.Factors.piQuotientEquiv_map, TensorProduct.quotTensorEquivQuotSMul_mk_tmul, derivationQuotKerSq_mk, noZeroDivisors, DoubleQuot.quotQuotEquivComm_algebraMap, mk_algebraMap, Algebra.FormallyUnramified.iff_comp_injective_of_small, Polynomial.isIntegral_isLocalization_polynomial_quotient, 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	12 math math: Representation.IsIrreducible.instIsSimpleModuleMonoidAlgebraAsModule, 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

Perfection

Definitions

Name	Category	Theorems
ring 📖	CompOp	—

Pi

Definitions

Name	Category	Theorems
ring 📖	CompOp	14 math math: NumberField.canonicalEmbedding.mem_span_latticeBasis, Function.update_exp, spectrum_eq, NumberField.canonicalEmbedding.integerLattice.inter_ball_finite, 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	113 math math: PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_apply, PowerSeries.IsWeierstrassFactorizationAt.algEquivQuotient_symm_apply, 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, 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', 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, 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, 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, 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, IsDistinguishedAt.algEquivQuotient_apply, AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot_mk_of, WeierstrassCurve.Ψ_odd, isIntegral_isLocalization_polynomial_quotient, KummerDedekind.quotMapEquivQuotQuotMap_symm_apply

PreLp

Definitions

Name	Category	Theorems
ring 📖	CompOp	—

Ring.DirectLimit

Definitions

Name	Category	Theorems
ring 📖	CompOp	3 math math: Field.DirectLimit.exists_inv, Field.DirectLimit.mul_inv_cancel, Field.DirectLimit.inv_mul_cancel

RingCat

Definitions

Name	Category	Theorems
ring 📖	CompOp	160 math math: PresheafOfModules.Monoidal.tensorObj_obj, CommRingCat.forget₂Ring_preservesLimitsOfSize, AlgebraicGeometry.StructureSheaf.instIsScalarTowerCarrierStalkCommRingCatStructurePresheafInCommRingCatCarrierAbPresheafOpensCarrierTopModuleStructurePresheaf, CommRingCat.instFullRingCatForget₂RingHomCarrierCarrier, FilteredColimits.instPreservesFilteredColimitsAddCommGrpCatForget₂RingHomCarrierAddMonoidHomCarrier, PresheafOfModules.add_app, PresheafOfModules.Sheafify.add_smul, PresheafOfModules.restrictScalars_map_app, PresheafOfModules.epi_iff_surjective, PresheafOfModules.evaluation_preservesColimitsOfShape, PresheafOfModules.comp_app, Colimits.cocone_naturality_components, PresheafOfModules.pushforward_map_app_apply, 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.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, 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.presheaf_obj_coe, 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.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, 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, forget₂SemiRing_preservesLimits, comp_apply, SheafOfModules.pushforwardNatTrans_app_val_app, PresheafOfModules.Sheafify.one_smul, forget₂AddCommGroup_preservesLimitsOfSize, PresheafOfModules.map_id, ofHom_hom, SheafOfModules.pushforwardPushforwardEquivalence_unit_app_val_app, SheafOfModules.relationsOfIsCokernelFree_s, PresheafOfModules.pushforward_obj_map_apply', PresheafOfModules.Hom.naturality, AlgCat.forget₂Ring_preservesLimits, forget_preservesLimits, SheafOfModules.forgetToSheafModuleCat_map_val, SheafOfModules.pushforwardPushforwardAdj_counit_app_val_app, PresheafOfModules.freeYonedaEquiv_comp, PresheafOfModules.Sheafify.zero_smul, AlgebraicGeometry.instIsQuasicoherentOpensCarrierCarrierCommRingCatSpecTilde, SheafOfModules.Presentation.IsFinite.finite_relations, SheafOfModules.pushforwardNatTrans_app_val_app_apply, PresheafOfModules.Finite.evaluation_preservesFiniteColimits, hom_inv_apply, 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, SheafOfModules.forgetToSheafModuleCat_obj_val, PresheafOfModules.evaluation_obj, forget_obj, FilteredColimits.forget₂SemiRing_preservesFilteredColimits, 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.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	52 math math: mapRingHom_id, Padic.withValUniformEquiv_norm_le_one_iff, Valued.valuedCompletion_surjective_iff, Isometry.extensionHom_coe, PadicComplex.valuation_extends, IsDedekindDomain.HeightOneSpectrum.instFaithfulSMulSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_symm_apply, IsDedekindDomain.HeightOneSpectrum.mem_adicCompletionIntegers, Valuation.IsEquiv.valuedCompletion_le_one_iff, PadicComplex.coe_natCast, extensionHom_coe, IsDedekindDomain.HeightOneSpectrum.adicCompletion.instIsScalarTower', Valued.exists_coe_eq_v, mapRingHom_apply, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_def, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.integers, IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletionIntegers_apply, IsDedekindDomain.HeightOneSpectrum.coe_smul_adicCompletionIntegers, PadicInt.coe_adicCompletionIntegersEquiv_symm_apply, Valued.continuous_extensionValuation, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation', IsDedekindDomain.HeightOneSpectrum.instIsTorsionFreeSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, PadicComplex.valuation_p, continuous_coeRingHom, PadicInt.coe_adicCompletionIntegersEquiv_apply, Valued.closure_coe_completion_v_lt, algebraMap_def, Valued.closure_coe_completion_v_mul_v_lt, Valued.valuedCompletion_apply, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_eq_valuation, LaurentSeries.powerSeries_ext_subring, Rat.HeightOneSpectrum.adicCompletionIntegers.coe_padicIntEquiv_apply, AbsoluteValue.Completion.isClosedEmbedding_extensionEmbedding_of_comp, AbsoluteValue.Completion.isometry_extensionEmbedding_of_comp, IsDedekindDomain.HeightOneSpectrum.valuedAdicCompletion_surjective, Valued.extensionValuation_apply_coe, mapRingHom_coe, LaurentSeries.valuation_compare, LaurentSeries.tendsto_valuation, coe_mapRingHom, LaurentSeries.comparePkg_eq_extension, PadicComplex.rankOne_hom_eq, instNonarchimedeanRingCompletion, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.isUnit_iff_valued_eq_one, mapRingHom_comp, instIsPrincipalIdealRingSubtypeAdicCompletionMemValuationSubringAdicCompletionIntegers, IsDedekindDomain.HeightOneSpectrum.adicCompletionIntegers.mem_units_iff_valued_eq_one, AbsoluteValue.Completion.extensionEmbedding_dist_eq_of_comp, AbsoluteValue.Completion.extensionEmbedding_of_comp_coe, PadicComplexInt.integers, topologicalRing, IsDedekindDomain.HeightOneSpectrum.notMem_adicCompletionIntegers

---

← Back to Index