| Name | Category | Theorems |
|---|
addGroupWithOne π | CompOp | β |
addMonoidWithOne π | CompOp | 2 mathmath: CharP.pi', CharP.pi
|
commRing π | CompOp | 19 mathmath: AlgebraicGeometry.pointsPi_surjective_of_isAffine, AlgebraicGeometry.ΞΉ_sigmaSpec, AlgebraicGeometry.instIsIsoSchemeSigmaSpecOfFinite, AlgebraicGeometry.pointsPi_injective, Algebra.FormallyEtale.instForallOfFinite, CommRingCat.coyoneda_map_app, Algebra.FormallyUnramified.instForall, CommRingCat.coyoneda_obj_map, Algebra.FormallyUnramified.pi_iff, AlgebraicGeometry.instIsOpenImmersionMapOfHomForallEvalRingHom, AlgebraicGeometry.instIsOpenImmersionSigmaSpec, Algebra.FormallySmooth.instForallOfFinite, Algebra.FormallyEtale.pi_iff, CommRingCat.coyonedaUnique_inv_app_hom_apply, AlgebraicGeometry.ΞΉ_sigmaSpec_assoc, CommRingCat.coyonedaUnique_hom_app_hom_apply, Algebra.FormallySmooth.pi_iff, CommRingCat.piFan_pt, AlgebraicGeometry.pointsPi_surjective
|
commSemiring π | CompOp | 23 mathmath: MeasureTheory.lpNorm_conj, PrimeSpectrum.sigmaToPi_bijective, PrimeSpectrum.iUnion_range_specComap_comp_evalRingHom, IsLocalization.bijective_lift_piRingHom_algebraMap_comp_piEvalRingHom, Localization.AtPrime.mapPiEvalRingHom_bijective, TensorProduct.piScalarRight_symm_algebraMap, conjneg_conj, PrimeSpectrum.toPiLocalization_not_surjective_of_infinite, IsLocalization.instForallPiUniv, PrimeSpectrum.iUnion_range_comap_comp_evalRingHom, IsLocalization.iff_map_piEvalRingHom, Localization.AtPrime.mapPiEvalRingHom_comp_algebraMap, AnalyticAt.harmonicAt_conj, PrimeSpectrum.sigmaToPi_asIdeal, PrimeSpectrum.exists_comap_evalRingHom_eq, conj_apply, MaximalSpectrum.toPiLocalization_not_surjective_of_infinite, PrimeSpectrum.exists_maximal_notMem_range_sigmaToPi_of_infinite, PrimeSpectrum.sigmaToPi_not_surjective_of_infinite, PrimeSpectrum.sigmaToPi_injective, IsLocalization.algebraMap_pi_surjective_of_isLocalization, MeasureTheory.eLpNorm_conj, Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply
|
constNonUnitalRingHom π | CompOp | 1 mathmath: constNonUnitalRingHom_apply
|
constRingHom π | CompOp | 2 mathmath: constRingHom_apply, constRingHom_eq_algebraMap
|
distrib π | CompOp | β |
evalNonUnitalRingHom π | CompOp | 1 mathmath: evalNonUnitalRingHom_apply
|
evalRingHom π | CompOp | 19 mathmath: RingHom.ker_evalRingHom, PrimeSpectrum.iUnion_range_specComap_comp_evalRingHom, Localization.AtPrime.mapPiEvalRingHom_bijective, AlgebraicGeometry.ΞΉ_sigmaSpec, CommRingCat.coyoneda_map_app, evalRingHom_apply, CommRingCat.coyoneda_obj_map, PrimeSpectrum.iUnion_range_comap_comp_evalRingHom, Ideal.IsMaximal.comap_piEvalRingHom, IsLocalization.iff_map_piEvalRingHom, Localization.mapPiEvalRingHom_bijective, Localization.AtPrime.mapPiEvalRingHom_comp_algebraMap, Ideal.map_evalRingHom_pi, PrimeSpectrum.sigmaToPi_asIdeal, PrimeSpectrum.exists_comap_evalRingHom_eq, AlgebraicGeometry.instIsOpenImmersionMapOfHomForallEvalRingHom, instRingHomSurjectiveForallEvalRingHom, AlgebraicGeometry.ΞΉ_sigmaSpec_assoc, Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply
|
hasDistribNeg π | CompOp | β |
nonAssocRing π | CompOp | β |
nonAssocSemiring π | CompOp | 100 mathmath: PrimeSpectrum.mapPiLocalization_id, WittVector.ghostMap.bijective_of_invertible, RingHom.ker_evalRingHom, MaximalSpectrum.mapPiLocalization_bijective, NumberField.canonicalEmbedding.mem_span_latticeBasis, NumberField.mixedEmbedding.convexBodyLT'_mem, NumberField.canonicalEmbedding.latticeBasis_apply, PrimeSpectrum.iUnion_range_specComap_comp_evalRingHom, Localization.AtPrime.mapPiEvalRingHom_bijective, NumberField.mixedEmbedding.norm_eq_norm, NumberField.mixedEmbedding.mem_idealLattice, NumberField.mixedEmbedding.fundamentalCone.completeBasis_apply_of_ne, MaximalSpectrum.toPiLocalization_apply_apply, Ideal.quotientInfToPiQuotient_inj, Matrix.blockDiagonal'RingHom_apply, Ideal.quotientInfToPiQuotient_surj, evalRingHom_apply, NumberField.mixedEmbedding.convexBodyLT_mem, MaximalSpectrum.mapPiLocalization_naturality, PrimeSpectrum.toPiLocalization_surjective_of_discreteTopology, Ideal.ker_Pi_Quotient_mk, NumberField.InfiniteAdeleRing.mixedEmbedding_eq_algebraMap_comp, PrimeSpectrum.mapPiLocalization_bijective, NumberField.canonicalEmbedding.integralBasis_repr_apply, ContinuousMap.coeFnRingHom_apply, RingHom.compLeft_apply, PrimeSpectrum.toPiLocalization_not_surjective_of_infinite, ker_ringHom, NumberField.mixedEmbedding.mem_span_fractionalIdealLatticeBasis, PrimeSpectrum.mapPiLocalization_comp, PrimeSpectrum.iUnion_range_comap_comp_evalRingHom, Ideal.IsMaximal.comap_piEvalRingHom, NumberField.mixedEmbedding.unit_smul_eq_iff_mul_eq, NumberField.mixedEmbedding.fundamentalCone.existsUnique_preimage_of_mem_integerSet, RingHom.functions_ext_iff, IsLocalization.iff_map_piEvalRingHom, Localization.mapPiEvalRingHom_bijective, Localization.AtPrime.mapPiEvalRingHom_comp_algebraMap, MaximalSpectrum.mapPiLocalization_id, PrimeSpectrum.mapPiLocalization_naturality, constRingHom_apply, Ideal.map_evalRingHom_pi, RingHom.pi_bijective_of_isIdempotentElem, PrimeSpectrum.toPiLocalization_bijective, NumberField.mixedEmbedding.det_basisOfFractionalIdeal_eq_norm, NumberField.mixedEmbedding.logMap_eq_logEmbedding, NumberField.canonicalEmbedding.nnnorm_eq, NumberField.mixedEmbedding.mixedEmbedding_apply_isReal, OrthogonalIdempotents.surjective_pi, PrimeSpectrum.discreteTopology_iff_toPiLocalization_surjective, ringHom_injective, WittVector.ghostMap_apply, PrimeSpectrum.piLocalizationToMaximal_comp_toPiLocalization, NumberField.mixedEmbedding.normAtAllPlaces_mixedEmbedding, PrimeSpectrum.piLocalizationToMaximal_surjective, Filter.Germ.coe_coeRingHom, NumberField.mixedEmbedding.fundamentalCone.mixedEmbedding_preimageOfMemIntegerSet, Algebra.TensorProduct.piRightHom_one, NumberField.inverse_basisMatrix_mulVec_eq_repr, NumberField.canonicalEmbedding.mem_rat_span_latticeBasis, NumberField.mixedEmbedding.unitSMul_smul, Matrix.diagonalRingHom_apply, MaximalSpectrum.mapPiLocalization_comp, NumberField.mixedEmbedding.normAtPlace_apply, NumberField.canonicalEmbedding.norm_le_iff, NumberField.mixedEmbedding_injective, conjnegRingHom_apply, NumberField.mixedEmbedding.latticeBasis_apply, NumberField.canonicalEmbedding_injective, ringHom_apply, NumberField.mixedEmbedding.latticeBasis_repr_apply, NumberField.canonicalEmbedding.apply_at, Ideal.quotientInfToPiQuotient_mk', MaximalSpectrum.toPiLocalization_injective, NumberField.mixedEmbedding.fractionalIdealLatticeBasis_apply, Ideal.quotientInfToPiQuotient_mk, CompleteOrthogonalIdempotents.bijective_pi', MaximalSpectrum.toPiLocalization_not_surjective_of_infinite, Matrix.blockDiagonalRingHom_apply, PrimeSpectrum.piLocalizationToMaximal_bijective, NumberField.mixedEmbedding.fundamentalCone.realSpaceToLogSpace_expMap_symm, PrimeSpectrum.toPiLocalization_injective, NumberField.mixedEmbedding.fundamentalCone.mem_idealSet, NumberField.mixedEmbedding.fundamentalCone.sum_expMap_symm_apply, ContMDiffMap.coeFnRingHom_apply, NumberField.mixedEmbedding.mixedEmbedding_apply_isComplex, NumberField.canonicalEmbedding_eq_basisMatrix_mulVec, NumberField.mixedEmbedding.fundamentalCone.mem_integerSet, WittVector.ghostEquiv_coe, PrimeSpectrum.maximalSpectrumToPiLocalization_surjective_of_discreteTopology, NumberField.mixedEmbedding.commMap_canonical_eq_mixed, NumberField.mixedEmbedding.norm_unit, LocallyConstant.coeFnRingHom_apply, NumberField.mixedEmbedding.fundamentalCone.expMap_basis_of_ne, Localization.AtPrime.mapPiEvalRingHom_algebraMap_apply, Matrix.algebraMap_eq_diagonalRingHom, PrimeSpectrum.discreteTopology_iff_toPiLocalization_bijective, NumberField.mixedEmbedding.convexBodySum_mem, CompleteOrthogonalIdempotents.bijective_pi, NumberField.mixedEmbedding.mem_rat_span_latticeBasis
|
nonUnitalCommRing π | CompOp | β |
nonUnitalCommSemiring π | CompOp | β |
nonUnitalNonAssocRing π | CompOp | 1 mathmath: instIsTopologicalRing
|
nonUnitalNonAssocSemiring π | CompOp | 11 mathmath: comul_eq_adjoint, nonUnitalRingHom_apply, instIsTopologicalSemiring, Algebra.TensorProduct.piRightHom_mul, constNonUnitalRingHom_apply, Finsupp.coe_pointwise_smul, NonUnitalRingHom.compLeft_apply, evalNonUnitalRingHom_apply, nonUnitalRingHom_injective, evalNonUnitalStarAlgHom_apply, evalStarAlgHom_apply
|
nonUnitalRing π | CompOp | 5 mathmath: cfcβ_map_pi, quasispectrum_eq, CFC.nnrpow_map_pi, CFC.nnrpow_eq_nnrpow_pi, CFC.sqrt_map_pi
|
nonUnitalRingHom π | CompOp | 2 mathmath: nonUnitalRingHom_apply, nonUnitalRingHom_injective
|
nonUnitalSemiring π | CompOp | 2 mathmath: isQuasiregular_pi_iff, instStarOrderedRing
|
ringHom π | CompOp | 13 mathmath: IsLocalization.bijective_lift_piRingHom_algebraMap_comp_piEvalRingHom, CommRingCat.coyoneda_map_app, CommRingCat.coyoneda_obj_map, Ideal.ker_Pi_Quotient_mk, ker_ringHom, IsLocalization.isUnit_piRingHom_algebraMap_comp_piEvalRingHom, RingHom.pi_bijective_of_isIdempotentElem, OrthogonalIdempotents.surjective_pi, ringHom_injective, ringHom_apply, CompleteOrthogonalIdempotents.bijective_pi', IsLocalization.surjective_piRingHom_algebraMap_comp_piEvalRingHom, CompleteOrthogonalIdempotents.bijective_pi
|
semiring π | CompOp | 91 mathmath: comul_eq_adjoint, RingHom.ker_evalRingHom, AlgEquiv.piCongrRight_refl, isOrderedRing, constAlgHom_apply, Localization.algebraMap_injective_of_span_eq_top, Polynomial.algebraMap_pi_eq_aeval, ContMDiffMap.coeFnAlgHom_apply, algebraMap_apply, Ideal.single_mem_pi, Subalgebra.pi_top, MvPowerSeries.mem_hasEvalIdeal_iff, TensorProduct.piScalarRight_symm_algebraMap, AlgEquiv.piCongrRight_trans, Polynomial.aeval_fn_apply, BoxIntegral.unitPartition.mem_smul_span_iff, algHom_comp, Algebra.TensorProduct.piRightHom_mul, Algebra.TensorProduct.piScalarRight_tmul, Ideal.instIsTwoSidedForallPi, counit_eq_adjoint, instIsArtinianRingForallOfFinite, Ideal.ker_Pi_Quotient_mk, AlgebraicGeometry.Ideal.span_eq_top_of_span_image_evalRingHom, Ideal.instIsPrincipalIdealRingForallOfFinite, ContinuousMap.coeFnAlgHom_apply, Ideal.span_single_eq_top, AlgEquiv.sumArrowEquivProdArrow_symm_apply_inr, ker_ringHom, Polynomial.aeval_pi_apply, AlgEquiv.piCongrRight_symm, Ideal.IsMaximal.comap_piEvalRingHom, IsSemisimpleRing.exists_algEquiv_pi_matrix_end_mulOpposite, Ideal.pi_le_pi_iff, Localization.mapPiEvalRingHom_bijective, IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing, algHom_apply, Ideal.map_evalRingHom_pi, Polynomial.algebraMap_pi_self_eq_eval, AlgEquiv.funUnique_apply, LocallyConstant.coeFnAlgHom_apply, CompleteOrthogonalIdempotents.single, AlgEquiv.piCongrLeft'_apply, AlgEquiv.piCongrLeft_apply, algebraMap_memβp_infty, AlgHom.compLeft_apply, algHom_evalAlgHom, Matrix.algebraMap_eq_diagonal, IsSemisimpleRing.exists_algEquiv_pi_matrix_of_isAlgClosed, Ideal.pi_span, NumberField.InfinitePlace.denseRange_algebraMap_pi, Matrix.diagonalAlgHom_apply, Subalgebra.pi_mono, IsSemisimpleModule.exists_end_algEquiv, Subalgebra.pi_toSubsemiring, Algebra.TensorProduct.piRight_tmul, MvPowerSeries.coe_hasEvalIdeal, Matrix.piAlgEquiv_symm_apply, AlgCat.instSmallSubtypeForallCarrierObjMemSubalgebraSectionsSubalgebra, instIsNoetherianRingForallOfFinite, Subalgebra.coe_pi, instRingHomSurjectiveForallEvalRingHom, IsSemisimpleModule.exists_end_algEquiv_pi_matrix_end, isPrincipalIdealRing_pi_iff, Ideal.coe_piOrderIso_symm_apply, AlgEquiv.piCongrLeft_symm_apply, LocallyConstant.coe_algebraMap, IsSemisimpleModule.exists_end_algEquiv_pi_matrix_divisionRing, AlgEquiv.piCongrRight_apply, Algebra.FinitePresentation.pi, IsSemisimpleRing.exists_algEquiv_pi_matrix_divisionRing_finite, Polynomial.aeval_pi, Subalgebra.mem_pi, IsLocalRing.not_isLocalRing_of_nontrivial_pi, Ideal.mem_pi, Polynomial.aeval_pi_applyβ, evalStarAlgHom_apply, constAlgHom_eq_algebra_ofId, AlgEquiv.sumArrowEquivProdArrow_apply, AlgEquiv.funUnique_symm_apply, Algebra.TensorProduct.piScalarRight_tmul_apply, evalAlgHom_apply, constRingHom_eq_algebraMap, MeasureTheory.SimpleFunc.coe_algebraMap, Ideal.coe_piOrderIso_apply, algebraMap_def, Subalgebra.pi_toSubmodule, AlgEquiv.piCongrLeft'_symm_apply, Matrix.piAlgEquiv_apply, Matrix.algebraMap_eq_diagonalRingHom, BoxIntegral.unitPartition.tag_mem_smul_span
|