| Metric | Count |
|---|
DefinitionsequivOpposite, hasDistribPointwiseNeg, idemSemiring, instAddCommMonoidWithOne, instDiv, instIdemCommSemiring, instNonUnitalSemiring, instPowNat, instSMul, mapHom, moduleSet, mul, one, pointwiseMulSemiringAction, ringHom, spanSingleton | 16 |
TheoremsalgebraMap_mem, mem_one', algebraMap_mem, bot_mul, bot_pow, bot_smul, coe_set_smul, comap_op_mul, comap_op_one, comap_op_pow, comap_unop_mul, comap_unop_one, comap_unop_pow, equivOpposite_apply, equivOpposite_symm_apply, iSup_mul, iSup_smul, instCovariantClassHSMulLe_1, instIsOrderedRing, instIsScalarTower, instMulLeftMono, instMulRightMono, instSMulCommClass, instSMulCommClass_1, ker_unitsMap_spanSingleton, le_div_iff, le_div_iff_mul_le, le_one_toAddSubmonoid, le_pow_toAddSubmonoid, le_self_mul_one_div, mapHom_apply, mapHom_id, map_div, map_mul, map_one, map_op_mul, map_op_one, map_op_pow, map_pow, map_unop_mul, map_unop_one, map_unop_pow, mem_div_iff_forall_mul_mem, mem_div_iff_smul_subset, mem_mul_span_singleton, mem_one, mem_smul_iff_inv_mul_mem, mem_span_mul_finite_of_mem_mul, mem_span_mul_finite_of_mem_span_mul, mem_span_singleton_mul, mker_spanSingleton, mul_bot, mul_comm, mul_comm_of_commute, mul_def, mul_eq_map₂, mul_eq_span_mul_set, mul_iSup, mul_induction_on, mul_induction_on', mul_le, mul_mem_mul, mul_mem_mul_rev, mul_mem_smul_iff, mul_one, mul_one_div_le_one, mul_smul_mul_eq_smul_mul_smul, mul_subset_mul, mul_sup, mul_toAddSubmonoid, mul_top_eq_top_of_mul_eq_one, one_eq_range, one_eq_span, one_eq_span_one_set, one_le, one_le_one_div, one_mem_div, one_mul, one_smul, pow_add, pow_eq_npowRec, pow_eq_span_pow_set, pow_induction_on_left, pow_induction_on_left', pow_induction_on_right, pow_induction_on_right', pow_mem_pow, pow_one, pow_subset_pow, pow_succ, pow_succ', pow_toAddSubmonoid, pow_zero, prod_span, prod_span_singleton, restrictScalars_mul, restrictScalars_pow, setSemiring_smul_def, singleton_smul, smul_assoc, smul_bot, smul_iSup, smul_induction_on, smul_induction_on', smul_le, smul_le_smul, smul_mem_smul, smul_mono, smul_mono_left, smul_one_eq_span, smul_subset_smul, smul_sup, smul_toAddSubmonoid, ringHom_apply, spanSingleton_apply, span_mul_span, span_pow, span_singleton_algebraMap_of_isUnit, span_singleton_eq_one_iff, span_singleton_mul, sup_mul, sup_smul, toSubMulAction_one, top_mul_eq_top_of_mul_eq_one | 124 |
| Total | 140 |
| Name | Category | Theorems |
|---|
equivOpposite 📖 | CompOp | 5 mathmath: LinearDisjoint.op, equivOpposite_apply, linearDisjoint_op, equivOpposite_symm_apply, mulMap_op
|
hasDistribPointwiseNeg 📖 | CompOp | — |
idemSemiring 📖 | CompOp | 249 mathmath: Ideal.toCotangent_to_quotient_square, Ideal.radical_sup, DoubleQuot.liftSupQuotQuotMkₐ_toRingHom, FractionalIdeal.finprod_heightOneSpectrum_factorization_principal, Ideal.finite_setOf_absNorm_le₀, ClassGroup.mk0_integralRep, ClassGroup.mk0_eq_mk0_iff, Ideal.toCotangent_eq, Ideal.absNorm_span_insert, Ideal.squarefree_span_singleton, Ideal.relNorm_smul, FractionalIdeal.coeIdealHom_apply, NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal, coe_mapAlgEquiv_symm_apply, normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity, NumberField.mixedEmbedding.fundamentalCone.integerSetEquivNorm_apply_fst, Associates.finite_factors, Ideal.comap_cotangentIdeal, NumberField.FinitePlace.norm_def', Ideal.finite_setOf_absNorm_eq, IsDedekindDomain.HeightOneSpectrum.intValuation_if_neg, DoubleQuot.coe_quotLeftToQuotSupₐ, AdicCompletion.incl_apply, FractionalIdeal.count_well_defined, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_apply, Ideal.range_cotangentToQuotientSquare, Ideal.relNorm_mono, FractionalIdeal.absNorm_eq', Ideal.relNorm_relNorm, Ideal.mem_toCotangent_ker, Ideal.absNorm_pos_iff_mem_nonZeroDivisors, Algebra.Generators.compLocalizationAwayAlgHom_toAlgHom_toComp, NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le, ker_unitsToPic, IsDedekindDomain.HeightOneSpectrum.intValuationDef_if_neg, Ideal.absNorm_eq_pow_inertiaDeg', Ideal.relNorm_top, NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_norm_eq_mul_torsion, Ideal.gcd_eq_sup, Ideal.relNorm_eq_pow_of_isPrime_isGalois, Ideal.absNorm_eq_pow_inertiaDeg_of_liesOver, Ideal.absNorm_mem, Ideal.sup_eq_top_iff_isCoprime, IsLocalRing.exists_maximalIdeal_pow_le_of_finite_quotient, Ideal.ramificationIdx_ne_one_iff, Ideal.map_sup_mem_minimalPrimes_of_map_quotientMk_mem_minimalPrimes, Ideal.absNorm_ne_zero_iff_mem_nonZeroDivisors, IsAdic.hasBasis_nhds, DoubleQuot.quotQuotToQuotSupₐ_toRingHom, Algebra.Generators.compLocalizationAwayAlgHom_X_inl, NumberField.mixedEmbedding.fundamentalCone.integerSetEquiv_apply_fst, Ideal.relNorm_singleton, Ideal.map_relNorm, MvPolynomial.degreesLE_nsmul, Ideal.sup_pow_add_le_pow_sup_pow, FractionalIdeal.coeIdeal_sup, Ideal.relNorm_le_comap, FractionalIdeal.finprod_heightOneSpectrum_factorization, PrimeSpectrum.sup_vanishingIdeal_le, IsDedekindDomain.HeightOneSpectrum.irreducible, StarAlgebra.adjoin_nonUnitalStarSubalgebra_eq_span, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_add_eq, FractionalIdeal.count_ne_zero, KaehlerDifferential.End_equiv_aux, Ideal.instIsScalarTowerQuotientHPowKerRingHomAlgebraMapOfNat, FractionalIdeal.canonicalEquiv_mk0, NumberField.natAbs_discr_eq_absNorm_differentIdeal_mul_natAbs_discr_pow, Associates.le_singleton_iff, Algebra.adjoin_nonUnitalSubalgebra_eq_span, IsFractional.sup, Algebra.Extension.Cotangent.mk_eq_zero_iff, Algebra.Generators.sq_ker_comp_le_ker_compLocalizationAwayAlgHom, Ideal.exists_relNorm_eq_pow_of_isPrime, Ideal.mem_minimalPrimes_sup, AdicCompletion.factorₐ_evalₐ_one, DoubleQuot.ker_quotQuotMk, Ideal.span_singleton_nonZeroDivisors, DoubleQuot.coe_quotQuotEquivQuotSupₐ, IsAdic.hasBasis_nhds_zero, Ideal.relNorm_algebraMap', projective_units, tensorKaehlerQuotKerSqEquiv_symm_tmul_D, Ideal.mk_mem_cotangentIdeal, coe_mapAlgEquiv_apply, Ideal.relNorm_int, Ideal.absNorm_dvd_absNorm_of_le, NumberField.Ideal.tendsto_norm_le_div_atTop₀, MvPolynomial.le_coeffsIn_pow, Int.absNorm_under_mem, NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def, unitsToPic_apply, Ideal.spanNorm_eq, FractionalIdeal.absNorm_eq, DoubleQuot.coe_quotQuotEquivQuotSupₐ_symm, range_unitsToPic, Ideal.relNorm_algebraMap, spanSingleton_apply, IsCoprime.sup_eq, tensorKaehlerQuotKerSqEquiv_tmul_D, Algebra.Generators.comp_localizationAway_ker, FractionalIdeal.coeSubmoduleHom_apply, Ideal.iSup_iInf_eq_top_iff_pairwise, Ideal.isCoprime_tfae, Ideal.relNorm_eq_bot_iff, IsPrimitiveRoot.not_coprime_norm_of_mk_eq_one, NumberField.FinitePlace.norm_def_int, Ideal.card_norm_le_eq_card_norm_le_add_one, DividedPowers.isSubDPIdeal_sup, unitsQuotEquivRelPic_symm_apply, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_mul, Ideal.sup_mul_inf, ClassGroup.mk_mk0, Ideal.isDomain, Polynomial.isEisensteinAt_iff, NumberField.absNorm_differentIdeal, DoubleQuot.ker_quotLeftToQuotSup, ClassGroup.mk0_eq_mk0_iff_exists_fraction_ring, Ideal.finite_mulSupport_coe, Ideal.absNorm_top, Ideal.absNorm_apply, Ideal.absNorm_pos_of_nonZeroDivisors, Ideal.toCotangent_eq_zero, Ideal.cotangentEquivIdeal_apply, Ideal.minimalPrimes_map_of_surjective, Algebra.Extension.Cotangent.mk_eq_mk_iff_sub_mem, Polynomial.coeff_divModByMonicAux_mem_span_pow_mul_span, Int.absNorm_under_dvd_absNorm, Algebra.FormallySmooth.iff_split_surjection, ClassGroup.equivPic_symm_apply, mker_spanSingleton, IsDedekindDomain.HeightOneSpectrum.intValuation_def, FractionalIdeal.coe_sup, NumberField.exists_ideal_in_class_of_norm_le, instInvertibleSubtypeMemVal, NumberField.Ideal.tendsto_norm_le_div_atTop, Ideal.count_associates_eq, Ideal.natAbs_det_equiv, emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity, Ideal.absNorm_eq_one_iff, DoubleQuot.quotQuotEquivQuotSup_quotQuotMk, NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_symm_apply, Ideal.radical_pow, instIsOrderedRing, Algebra.Generators.ker_comp_eq_sup, MvPolynomial.coeffsIn_pow, Ideal.span_singleton_mem_isPrincipalSubmonoid, IsHausdorff.eq_iff_smodEq, DoubleQuot.coe_quotQuotToQuotSupₐ, Ideal.map_eq_iff_sup_ker_eq_of_surjective, mapHom_id, Algebra.Extension.Hom.sub_aux, Ideal.isUnit_iff, DoubleQuot.quotQuotEquivQuotSupₐ_toRingEquiv, AlgebraicGeometry.Scheme.IdealSheafData.ideal_sup, ClassGroup.exists_mk0_eq_mk0, Ideal.finite_quotient_pow, IsLocalRing.exists_maximalIdeal_pow_le_of_isArtinianRing_quotient, MvPolynomial.C_mem_pow_idealOfVars_iff, Ideal.finprod_count, ClassGroup.mk0_surjective, Ideal.finite_setOf_absNorm_le, AlgHom.ker_kerSquareLift, Ideal.mem_isPrincipalSubmonoid_iff, ClassGroup.exists_min, NumberField.toNNReal_valued_eq_adicAbv, NumberField.mixedEmbedding.fundamentalCone.preimage_of_IdealSetMap, Units.submodule_isFractional, FractionalIdeal.absNorm_div_norm_eq_absNorm_div_norm, Algebra.Generators.compLocalizationAwayAlgHom_relation_eq_zero, Ideal.eq_prime_pow_mul_coprime, ProjectiveSpectrum.zeroLocus_sup_ideal, FractionalIdeal.map_canonicalEquiv_mk0, Ideal.absNorm_eq_pow_inertiaDeg, Ideal.cotangentEquivIdeal_symm_apply, Ideal.finprod_heightOneSpectrum_factorization_coe, mulExact_unitsMap_spanSingleton_unitsToPic, Ideal.absNorm_eq_zero_iff, IsCyclotomicExtension.Rat.absNorm_span_zeta_sub_one, FractionalIdeal.finite_factors', mapHom_apply, Ideal.IsDedekindDomain.ramificationIdx_eq_multiplicity, count_associates_factors_eq, Ideal.count_associates_eq', coe_mapAlgHom_apply, ClassGroup.equiv_mk0, Ideal.absNorm_bot, DoubleQuot.quotQuotEquivQuotSup_symm_quotQuotMk, Ideal.relNorm_apply, NumberField.mixedEmbedding.fundamentalCone.mem_idealSet, NumberField.Ideal.tendsto_norm_le_and_mk_eq_div_atTop, NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_apply, sup_eq_prod_inf_factors, Int.ideal_span_absNorm_eq_self, MonomialOrder.sPolynomial_mem_sup_ideal, Ideal.relNorm_bot, Ideal.norm_mem_relNorm, ClassGroup.mk0_eq_mk0_inv_iff, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_map_one, PrimeSpectrum.zeroLocus_sup, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_coe, DoubleQuot.quotQuotEquivQuotSup_quot_quot_algebraMap, IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, span.ringHom_apply, Ideal.absNorm_relNorm, ClassGroup.equivPic_apply, Int.absNorm_under_eq_sInf, Ideal.absNorm_span_singleton, FractionalIdeal.coeIdeal_absNorm, AlgHom.kerSquareLift_mk, Ideal.map_toCotangent_ker, Ideal.absNorm_algebraMap, Int.cast_mem_ideal_iff, Ideal.isCoprime_iff_sup_eq, Ideal.relNorm_map_algEquiv, emultiplicity_eq_emultiplicity_span, IsDedekindDomain.exists_sup_span_eq, DoubleQuot.quotLeftToQuotSupₐ_toRingHom, FractionalIdeal.finprod_heightOneSpectrum_factorization_principal_fraction, NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm, Ideal.span_singleton_absNorm_le, Ideal.finprod_not_dvd, Ideal.natAbs_det_basis_change, IsLocalRing.finite_quotient_iff, DoubleQuot.quotQuotEquivQuotSupₐ_symm_toRingEquiv, ClassGroup.integralRep_mem_nonZeroDivisors, Ideal.ringChar_quot, Ideal.cotangentIdeal_square, IsDedekindDomain.HeightOneSpectrum.associates_irreducible, Int.liesOver_span_absNorm, IsLocalization.coeSubmodule_sup, Ideal.finite_mulSupport_inv, mulExact_unitsToPic_mapAlgebra, FractionalIdeal.coe_mk0, Ideal.mapHom_apply, Ideal.relNorm_eq_pow_of_isMaximal, DoubleQuot.coe_liftSupQuotQuotMkₐ, Polynomial.IsEisensteinAt.notMem, NumberField.Ideal.primesOverSpanEquivMonicFactorsMod_symm_apply, Nat.absNorm_under_prime, FractionalIdeal.count_coe, ker_unitsMap_spanSingleton, Ideal.relNorm_comap_algEquiv, Ideal.to_quotient_square_comp_toCotangent, fg_unit, emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity, unitsQuotEquivRelPic_apply_coe, derivationQuotKerSq_mk, NumberField.mixedEmbedding.fundamentalCone.intNorm_idealSetEquiv_apply, Ideal.absNorm_dvd_norm_of_mem
|
instAddCommMonoidWithOne 📖 | CompOp | 69 mathmath: Ideal.Quotient.map_ker_stabilizer_subtype, Ideal.relNorm_smul, Ideal.natCast_eq_top, Ideal.smul_closure, Ideal.mem_pointwise_smul_iff_inv_smul_mem, BoxIntegral.unitPartition.mem_smul_span_iff, Ideal.exists_smul_eq_of_isGaloisGroup, Ideal.subset_pointwise_smul_iff, Ideal.LiesOver.smul, Ideal.smul_sup, Ideal.Quotient.stabilizerHom_surjective, Ideal.pointwise_smul_subset_iff, Ideal.instCovariantClassHSMulLe, instSMulCommClass, Algebra.IsInvariant.exists_smul_of_under_eq, Ideal.under_smul, mul_mem_smul_iff, Ideal.card_stabilizer_eq, mem_smul_iff_inv_mul_mem, FractionalIdeal.coe_nsmul, FractionalIdeal.coe_natCast, Ideal.IsPrime.smul_iff, spinGroup.conjAct_smul_range_ι, Ideal.Quotient.smul_top, traceForm_dualSubmodule_adjoin, Ideal.Quotient.stabilizerHom_surjective_of_profinite, Ideal.inertia_le_stabilizer, Algebra.IsInvariant.orbit_eq_primesOver, smul_le_smul, Ideal.exact_mulQuot_quotOfMul, IsFractionRing.stabilizerHom_surjective, Ideal.Quotient.stabilizerHom_apply, Algebra.IsInvariant.exists_smul_of_under_eq_of_profinite, Ideal.Quotient.stabilizerQuotientInertiaEquiv_mk, mul_smul_mul_eq_smul_mul_smul, singleton_smul, Ideal.coe_smul_primesOver_mk, pinGroup.conjAct_smul_range_ι, Ideal.quotOfMul_surjective, Ideal.pointwise_smul_eq_comap, Ideal.IsPrime.smul, FractionalIdeal.den_mul_self_eq_num, Ideal.smul_mem_pointwise_smul, smul_one_eq_span, Ideal.Quotient.ker_stabilizerHom, Ideal.smul_bot, Ideal.pointwise_smul_le_pointwise_smul_iff, Ideal.card_stabilizer_eq_card_inertia_mul_finrank, Ideal.pointwise_central_scalar, Ideal.pointwise_smul_toAddSubgroup, span_singleton_mul, setSemiring_smul_def, IsFractional.nsmul, instSMulCommClass_1, Subalgebra.pointwise_smul_toSubmodule, Ideal.map_pointwise_smul, Ideal.smul_mem_pointwise_smul_iff, Ideal.coe_smul_primesOver, Ideal.exists_map_eq_of_isGalois, Ideal.instNormalSubtypeMemSubgroupStabilizerSubgroupOfInertia, ringKrullDim_le_ringKrullDim_quotSMulTop_succ, IsArithFrobAt.conj, Ideal.pointwise_smul_toAddSubmonoid, lipschitzGroup.conjAct_smul_range_ι, Ideal.mem_inv_pointwise_smul_iff, Ideal.pointwise_smul_def, BoxIntegral.unitPartition.tag_mem_smul_span, instIsScalarTower, Ideal.mulQuot_injective
|
instDiv 📖 | CompOp | 21 mathmath: mul_one_div_le_one, FractionalIdeal.isFractional_div_of_ne_zero, one_mem_div, le_self_mul_one_div, le_div_iff_mul_le, FractionalIdeal.inv_nonzero, mem_div_iff_forall_mul_mem, FractionalIdeal.div_of_ne_zero, coeSubmodule_differentIdeal, coeSubmodule_differentIdeal_fractionRing, FractionalIdeal.fractional_div_of_nonzero, one_le_one_div, FractionalIdeal.div_nonzero, IsFractional.div_of_nonzero, FractionalIdeal.coe_inv_of_ne_zero, FractionalIdeal.coe_inv_of_nonzero, le_div_iff, FractionalIdeal.coe_div, mem_div_iff_smul_subset, map_div, FractionalIdeal.inv_of_ne_zero
|
instIdemCommSemiring 📖 | CompOp | 23 mathmath: Ideal.prod_le_inf, Ideal.multiset_prod_span_singleton, prod_span, prod_span_singleton, Ideal.isCoprime_tfae, unitsQuotEquivRelPic_symm_apply, Ideal.prod_mem_prod, Ideal.isCoprime_iff_exists, ClassGroup.equivPic_symm_apply, Ideal.coprime_of_no_prime_ge, Ideal.prod_span, Ideal.sup_prod_eq_top, Ideal.isCoprime_span_singleton_iff, Ideal.isCoprime_iff_add, Ideal.multiset_prod_le_inf, Ideal.multiset_prod_eq_bot, Ideal.prod_span_singleton, Ideal.prod_sup_eq_top, Ideal.isCoprime_iff_codisjoint, Ideal.isCoprime_iff_sup_eq, Ideal.isCoprime_of_isMaximal, Ideal.sup_multiset_prod_eq_top, unitsQuotEquivRelPic_apply_coe
|
instNonUnitalSemiring 📖 | CompOp | 25 mathmath: IsDedekindDomain.differentIdeal_dvd_map_differentIdeal, Ideal.dvd_iff_le, IsDedekindDomain.HeightOneSpectrum.equivPrimesOver_apply, span_singleton_dvd_span_singleton_iff_dvd, idealFactorsEquivOfQuotEquiv_mem_normalizedFactors_of_mem_normalizedFactors, Ideal.liesOver_iff_dvd_map, NumberField.mixedEmbedding.fundamentalCone.card_isPrincipal_dvd_norm_le, idealFactorsFunOfQuotHom_comp, IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd, IsDedekindDomain.HeightOneSpectrum.valuation_lt_one_iff_dvd, IsDedekindDomain.map_differentIdeal_dvd_differentIdeal, Ideal.dvd_bot, not_dvd_differentIdeal_of_isCoprime_of_isSeparable, dvd_differentIdeal_iff, IsDedekindDomain.HeightOneSpectrum.intValuation_lt_one_iff_dvd, idealFactorsEquivOfQuotEquiv_symm, dvd_differentIdeal_of_not_isSeparable, Ideal.finite_factors, not_dvd_differentIdeal_of_isCoprime, not_dvd_differentIdeal_iff, idealFactorsFunOfQuotHom_id, idealFactorsFunOfQuotHom_coe_coe, not_dvd_differentIdeal_of_intTrace_not_mem, Ideal.dvd_span_singleton, Ideal.finprod_not_dvd
|
instPowNat 📖 | CompOp | 221 mathmath: Ideal.exists_pow_le_of_le_radical_of_fg_radical, AdicCompletion.val_sub_apply, pow_zero, Ideal.IsTwoSided.pow_succ, AdicCompletion.AdicCauchySequence.mk_eq_mk, Ideal.iInf_pow_smul_eq_bot_of_isLocalRing, AdicCompletion.map_val_apply, mem_reesAlgebra_iff_support, Ideal.rank_prime_pow_ramificationIdx, Matrix.coeff_charpoly_mem_ideal_pow, ChevalleyThm.chevalley_polynomialC, Ideal.span_pow_eq_map_homogeneousSubmodule, comap_op_pow, AdicCompletion.val_smul, WittVector.factorPowSucc_comp_fontaineThetaModPPow, Ideal.iInf_pow_smul_eq_bot_of_le_jacobson, AdicCompletion.val_smul_eq_evalₐ_smul, span_pow, WittVector.factorPowSucc_fontaineThetaModPPow_eq, Ideal.bot_pow, Ideal.FG.pow, MvPolynomial.pow_idealOfVars, Ideal.pow_sup_eq_top, IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_mem, irreducible_pow_sup_of_ge, Ideal.exists_pow_le_of_le_radical_of_fg, pow_smul_top_le, MvPolynomial.mem_pow_idealOfVars_iff, Ideal.pow_sup_pow_eq_top, Ideal.relNorm_eq_pow_of_isPrime_isGalois, AdicCompletion.pi_apply_coe, pow_add, PowerSeries.IsWeierstrassDivisorAt.coeff_seq_succ_sub_seq_mem, AdicCompletion.val_add_apply, AdicCompletion.smul_eval, WittVector.mk_pow_fontaineTheta, Ideal.adic_module_basis, FractionalIdeal.coe_pow, Ideal.powQuotSuccInclusion_apply_coe, isInternal_prime_power_torsion_of_is_torsion_by_ideal, AlgebraicGeometry.Scheme.IdealSheafData.ideal_pow, Hausdorffification.instIsHausdorff, ChevalleyThm.chevalley_mvPolynomialC, Ideal.sup_pow_add_le_pow_sup_pow, AdicCompletion.mkₐ_apply_coe, Ideal.pow_succ_lt_pow, Ideal.map_mk_comap_factorPow, AdicCompletion.isAdicCauchy_iff, AdicCompletion.val_sum, IsDedekindDomain.HeightOneSpectrum.intValuation_le_pow_iff_dvd, IsHausdorff.iInf_pow_smul, IsDedekindDomain.exists_forall_sub_mem_ideal, Polynomial.exists_monic_aeval_eq_zero_forall_mem_pow_of_isIntegral, Ideal.index_pow_le, MvPolynomial.pow_idealOfVars_eq_span, AdicCompletion.range_eval, AdicCompletion.val_neg_apply, Ideal.sup_pow_eq_top', AdicCompletion.transitionMap_comp_eval, Associates.le_singleton_iff, Ideal.finrank_prime_pow_ramificationIdx, Ideal.le_pow_ramificationIdx, Polynomial.coeff_modByMonic_mem_pow_natDegree_mul, pow_succ, Valuation.pow_Uniformizer_is_pow_generator, CliffordAlgebra.submodule_map_pow_reverse, AdicCompletion.coe_eval, AdicCompletion.factorₐ_evalₐ_one, map_unop_pow, Ideal.exists_radical_pow_le_of_fg, AdicCompletion.val_mul, MvPolynomial.mem_pow_idealOfVars_iff', Ideal.Filtration.Stable.exists_pow_smul_eq_of_ge, AdicCompletion.mk_ofAlgEquiv_symm, IsSemiprimaryRing.isNilpotent, MvPolynomial.monomial_mem_pow_idealOfVars_iff, reesAlgebra.monomial_mem, Ideal.pow_le_self, Ideal.relNorm_algebraMap', AdicCompletion.transitionMap_comp_reduceModIdeal, bot_pow, Ideal.pow_right_mono, Ideal.isOpen_pow_of_isMaximal, map_op_pow, MvPolynomial.le_coeffsIn_pow, Ideal.Filtration.Stable.exists_pow_smul_eq, AdicCompletion.smul_mk, WittVector.ker_map_le_ker_mk_comp_ghostComponent, WittVector.fontaineThetaModPPow_teichmuller, Ideal.hasBasis_nhds_zero_adic, Ideal.relNorm_algebraMap, irreducible_pow_sup, FG.pow, WittVector.ghostComponentModPPow_teichmuller_coeff, IsFractional.pow, Polynomial.coeff_mem_pow_of_mem_adjoin_C_mul_X, Ideal.Quotient.algebraMap_quotient_pow_ramificationIdx, cardQuot_pow_of_prime, AdicCompletion.Ideal.mk_eq_mk, Ideal.IsTwoSided.instHPowNat, Ideal.pow_le_pow_right, Ideal.Filtration.stable_iff_exists_pow_smul_eq_of_ge, PowerSeries.IsWeierstrassDivisorAt.coeff_seq_mem, Ideal.Filtration.pow_smul_le_pow_smul, MvPolynomial.restrictSupport_nsmul, IsDedekindDomain.inf_prime_pow_eq_prod, exists_maximalIdeal_pow_eq_of_principal, Ideal.adic_basis, Ideal.stableFiltration_N, Polynomial.coeff_divModByMonicAux_mem_span_pow_mul_span, pow_mem_pow, Ideal.pow_sup_eq_top', Ideal.iInf_pow_eq_bot_of_isLocalRing, TensorAlgebra.GradedAlgebra.ι_apply, AdicCompletion.val_add, Ideal.pow_sup_pow_eq_top', IsNoetherianRing.isNilpotent_nilradical, nat_power_gradedMonoid, Ideal.IsPrime.pow_le_iff, MvPolynomial.monomial_mem_homogeneousSubmodule_pow_degree, AdicCompletion.mk_smul_top_ofAlgEquiv_symm, AdicCompletion.val_one, IsArtinianRing.isNilpotent_jacobson_bot, Ideal.Factors.finrank_pow_ramificationIdx, Ideal.mem_iInf_smul_pow_eq_bot_iff, Ideal.Filtration.pow_smul_le, Hausdorffification.lift_comp_of, Ideal.rank_pow_quot_aux, AdicCompletion.surjective_evalₐ, Polynomial.exists_monic_aeval_eq_zero_forall_mem_pow_of_mem_map, Ideal.FG.isNilpotent_iff_le_nilradical, Ideal.map_algebraMap_eq_finset_prod_pow, PreTilt.exists_smodEq_untiltAux, AdicCompletion.transitionMap_map_pow, Ideal.rank_pow_quot, isArtinianRing_iff_isNilpotent_maximalIdeal, pow_eq_span_pow_set, exists_isInternal_prime_power_torsion, PreTilt.untiltAux_smodEq_untiltFun, MvPolynomial.coeffsIn_pow, AdicCompletion.val_sub, AdicCompletion.val_neg, Ideal.powQuotSuccInclusion_injective, IsLocalRing.isOpen_maximalIdeal_pow, Ideal.le_comap_pow, isInternal_prime_power_torsion, Ideal.iInf_pow_eq_bot_of_isDomain, AdicCompletion.transitionMap_ideal_mk, AdicCompletion.transitionMap_map_mul, Valued.integer.finite_quotient_maximalIdeal_pow_of_finite_residueField, CliffordAlgebra.iSup_ι_range_eq_top, IsCyclotomicExtension.Rat.map_eq_span_zeta_sub_one_pow, CliffordAlgebra.submodule_comap_pow_reverse, Polynomial.coeff_divByMonic_mem_pow_natDegree_mul, Hausdorffification.lift_of, comap_unop_pow, pow_eq_npowRec, Ideal.pow_right_strictAnti, Ideal.exists_mem_pow_notMem_pow_succ, mem_reesAlgebra_iff, IsDedekindDomain.HeightOneSpectrum.maxPowDividing_eq_pow_multiset_count, Ideal.IsTwoSided.pow_add, AdicCompletion.evalₐ_of, isPrecomplete_iff, map_pow, Ideal.eq_prime_pow_mul_coprime, pow_subset_pow, MvPolynomial.homogeneousSubmodule_one_pow, Ideal.Factors.finiteDimensional_quotient_pow, Ideal.le_pow_of_le_ramificationIdx, Ideal.pow_lt_self, AdicCompletion.eval_of, AdicCompletion.evalₐ_mk, AdicCompletion.evalₐ_mkₐ, Irreducible.maximalIdeal_pow_eq_closedBall_pow, is_ideal_adic_pow, isSemiprimaryRing_iff, Ideal.pow_mem_pow, Irreducible.maximalIdeal_pow_eq_setOf_le_v_coe_pow, Ideal.top_pow, AdicCompletion.val_zero, irreducible_pow_sup_of_le, Ideal.sup_pow_eq_top, Ideal.pow_eq_top_iff, AdicCompletion.mk_apply_coe, Ideal.iInf_pow_smul_eq_bot_of_isTorsionFree, IsDedekindDomain.exists_representative_mod_finset, AdicCompletion.transitionMap_comp_eval_apply, AdicCompletion.val_zero_apply, pow_succ', Ideal.mem_span_pow_iff_exists_isHomogeneous, IsArtinianRing.isNilpotent_nilradical, AdicCompletion.eval_surjective, isAdic_iff, Ideal.iInf_pow_smul_eq_bot_of_noZeroSMulDivisors, Ideal.Factors.piQuotientEquiv_mk, Ideal.finprod_not_dvd, AdicCompletion.transitionMap_map_one, pow_toAddSubmonoid, AdicCompletion.eval_apply, Ideal.map_pow, le_pow_toAddSubmonoid, IsDedekindDomain.quotientEquivPiFactors_mk, restrictScalars_pow, PrimeSpectrum.zeroLocus_pow, Ideal.hasBasis_nhds_adic, Ideal.relNorm_eq_pow_of_isMaximal, AdicCompletion.val_sum_apply, Ideal.span_singleton_pow, PowerSeries.IsWeierstrassDivisorAt.coeff_div_sub_seq_mem, Valuation.Integers.maximalIdeal_pow_eq_setOf_le_v_algebraMap_pow, FractionalIdeal.coeIdeal_pow, AdicCompletion.of_apply, WittVector.ghostComponentModPPow_map_mk, pow_one, Ideal.exists_pow_inf_eq_pow_smul, AdicCompletion.eval_comp_of, AdicCompletion.val_smul_apply, Ideal.le_comap_pow_ramificationIdx, LinearMap.exists_monic_and_coeff_mem_pow_and_aeval_eq_zero_of_range_le_smul, Ideal.Factors.piQuotientEquiv_map
|
instSMul 📖 | CompOp | 149 mathmath: AdicCompletion.val_sub_apply, Ideal.Filtration.submodule_eq_span_le_iff_stable_ge, Module.support_quotient, le_annihilator_iff, mem_ideal_smul_span_iff_exists_sum, AdicCompletion.AdicCauchySequence.mk_eq_mk, smul_eq_map₂, Ideal.iInf_pow_smul_eq_bot_of_isLocalRing, AdicCompletion.map_val_apply, Ideal.smul_top_eq_map, smul_bot, Module.isTorsionBySet_quotient_ideal_smul, ideal_span_singleton_smul, top_eq_ofList_cons_smul_iff, AdicCompletion.val_smul, mem_smul_span_singleton, AdicCompletion.incl_apply, Ideal.iInf_pow_smul_eq_bot_of_le_jacobson, AdicCompletion.val_smul_eq_evalₐ_smul, Ideal.Filtration.smul_le, Module.supportDim_add_length_eq_supportDim_of_isRegular, TensorProduct.quotTensorEquivQuotSMul_comp_mkQ_rTensor, smul_mono, IsLocalRing.map_mkQ_eq, mem_ideal_smul_span_iff_exists_sum', Ring.jacobson_smul_top_le, pow_smul_top_le, TensorProduct.tensorQuotEquivQuotSMul_comp_mkQ_lTensor, map_smul'', AdicCompletion.pi_apply_coe, Ideal.smul_eq_mul, RingTheory.Sequence.isWeaklyRegular_iff_Fin, AdicCompletion.val_add_apply, AdicCompletion.smul_eval, instSMulCommClass, Ideal.adic_module_basis, smul_subset_smul, Hausdorffification.instIsHausdorff, AdicCompletion.mkₐ_apply_coe, AdicCompletion.isAdicCauchy_iff, AdicCompletion.val_sum, IsHausdorff.iInf_pow_smul, AdicCompletion.range_eval, AdicCompletion.val_neg_apply, Module.Quotient.mk_smul_mk, bot_smul, AdicCompletion.transitionMap_comp_eval, annihilator_smul, jacobson_smul_lt_top, AdicCompletion.coe_eval, TensorProduct.tensorQuotEquivQuotSMul_tmul_mk, AdicCompletion.val_mul, localized₀_smul, SModEq.smul', Ideal.Filtration.Stable.exists_pow_smul_eq_of_ge, AdicCompletion.mk_smul_mk, smul_toAddSubmonoid, smul_iSup, RingTheory.Sequence.IsWeaklyRegular.regular_mod_prev, AdicCompletion.transitionMap_comp_reduceModIdeal, AdicCompletion.instIsScalarTowerQuotientIdealHSMulTopSubmodule, finite_quotient_smul, Ideal.Filtration.Stable.exists_pow_smul_eq, AdicCompletion.smul_mk, quotOfListConsSMulTopEquivQuotSMulTopInner_naturality, sup_smul, RingTheory.Sequence.isWeaklyRegular_append_iff', smul_le_right, Ideal.ker_tensorProductMk_quotient, TensorProduct.tensorQuotEquivQuotSMul_symm_mk, LinearMap.reduceModIdeal_apply, RingTheory.Sequence.isWeaklyRegular_append_iff, Ideal.Filtration.stable_iff_exists_pow_smul_eq_of_ge, Ideal.toCotangent_apply, Ideal.Filtration.pow_smul_le_pow_smul, Ideal.adic_basis, Ideal.stableFiltration_N, instCovariantClassHSMulLe_1, TensorProduct.quotTensorEquivQuotSMul_symm_mk, smul_sup, AdicCompletion.val_add, one_smul, AdicCompletion.mk_smul_top_ofAlgEquiv_symm, AdicCompletion.val_one, mem_smul_top_iff, smul_assoc, Ideal.mem_iInf_smul_pow_eq_bot_iff, Ideal.Filtration.pow_smul_le, Hausdorffification.lift_comp_of, Ideal.smul_restrictScalars, mem_smul_span, PreTilt.exists_smodEq_untiltAux, AdicCompletion.transitionMap_map_pow, iSup_smul, mul_smul, AdicCompletion.val_sub, IsHausdorff.eq_iff_smodEq, Ideal.range_finsuppTotal, RingTheory.Sequence.IsRegular.quot_ofList_smul_nontrivial, AdicCompletion.val_neg, smul_comap_le_comap_smul, AdicCompletion.transitionMap_ideal_mk, smul_le, AdicCompletion.transitionMap_map_mul, Ideal.ofList_cons_smul, Hausdorffification.lift_of, FG.jacobson_smul_lt, isPrecomplete_iff, top_smul, span_smul_eq, AdicCompletion.eval_of, map_range_rTensor_subtype_lid, coe_set_smul, TensorProduct.tensorQuotEquivQuotSMul_comp_mk, smul_mem_smul, instSMulCommClass_1, AdicCompletion.val_zero, AdicCompletion.mk_apply_coe, IsLocalRing.map_mkQ_eq_top, Ideal.iInf_pow_smul_eq_bot_of_isTorsionFree, RingTheory.Sequence.map_first_exact_on_four_term_right_exact_of_isSMulRegular_last, RingTheory.Sequence.isWeaklyRegular_iff, AdicCompletion.transitionMap_comp_eval_apply, comap_smul'', TensorProduct.quotTensorEquivQuotSMul_comp_mk, span_smul_span, AdicCompletion.val_zero_apply, index_smul_le, smul_top_le_comap_smul_top, AdicCompletion.eval_surjective, FG.smul, Ideal.iInf_pow_smul_eq_bot_of_noZeroSMulDivisors, localized'_smul, AdicCompletion.transitionMap_map_one, LinearMap.ker_tensorProductMk, AdicCompletion.eval_apply, TensorProduct.quotTensorEquivQuotSMul_symm_comp_mkQ, Algebra.Extension.Cotangent.ker_mk, AdicCompletion.val_sum_apply, AdicCompletion.of_apply, Ideal.exists_pow_inf_eq_pow_smul, AdicCompletion.eval_comp_of, restrictScalars_localized'_smul, AdicCompletion.val_smul_apply, smul_mono_left, TensorProduct.quotTensorEquivQuotSMul_mk_tmul, map_le_smul_top, TensorProduct.tensorQuotEquivQuotSMul_symm_comp_mkQ, instIsScalarTower
|
mapHom 📖 | CompOp | 2 mathmath: mapHom_id, mapHom_apply
|
moduleSet 📖 | CompOp | 3 mathmath: smul_le_smul, singleton_smul, setSemiring_smul_def
|
mul 📖 | CompOp | 187 mathmath: mul_one, HomogeneousIdeal.toIdeal_mul, Ideal.mul_eq_inf_of_coprime, cardQuot_mul, Ideal.IsTwoSided.pow_succ, Ideal.span_singleton_mul_le_span_singleton_mul, ClassGroup.mk0_eq_mk0_iff, IsLocalization.coeSubmodule_mul, ClassGroup.mk_eq_mk_of_coe_ideal, differentIdeal_eq_differentIdeal_mul_differentIdeal, Ideal.mul_le_right, mul_annihilator, Ideal.le_span_singleton_mul_iff, mul_comm, ProjectiveSpectrum.zeroLocus_mul_ideal, comap_op_mul, IsDedekindDomain.differentIdeal_eq_differentIdeal_mul_differentIdeal_of_isCoprime, MvPolynomial.weightedHomogeneousSubmodule_mul, mul_mem_mul, Ideal.span_singleton_mul_left_injective, mul_one_div_le_one, restrictScalars_mul, AlgebraicGeometry.Scheme.zeroLocus_mul, LinearDisjoint.op, val_mulMap'_tmul, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_apply, Ideal.iInf_mul, Ideal.mul_sup_eq_of_coprime_right, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_symm_apply, AlgebraicGeometry.Scheme.IdealSheafData.ideal_mul, FractionalIdeal.mk'_mul_coeIdeal_eq_coeIdeal, le_self_mul_one_div, le_div_iff_mul_le, Ideal.mul_comm, Ideal.map_mul, Ideal.isIdempotentElem_iff_eq_bot_or_top, Ideal.mul_bot, Ideal.smul_eq_mul, pow_add, Ideal.isIdempotentElem_iff_of_fg, map_unop_mul, annihilator_mul, iSup_mul, Ideal.span_singleton_mul_eq_span_singleton_mul, Ideal.inf_mul, Ideal.bot_mul, instPosMulStrictMonoIdeal, span_mul_span, Ideal.mul_left_self_sup, MvPolynomial.degreesLE_add, Subalgebra.isIdempotentElem_toSubmodule, IsFractional.mul, Ideal.span_singleton_mul_right_inj, Ideal.FG.mul, Ideal.eq_span_singleton_mul, Subalgebra.mul_toSubmodule, Ideal.mul_sup, instMulLeftMono, Polynomial.coeff_modByMonic_mem_pow_natDegree_mul, CliffordAlgebra.submodule_comap_mul_reverse, Ideal.mul_mono, pow_succ, mul_sup, mul_comm_of_commute, Algebra.FormallySmooth.iff_of_surjective, Ideal.sup_mul_right_self, Ideal.mul_le, Ideal.quotientMulEquivQuotientProd_snd, Ideal.fst_comp_quotientMulEquivQuotientProd, Ideal.span_mul_span', mem_mul_span_singleton, equivOpposite_apply, Subalgebra.mul_toSubmodule_le, MvPolynomial.coeffsIn_mul, Ideal.iSup_mul, FractionalIdeal.coeIdeal_mul, Ideal.le_mul_of_no_prime_factors, Ideal.mul_mem_mul, Ideal.mul_sup_eq_of_coprime_left, mul_smul_mul_eq_smul_mul_smul, Ideal.isCancelMulZero, Ideal.spanNorm_mul, FractionalIdeal.coe_mul, Ideal.span_mul_span, FractionalIdeal.mul_def, map_mul, le_traceDual, Ideal.IsPrime.mul_le, mul_toAddSubmonoid, mul_iSup, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_mul, Algebra.FormallyEtale.Algebra.FormallyEtale.iff_of_surjective, mem_span_singleton_mul, Ideal.span_singleton_mul_span_singleton, Ideal.sup_mul_inf, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_neg_mul, Ideal.snd_comp_quotientMulEquivQuotientProd, PrimeSpectrum.zeroLocus_mul, Ideal.mul_assoc, linearDisjoint_op, map_op_mul, Polynomial.coeff_divModByMonicAux_mem_span_pow_mul_span, Algebra.adjoin_union_coe_submodule, FG.mul, Ideal.span_singleton_mul_left_mono, bot_mul, Ideal.IsTwoSided.mul_one, Ideal.restrictScalars_mul, Ideal.sup_mul_eq_of_coprime_right, Ideal.mul_le_left, sup_mul, Ideal.span_singleton_mul_right_mono, Ideal.quotientMulEquivQuotientProd_fst, FractionalIdeal.spanSingleton_mul_coeIdeal_eq_coeIdeal, mulMap'_surjective, CliffordAlgebra.submodule_map_mul_reverse, mul_smul, CliffordAlgebra.evenOdd_mul_le, FractionalIdeal.mul_def', Ideal.top_mul, FractionalIdeal.instPosMulReflectLEIdealOfIsDedekindDomain, mul_subset_mul, MvPolynomial.restrictSupport_add, Ideal.associatesEquivIsPrincipal_mul, Ideal.mul_le_inf, instMulPosStrictMonoIdeal, mul_eq_map₂, mul_le, Ideal.sup_mul_eq_of_coprime_left, Ideal.mul_iSup, PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal, Polynomial.coeff_divByMonic_mem_pow_natDegree_mul, Ideal.mul_mem_mul_rev, pow_eq_npowRec, one_mul, Ideal.span_singleton_mul_left_inj, span_singleton_mul, Ideal.mem_mul_span_singleton, Ideal.IsTwoSided.pow_add, conductor_mul_differentIdeal, Ideal.eq_prime_pow_mul_coprime, Ideal.mul_mono_left, LinearDisjoint.val_mulMap_tmul, Ideal.mul_iInf, Ideal.spanNorm_mul_spanNorm_le, mul_eq_span_mul_set, Ideal.instNoZeroDivisors, Ideal.span_singleton_mul_right_injective, setSemiring_smul_def, equivOpposite_symm_apply, le_traceDual_mul_iff, Module.Flat.top_mul_submoduleAlgebra, Ideal.mem_span_singleton_mul, Ideal.mul_top, Ideal.isIdempotentElem_iff_eq_bot_or_top_of_isLocalRing, mulMap_op, Ideal.inf_eq_mul_of_isCoprime, Ideal.mul_inf, ClassGroup.mk0_eq_mk0_inv_iff, Polynomial.contentIdeal_mul_le_mul_contentIdeal, MvPolynomial.homogeneousSubmodule_mul, Ideal.IsHomogeneous.mul, Ideal.spanNorm_mul_of_bot_or_top, Ideal.mul_mono_right, Algebra.FormallyEtale.iff_of_surjective, instMulRightMono, pow_succ', mul_def, Ideal.sup_mul, Ideal.IsTwoSided.instHMul, Ideal.le_comap_mul, mulMap_range, Ideal.span_pair_mul_span_pair, cardQuot_mul_of_coprime, PowerSeries.coeff_mul_mem_ideal_mul_ideal_of_coeff_mem_ideal', Ideal.sup_mul_left_self, Ideal.mul_right_self_sup, Polynomial.mul_contentIdeal_le_radical_contentIdeal_mul, Ideal.mul_eq_bot, le_traceDual_iff_map_le_one, mul_mem_mul_rev, Ideal.radical_mul, comap_unop_mul, WeierstrassCurve.Affine.CoordinateRing.XYIdeal_mul_XYIdeal, mul_bot, Ideal.span_singleton_mul_le_iff, Ideal.cotangent_subsingleton_iff
|
one 📖 | CompOp | 58 mathmath: mul_one, pow_zero, algebraMap_mem, Ideal.one_eq_top, mul_one_div_le_one, one_le_traceDual_one, Ideal.isCoprime_iff_gcd, Algebra.toSubmodule_bot, coeSubmodule_differentIdeal, coeSubmodule_differentIdeal_fractionRing, traceDual_top', le_one_toAddSubmonoid, one_le_one_div, span_singleton_algebraMap_of_isUnit, LinearDisjoint.one_left, differentialIdeal_le_iff, FractionalIdeal.coe_dual_one, CliffordAlgebra.one_le_evenOdd_zero, LinearMap.BilinForm.mem_dualSubmodule, TensorAlgebra.ι_range_disjoint_one, ExteriorAlgebra.ι_range_disjoint_one, traceDual_le_span_map_traceDual, MvPolynomial.homogeneousSubmodule_zero, MvPolynomial.restrictSupport_zero, FractionalIdeal.coe_one, differentialIdeal_le_fractionalIdeal_iff, Ideal.add_eq_one_iff, Ideal.isCoprime_tfae, MvPolynomial.degreesLE_zero, le_traceDual, FractionalIdeal.coeIdeal_eq_one, one_eq_span_one_set, Polynomial.coeff_divModByMonicAux_mem_span_pow_mul_span, Ideal.finite_mulSupport, Ideal.IsTwoSided.mul_one, one_smul, smul_one_eq_span, traceDual_eq_span_map_traceDual_of_linearDisjoint, mem_one, map_unop_one, span_singleton_eq_one_iff, pow_eq_npowRec, one_mul, Ideal.isCoprime_iff_add, LinearDisjoint.one_right, comap_unop_one, one_le, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_map_one, one_eq_range, comap_op_one, map_op_one, IsLocalization.coeSubmodule_top, map_one, toSubMulAction_one, le_traceDual_iff_map_le_one, Ideal.associatesEquivIsPrincipal_map_one, IsCoprime.add_eq, one_eq_span
|
pointwiseMulSemiringAction 📖 | CompOp | — |
spanSingleton 📖 | CompOp | 9 mathmath: ker_unitsToPic, spanSingleton_apply, unitsQuotEquivRelPic_symm_apply, ClassGroup.equivPic_symm_apply, mker_spanSingleton, mulExact_unitsMap_spanSingleton_unitsToPic, ClassGroup.equivPic_apply, ker_unitsMap_spanSingleton, unitsQuotEquivRelPic_apply_coe
|