Operations

📁 Source: Mathlib/Algebra/Algebra/Operations.lean

Statistics

Metric	Count
Definitions equivOpposite, hasDistribPointwiseNeg, idemSemiring, instAddCommMonoidWithOne, instDiv, instIdemCommSemiring, instNonUnitalSemiring, instPowNat, instSMul, mapHom, moduleSet, mul, one, pointwiseMulSemiringAction, ringHom, spanSingleton	16
Theorems algebraMap_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_image_smul_eq, 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	125
Total	141

SubMulAction

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_mem 📖	mathematical	—	SubMulAction Algebra.toSMul SetLike.instMembership instSetLike instOne MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Module.toDistribMulAction Algebra.toModule AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	Algebra.algebraMap_eq_smul_one
mem_one' 📖	mathematical	—	SubMulAction Algebra.toSMul SetLike.instMembership instSetLike instOne MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring DistribMulAction.toMulAction AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Module.toDistribMulAction Algebra.toModule AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	Algebra.algebraMap_eq_smul_one

Submodule

Definitions

Name	Category	Theorems
equivOpposite 📖	CompOp	5 math math: LinearDisjoint.op, equivOpposite_apply, linearDisjoint_op, equivOpposite_symm_apply, mulMap_op
hasDistribPointwiseNeg 📖	CompOp	—
idemSemiring 📖	CompOp	282 math math: Ideal.toCotangent_to_quotient_square, Ideal.radical_sup, DoubleQuot.liftSupQuotQuotMkₐ_toRingHom, FractionalIdeal.finprod_heightOneSpectrum_factorization_principal, Ideal.finite_setOf_absNorm_le₀, Ideal.hasFiniteMulSupport_coe, 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, 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, NumberField.HeightOneSpectrum.NumberField.toNNReal_valued_eq_adicAbv, DoubleQuot.coe_quotLeftToQuotSupₐ, AdicCompletion.incl_apply, FractionalIdeal.count_well_defined, Ideal.associatesNonZeroDivisorsEquivIsPrincipal_apply, NumberField.HeightOneSpectrum.rankOne_hom'_def, 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', irreducible_pow_sup_of_ge, ClassGroup.mk0_eq_one_iff, 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, NumberField.HeightOneSpectrum.adicAbv_def, 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, Ring.HasFiniteQuotients.finite_absNorm_heightOneSpectrum_le, NumberField.HeightOneSpectrum.NumberField.rankOne_hom'_def, Ideal.instIsScalarTowerQuotientHPowKerRingHomAlgebraMapOfNat, Ring.HasFiniteQuotients.finite_absNorm_le, 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, KummerDedekind.emultiplicity_factors_map_eq_emultiplicity, AdicCompletion.factorₐ_evalₐ_one, DoubleQuot.ker_quotQuotMk, Ideal.span_singleton_nonZeroDivisors, DoubleQuot.coe_quotQuotEquivQuotSupₐ, NumberField.FinitePlace.IsDedekindDomain.HeightOneSpectrum.embedding_mul_absNorm, 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, NumberField.HeightOneSpectrum.embedding_mul_absNorm, Int.absNorm_under_mem, unitsToPic_apply, Ideal.spanNorm_eq, FractionalIdeal.absNorm_eq, DoubleQuot.coe_quotQuotEquivQuotSupₐ_symm, range_unitsToPic, Ideal.relNorm_algebraMap, spanSingleton_apply, IsCoprime.sup_eq, irreducible_pow_sup, 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, KummerDedekind.Ideal.irreducible_map_of_irreducible_minpoly, Ideal.cotangentEquivIdeal_apply, Ideal.exists_subset_radical_span_sup_of_subset_radical_sup, 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, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm, FractionalIdeal.coe_sup, NumberField.exists_ideal_in_class_of_norm_le, instInvertibleSubtypeMemVal, NumberField.Ideal.tendsto_norm_le_div_atTop, Ideal.irreducible_of_irreducible_absNorm, TrivSqZeroExt.kerIdeal_sq, Ideal.count_associates_eq, Ideal.cotangentToQuotientSquare_injective, Ideal.natAbs_det_equiv, emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity, Ideal.absNorm_eq_one_iff, DoubleQuot.quotQuotEquivQuotSup_quotQuotMk, NumberField.mixedEmbedding.fundamentalCone.idealSetEquiv_symm_apply, NumberField.torsionOrder_dvd_absNorm_sub_one, Ideal.radical_pow, instIsOrderedRing, Algebra.Generators.ker_comp_eq_sup, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.one_lt_absNorm_nnreal, MvPolynomial.coeffsIn_pow, Ideal.span_singleton_mem_isPrincipalSubmonoid, IsHausdorff.eq_iff_smodEq, DoubleQuot.coe_quotQuotToQuotSupₐ, Ideal.primaryComponent_mem, 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, Ideal.sup_prod_eq_top, AlgHom.ker_kerSquareLift, Ideal.mem_isPrincipalSubmonoid_iff, Ideal.span_singleton_absNorm, ClassGroup.exists_min, NumberField.HeightOneSpectrum.NumberField.RingOfIntegers.HeightOneSpectrum.adicAbv_def, 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, Ideal.IsDedekindDomain.emultiplicity_map_eq_zero_of_ne, NumberField.HeightOneSpectrum.one_lt_absNorm, 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, RatFunc.valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one, 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, irreducible_pow_sup_of_le, 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, NumberField.HeightOneSpectrum.toNNReal_valued_eq_adicAbv, span.ringHom_apply, NumberField.FinitePlace.norm_embedding', Ideal.absNorm_relNorm, ClassGroup.equivPic_apply, Int.absNorm_under_eq_sInf, Ideal.absNorm_span_singleton, FractionalIdeal.coeIdeal_absNorm, Ideal.prod_sup_eq_top, 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, Ideal.hasFiniteMulSupport_inv, FractionalIdeal.finprod_heightOneSpectrum_factorization_principal_fraction, Ideal.span_singleton_absNorm_le, Ideal.finprod_not_dvd, Ideal.natAbs_det_basis_change, IsLocalRing.finite_quotient_iff, NumberField.HeightOneSpectrum.one_lt_absNorm_nnreal, 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, NumberField.FinitePlace.norm_embedding_int, 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, NumberField.FinitePlace.norm_def, Ideal.relNorm_comap_algEquiv, Ideal.to_quotient_square_comp_toCotangent, fg_unit, emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_eq_emultiplicity, Ideal.sup_multiset_prod_eq_top, unitsQuotEquivRelPic_apply_coe, derivationQuotKerSq_mk, Ideal.IsDedekindDomain.emultiplicity_map_eq_ramificationIdx_mul, NumberField.mixedEmbedding.fundamentalCone.intNorm_idealSetEquiv_apply, Ideal.absNorm_dvd_norm_of_mem
instAddCommMonoidWithOne 📖	CompOp	77 math math: 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, IsDecompositionField.toIsGaloisGroup, Ideal.card_stabilizer_eq, mem_smul_iff_inv_mul_mem, FractionalIdeal.coe_nsmul, Ideal.stabilizerEquiv_symm_apply_smul, FractionalIdeal.coe_natCast, Ideal.IsPrime.smul_iff, spinGroup.conjAct_smul_range_ι, Ideal.Quotient.smul_top, isDecompositionField_iff, traceForm_dualSubmodule_adjoin, Ideal.Quotient.stabilizerHom_surjective_of_profinite, Ideal.inertia_le_stabilizer, Algebra.IsInvariant.orbit_eq_primesOver, Ideal.Quotient.stabilizerHomSurjectiveAuxFunctor_aux, 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, instIsDecompositionFieldSubtypeMemIntermediateFieldIntermediateFieldAlgEquivSubgroupStabilizerIdealOfIsGalois, mul_smul_mul_eq_smul_mul_smul, singleton_smul, Ideal.coe_smul_primesOver_mk, pinGroup.conjAct_smul_range_ι, IsCyclotomicExtension.Rat.galEquivZMod_stabilizer, Ideal.quotOfMul_surjective, Ideal.pointwise_smul_eq_comap, Ideal.IsPrime.smul, IsFractionRing.stabilizerHom_apply_apply_mk, 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, Ideal.stabilizerEquiv_apply_smul, instIsScalarTower, Ideal.mulQuot_injective
instDiv 📖	CompOp	17 math math: mul_one_div_le_one, FractionalIdeal.isFractional_div_of_ne_zero, one_mem_div, le_self_mul_one_div, le_div_iff_mul_le, mem_div_iff_forall_mul_mem, FractionalIdeal.div_of_ne_zero, coeSubmodule_differentIdeal, coeSubmodule_differentIdeal_fractionRing, one_le_one_div, IsFractional.div_of_nonzero, FractionalIdeal.coe_inv_of_ne_zero, le_div_iff, FractionalIdeal.coe_div, mem_div_iff_smul_subset, map_div, FractionalIdeal.inv_of_ne_zero
instIdemCommSemiring 📖	CompOp	25 math math: 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.isCoprime_biInf, Ideal.sup_prod_eq_top, Ideal.isCoprime_span_singleton_iff, Ideal.isCoprime_iff_add, Ideal.prod_eq_iInf_of_pairwise_isCoprime, 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	28 math math: 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, pow_sub_one_dvd_differentIdeal, 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, idealFactorsEquivOfQuotEquiv_is_dvd_iso, idealFactorsFunOfQuotHom_id, idealFactorsFunOfQuotHom_coe_coe, not_dvd_differentIdeal_of_intTrace_not_mem, Ideal.dvd_span_singleton, Ideal.finprod_not_dvd, pow_sub_one_dvd_differentIdeal_aux
instPowNat 📖	CompOp	288 math math: Ideal.exists_pow_le_of_le_radical_of_fg_radical, Polynomial.coeff_prod_mem_ideal_pow_tsub, AdicCompletion.val_sub_apply, pow_zero, IsAdicComplete.StrictMono.mk_liftRingHom, Ideal.IsTwoSided.pow_succ, AdicCompletion.AdicCauchySequence.mk_eq_mk, Ideal.iInf_pow_smul_eq_bot_of_isLocalRing, SModEq.pow_pow_add_one, 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, AdicCompletion.exists_smodEq_pow_smul_top_and_smodEq_pow_add_one_smul_top, Ideal.IsPrime.mem_pow_mul, span_pow, IsAdicComplete.mkQ_comp_lift, 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_sub_one_dvd_differentIdeal, 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.ofPowSMul_ofValEqZero, AdicCompletion.smul_eval, WittVector.mk_pow_fontaineTheta, Ideal.adic_module_basis, FractionalIdeal.coe_pow, AdicCompletion.factor_eval_eq_evalₐ, Ideal.powQuotSuccInclusion_apply_coe, IsAdicComplete.StrictMono.factorPow_comp_eq_of_factorPow_comp_succ_eq', isInternal_prime_power_torsion_of_is_torsion_by_ideal, Ideal.IsPrime.mul_mem_pow, AlgebraicGeometry.Scheme.IdealSheafData.ideal_pow, IsAdicComplete.StrictMono.mk_comp_liftRingHom, IsDedekindDomain.HeightOneSpectrum.isCoprime_pow_of_ne, 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', Ideal.eq_prime_pow_of_succ_lt_of_le, AdicCompletion.transitionMap_comp_eval, Associates.le_singleton_iff, Ideal.quotientToQuotientRangePowQuotSucc_mk, 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, IsDedekindDomain.inf_pow_eq_prod_of_prime, AdicCompletion.factorₐ_evalₐ_one, map_unop_pow, Ideal.exists_radical_pow_le_of_fg, SModEq.pow_add_one, AdicCompletion.val_mul, MvPolynomial.mem_pow_idealOfVars_iff', Ideal.Filtration.Stable.exists_pow_smul_eq_of_ge, IsAdicComplete.StrictMono.factorPow_comp_eq_of_factorPow_comp_succ_eq, 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, AdicCompletion.ofPowSMul_injective, Ideal.IsMaximal.mem_pow_mul, Ideal.pow_right_mono, Ideal.isOpen_pow_of_isMaximal, map_op_pow, MvPolynomial.le_coeffsIn_pow, Ideal.Quotient.isUnit_mk_pow_iff_isUnit_mk, Ideal.Filtration.Stable.exists_pow_smul_eq, AdicCompletion.smul_mk, AdicCompletion.exists_smodEq_pow_add_one_smul, Perfection.teichmullerFun_sModEq, Perfection.teichmuller_sModEq, Ideal.quotientToQuotientRangePowQuotSucc_surjective, WittVector.ker_map_le_ker_mk_comp_ghostComponent, Perfection.teichmuller₀_sModEq, WittVector.fontaineThetaModPPow_teichmuller, factorPowSucc.isUnit_of_isUnit_image, AdicCompletion.pow_smul_top_eq_ker_eval, Ideal.hasBasis_nhds_zero_adic, Ideal.relNorm_algebraMap, irreducible_pow_sup, FG.pow, AdicCompletion.val_apply_mem_smul_top_iff, 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, AdicCompletion.ofPowSMul_val_apply_eq_zero, Ideal.pow_le_pow_right, Ideal.Filtration.stable_iff_exists_pow_smul_eq_of_ge, PowerSeries.IsWeierstrassDivisorAt.coeff_seq_mem, IsAdicComplete.mk_liftAlgHom, Ideal.Filtration.pow_smul_le_pow_smul, MvPolynomial.restrictSupport_nsmul, AdicCompletion.pow_smul_top_le_ker_eval, IsAdicComplete.mkₐ_comp_liftAlgHom, IsDedekindDomain.inf_prime_pow_eq_prod, exists_maximalIdeal_pow_eq_of_principal, Ideal.quotientToQuotientRangePowQuotSucc_injective, range_powSMulQuotInclusion, 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, Ideal.mul_add_mem_pow_succ_inj, torsionBySet_le_torsionBySet_pow, TensorAlgebra.GradedAlgebra.ι_apply, AdicCompletion.val_add, Ideal.pow_sup_pow_eq_top', Ideal.IsMaximal.mul_mem_pow, 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, IsAdicComplete.mk_liftRingHom, IsArtinianRing.isNilpotent_jacobson_bot, AdicCompletion.factor_eval_liftRingHom, 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, Perfection.exists_teichmullerFun, AdicCompletion.evalₐ_liftAlgHom, 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, AdicCompletion.transitionMap_map_pow, powSMulQuotInclusion_mk, Ideal.rank_pow_quot, isArtinianRing_iff_isNilpotent_maximalIdeal, pow_eq_span_pow_set, exists_isInternal_prime_power_torsion, Ideal.exists_mul_add_mem_pow_succ, factorPow_comp_powSMulQuotInclusion, MvPolynomial.coeffsIn_pow, AdicCompletion.val_sub, AdicCompletion.restrictScalars_range_ofPowSMul_eq_ker_eval, Ideal.Quotient.isUnit_mk_pow_iff_notMem, IsPrecomplete.prec, 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, IsPrecomplete.prec', 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, IsAdicComplete.StrictMono.factorPow_comp_extend, IsDedekindDomain.HeightOneSpectrum.maxPowDividing_eq_pow_multiset_count, Ideal.IsTwoSided.pow_add, WittVector.quotEquivOfEq_ghostComponentModPPow, AdicCompletion.evalₐ_of, isPrecomplete_iff, map_pow, Ideal.eq_prime_pow_mul_coprime, pow_subset_pow, IsAdicComplete.mk_lift, AdicCompletion.factor_evalₐ_eq_eval, MvPolynomial.homogeneousSubmodule_one_pow, AdicCompletion.evalₐ_comp_liftRingHom, 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.eval_lift_apply, Ideal.IsMaximal.exists_inv_pow, AdicCompletion.val_zero_apply, pow_succ', IsAdicComplete.mk_comp_liftRingHom, powSMulQuotInclusion_injective, Ideal.quotientToQuotientRangePowQuotSuccAux_mk, Ideal.mem_span_pow_iff_exists_isHomogeneous, IsArtinianRing.isNilpotent_nilradical, AdicCompletion.eval_surjective, AdicCompletion.ofPowSMul_val_apply, isAdic_iff, Ideal.iInf_pow_smul_eq_bot_of_noZeroSMulDivisors, Ideal.Factors.piQuotientEquiv_mk, Ideal.finprod_not_dvd, AdicCompletion.transitionMap_map_one, pow_sub_one_dvd_differentIdeal_aux, pow_toAddSubmonoid, AdicCompletion.eval_apply, Ideal.map_pow, le_pow_toAddSubmonoid, IsDedekindDomain.quotientEquivPiFactors_mk, AdicCompletion.exists_smodEq_pow_smul_top_and_mkQ_eq, restrictScalars_pow, PrimeSpectrum.zeroLocus_pow, Ideal.hasBasis_nhds_adic, Ideal.relNorm_eq_pow_of_isMaximal, AdicCompletion.val_sum_apply, AdicCompletion.evalOneₐ_liftAlgHom, Ideal.span_singleton_pow, PowerSeries.IsWeierstrassDivisorAt.coeff_div_sub_seq_mem, AdicCompletion.evalₐ_liftRingHom, IsAdicComplete.StrictMono.mkQ_comp_lift, Perfection.teichmullerAux_sModEq, Valuation.Integers.maximalIdeal_pow_eq_setOf_le_v_algebraMap_pow, FractionalIdeal.coeIdeal_pow, AdicCompletion.of_apply, WittVector.ghostComponentModPPow_map_mk, IsAdicComplete.StrictMono.mk_lift, 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, AdicCompletion.eval_lift, IsDedekindDomain.HeightOneSpectrum.inf_pow_eq_prod
instSMul 📖	CompOp	187 math math: 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, sup_eq_sup_smul_of_le_smul_of_le_jacobson, 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, AdicCompletion.exists_smodEq_pow_smul_top_and_smodEq_pow_add_one_smul_top, Module.supportDim_add_length_eq_supportDim_of_isRegular, IsAdicComplete.mkQ_comp_lift, TensorProduct.quotTensorEquivQuotSMul_comp_mkQ_rTensor, smul_mono, IsLocalRing.map_mkQ_eq, mem_ideal_smul_span_iff_exists_sum', Ring.jacobson_smul_top_le, comap_smul_top_of_surjective, 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.ofPowSMul_ofValEqZero, AdicCompletion.smul_eval, TensorProduct.quotTensorEquivQuotSMul_mk_one_tmul, instSMulCommClass, Ideal.adic_module_basis, AdicCompletion.factor_eval_eq_evalₐ, smul_subset_smul, Hausdorffification.instIsHausdorff, AdicCompletion.mkₐ_apply_coe, AdicCompletion.isAdicCauchy_iff, AdicCompletion.val_sum, IsHausdorff.iInf_pow_smul, eq_smul_of_le_smul_of_le_jacobson, AdicCompletion.range_eval, AdicCompletion.val_neg_apply, Module.Quotient.mk_smul_mk, bot_smul, AdicCompletion.transitionMap_comp_eval, restrictScalars_map_smul_eq, 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, IsAdicComplete.StrictMono.factorPow_comp_eq_of_factorPow_comp_succ_eq, AdicCompletion.mk_smul_mk, smul_toAddSubmonoid, smul_iSup, RingTheory.Sequence.IsWeaklyRegular.regular_mod_prev, AdicCompletion.transitionMap_comp_reduceModIdeal, AdicCompletion.instIsScalarTowerQuotientIdealHSMulTopSubmodule, AdicCompletion.ofPowSMul_injective, finite_quotient_smul, Ideal.Filtration.Stable.exists_pow_smul_eq, AdicCompletion.smul_mk, AdicCompletion.exists_smodEq_pow_add_one_smul, quotOfListConsSMulTopEquivQuotSMulTopInner_naturality, sup_smul, AdicCompletion.pow_smul_top_eq_ker_eval, RingTheory.Sequence.isWeaklyRegular_append_iff', smul_le_right, Ideal.ker_tensorProductMk_quotient, AdicCompletion.val_apply_mem_smul_top_iff, TensorProduct.tensorQuotEquivQuotSMul_symm_mk, LinearMap.reduceModIdeal_apply, RingTheory.Sequence.isWeaklyRegular_append_iff, AdicCompletion.ofPowSMul_val_apply_eq_zero, instFiniteQuotientIdealHSMulTop, Ideal.Filtration.stable_iff_exists_pow_smul_eq_of_ge, Ideal.toCotangent_apply, Ideal.Filtration.pow_smul_le_pow_smul, AdicCompletion.pow_smul_top_le_ker_eval, range_powSMulQuotInclusion, 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, exists_injOn_mkQ_image_span_eq_of_span_eq_map_mkQ_of_le_jacobson_bot, smul_assoc, AdicCompletion.factor_eval_liftRingHom, Ideal.mem_iInf_smul_pow_eq_bot_iff, Ideal.Filtration.pow_smul_le, Hausdorffification.lift_comp_of, Ideal.smul_restrictScalars, Perfection.exists_teichmullerFun, mem_smul_span, AdicCompletion.transitionMap_map_pow, powSMulQuotInclusion_mk, iSup_smul, mul_smul, factorPow_comp_powSMulQuotInclusion, AdicCompletion.val_sub, IsHausdorff.eq_iff_smodEq, AdicCompletion.restrictScalars_range_ofPowSMul_eq_ker_eval, Ideal.range_finsuppTotal, RingTheory.Sequence.IsRegular.quot_ofList_smul_nontrivial, IsPrecomplete.prec, AdicCompletion.val_neg, smul_comap_le_comap_smul, AdicCompletion.transitionMap_ideal_mk, smul_le, AdicCompletion.transitionMap_map_mul, IsPrecomplete.prec', Ideal.ofList_cons_smul, smul_le_of_le_smul_of_le_jacobson_bot, Hausdorffification.lift_of, IsAdicComplete.StrictMono.factorPow_comp_extend, FG.jacobson_smul_lt, isPrecomplete_iff, IsAdicComplete.mk_lift, top_smul, AdicCompletion.factor_evalₐ_eq_eval, 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.eval_lift_apply, AdicCompletion.val_zero_apply, index_smul_le, smul_top_le_comap_smul_top, powSMulQuotInclusion_injective, AdicCompletion.eval_surjective, AdicCompletion.ofPowSMul_val_apply, FG.smul, Ideal.iInf_pow_smul_eq_bot_of_noZeroSMulDivisors, localized'_smul, AdicCompletion.transitionMap_map_one, LinearMap.ker_tensorProductMk, sup_smul_eq_sup_smul_of_le_smul_of_le_jacobson, AdicCompletion.eval_apply, TensorProduct.quotTensorEquivQuotSMul_symm_comp_mkQ, AdicCompletion.exists_smodEq_pow_smul_top_and_mkQ_eq, Algebra.Extension.Cotangent.ker_mk, AdicCompletion.val_sum_apply, IsAdicComplete.StrictMono.mkQ_comp_lift, IsLocalRing.spanFinrank_eq_finrank_quotient, AdicCompletion.of_apply, IsAdicComplete.StrictMono.mk_lift, 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, AdicCompletion.eval_lift
mapHom 📖	CompOp	2 math math: mapHom_id, mapHom_apply
moduleSet 📖	CompOp	3 math math: smul_le_smul, singleton_smul, setSemiring_smul_def
mul 📖	CompOp	194 math math: 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, top_mul_eq_top_of_mul_eq_one, 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_eq_inf_of_isCoprime, 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, SModEq.pow_mul_of_le, 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.inf_eq_mul_of_pure, 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, Ideal.isIdempotentElem_of_pure, 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, mul_top_eq_top_of_mul_eq_one, 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, injective_lTensor_quotient_iff_inf_eq_mul, 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	60 math math: mul_one, pow_zero, algebraMap_mem, Ideal.one_eq_top, mul_one_div_le_one, one_le_traceDual_one, le_self_mul_one_div, 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, Ideal.hasFiniteMulSupport, 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 math math: 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

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
algebraMap_mem 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SetLike.instMembership setLike one DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	RingHomSurjective.ids one_eq_range
bot_mul 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring mul Bot.bot instBot	—	bot_smul
bot_pow 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instPowNat Bot.bot instBot	—	pow_one pow_succ bot_mul
bot_smul 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSMul Bot.bot instBot	—	le_bot_iff smul_le zero_smul ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass addSubmonoidClass
coe_set_smul 📖	mathematical	—	Set Submodule pointwiseSetSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SetLike.coe NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring setLike instSMul	—	set_smul_eq_of_le smul_mem_smul smul_le mem_set_smul_of_mem_mem
comap_op_mul 📖	mathematical	—	comap MulOpposite CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulOpposite.instAddCommMonoid Algebra.toModule MulOpposite.instModule RingHom.id LinearEquiv.toLinearMap RingHomInvPair.ids MulOpposite.opLinearEquiv Submodule mul MulOpposite.instSemiring IsScalarTower.right MulOpposite.instAlgebra	—	RingHomInvPair.ids IsScalarTower.right RingHomSurjective.invPair comap_equiv_eq_map_symm RingHomSurjective.ids map_unop_mul
comap_op_one 📖	mathematical	—	comap MulOpposite CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulOpposite.instAddCommMonoid Algebra.toModule MulOpposite.instModule RingHom.id LinearEquiv.toLinearMap RingHomInvPair.ids MulOpposite.opLinearEquiv Submodule one MulOpposite.instSemiring	—	ext RingHomInvPair.ids
comap_op_pow 📖	mathematical	—	comap MulOpposite CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulOpposite.instAddCommMonoid Algebra.toModule MulOpposite.instModule RingHom.id LinearEquiv.toLinearMap RingHomInvPair.ids MulOpposite.opLinearEquiv Submodule instPowNat MulOpposite.instSemiring IsScalarTower.right MulOpposite.instAlgebra	—	MulOpposite.op_injective RingHomInvPair.ids IsScalarTower.right RingEquiv.map_pow
comap_unop_mul 📖	mathematical	—	comap MulOpposite CommSemiring.toSemiring MulOpposite.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulOpposite.instModule Algebra.toModule RingHom.id LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm MulOpposite.opLinearEquiv Submodule mul IsScalarTower.right MulOpposite.instSemiring MulOpposite.instAlgebra	—	RingHomInvPair.ids IsScalarTower.right RingHomSurjective.invPair RingHomSurjective.ids map_op_mul
comap_unop_one 📖	mathematical	—	comap MulOpposite CommSemiring.toSemiring MulOpposite.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulOpposite.instModule Algebra.toModule RingHom.id LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm MulOpposite.opLinearEquiv Submodule one MulOpposite.instSemiring	—	RingHomInvPair.ids RingHomSurjective.invPair map_equiv_eq_comap_symm RingHomSurjective.ids map_op_one
comap_unop_pow 📖	mathematical	—	comap MulOpposite CommSemiring.toSemiring MulOpposite.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulOpposite.instModule Algebra.toModule RingHom.id LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm MulOpposite.opLinearEquiv Submodule instPowNat IsScalarTower.right MulOpposite.instSemiring MulOpposite.instAlgebra	—	RingEquiv.map_pow IsScalarTower.right
equivOpposite_apply 📖	mathematical	—	DFunLike.coe RingEquiv Submodule MulOpposite CommSemiring.toSemiring MulOpposite.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulOpposite.instModule Algebra.toModule mul MulOpposite.instSemiring IsScalarTower.right MulOpposite.instAlgebra MulOpposite.instMul pointwiseAdd MulOpposite.instAdd EquivLike.toFunLike RingEquiv.instEquivLike equivOpposite MulOpposite.op comap RingHom.id LinearEquiv.toLinearMap MulOpposite.opLinearEquiv	—	IsScalarTower.right
equivOpposite_symm_apply 📖	mathematical	—	DFunLike.coe RingEquiv MulOpposite Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule MulOpposite.instAddCommMonoid MulOpposite.instModule MulOpposite.instMul mul IsScalarTower.right MulOpposite.instSemiring MulOpposite.instAlgebra MulOpposite.instAdd pointwiseAdd EquivLike.toFunLike RingEquiv.instEquivLike RingEquiv.symm equivOpposite comap RingHom.id LinearEquiv.toLinearMap LinearEquiv.symm MulOpposite.opLinearEquiv MulOpposite.unop	—	IsScalarTower.right
iSup_mul 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring mul iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	—	iSup_smul
iSup_smul 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSMul iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	—	le_antisymm smul_le iSup_induction mem_iSup_of_mem smul_mem_smul zero_smul ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass addSubmonoidClass add_smul AddMemClass.add_mem AddSubmonoidClass.toAddMemClass iSup_le smul_mono_left le_iSup
instCovariantClassHSMulLe_1 📖	mathematical	—	CovariantClass Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSMul Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	smul_mono le_rfl
instIsOrderedRing 📖	mathematical	—	IsOrderedRing Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule IdemSemiring.toSemiring idemSemiring instPartialOrder	—	instIsOrderedAddMonoid CanonicallyOrderedAdd.toZeroLEOneClass instCanonicallyOrderedAdd MulLeftMono.toPosMulMono instMulLeftMono IsScalarTower.right MulRightMono.toMulPosMono instMulRightMono
instIsScalarTower 📖	mathematical	—	IsScalarTower Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction instSMul Semiring.toModule IsScalarTower.right	—	IsScalarTower.right span_eq smul_span smul_eq_mul span_mul_span smul_mul_assoc Set.isScalarTower'
instMulLeftMono 📖	mathematical	—	MulLeftMono Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring mul Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	smul_mono_right instCovariantClassHSMulLe_1
instMulRightMono 📖	mathematical	—	MulRightMono Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring mul Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	smul_mono_left
instSMulCommClass 📖	mathematical	—	SMulCommClass Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction instSMul Semiring.toModule IsScalarTower.right	—	IsScalarTower.right span_eq smul_span smul_eq_mul span_mul_span mul_smul_comm Set.smulCommClass_set'
instSMulCommClass_1 📖	mathematical	—	SMulCommClass Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instSMul Semiring.toModule IsScalarTower.right SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction	—	SMulCommClass.symm IsScalarTower.right instSMulCommClass
ker_unitsMap_spanSingleton 📖	mathematical	—	MonoidHom.ker Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero Units.instGroup Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule IdemSemiring.toSemiring idemSemiring Units.instMulOneClass Units.map MonoidWithZeroHom.toMonoidHom NonAssocSemiring.toMulZeroOneClass spanSingleton MonoidHom.range RingHom.toMonoidHom algebraMap	—	Subgroup.ext MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass span_singleton_eq_one_iff
le_div_iff 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder instPartialOrder instDiv SetLike.instMembership setLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
le_div_iff_mul_le 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder instPartialOrder instDiv mul IsScalarTower.right	—	IsScalarTower.right le_div_iff mul_le
le_one_toAddSubmonoid 📖	mathematical	—	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Preorder.toLE PartialOrder.toPreorder AddSubmonoid.instPartialOrder AddSubmonoid.one AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne toAddSubmonoid Submodule one	—	Nat.cast_smul_eq_nsmul nsmul_one
le_pow_toAddSubmonoid 📖	mathematical	—	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Preorder.toLE PartialOrder.toPreorder AddSubmonoid.instPartialOrder Monoid.toPow AddSubmonoid.monoid toAddSubmonoid Submodule instPowNat	—	Decidable.eq_or_ne pow_zero pow_zero le_one_toAddSubmonoid Eq.ge pow_toAddSubmonoid
le_self_mul_one_div 📖	mathematical	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder instPartialOrder one	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder instPartialOrder mul IsScalarTower.right instDiv one	—	IsScalarTower.right mul_one mul_le_mul_right instMulLeftMono one_le_one_div
mapHom_apply 📖	mathematical	—	DFunLike.coe RingHom Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule IdemSemiring.toSemiring idemSemiring RingHom.instFunLike mapHom map RingHom.id AlgHom.toLinearMap	—	—
mapHom_id 📖	mathematical	—	mapHom AlgHom.id RingHom.id Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule IdemSemiring.toSemiring idemSemiring	—	RingHom.ext map_id
map_div 📖	mathematical	—	map CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule RingHom.id RingHomSurjective.ids AlgEquiv.toLinearMap Submodule instDiv	—	ext RingHomSurjective.ids map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgEquivClass.toAlgHomClass AlgEquiv.instAlgEquivClass AlgEquiv.injective AlgEquiv.apply_symm_apply
map_mul 📖	mathematical	—	map CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule RingHom.id RingHomSurjective.ids AlgHom.toLinearMap Submodule mul IsScalarTower.right	—	RingHomSurjective.ids IsScalarTower.right smulCommClass_self Algebra.to_smulCommClass mul_eq_map₂ map_iSup Set.ext mem_map ext map_mul NonUnitalAlgSemiHomClass.toMulHomClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass AlgHom.toLinearMap_apply
map_one 📖	mathematical	—	map CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule RingHom.id RingHomSurjective.ids AlgHom.toLinearMap Submodule one	—	ext RingHomSurjective.ids AlgHom.commutes
map_op_mul 📖	mathematical	—	map MulOpposite CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulOpposite.instAddCommMonoid Algebra.toModule MulOpposite.instModule RingHom.id RingHomSurjective.ids LinearEquiv.toLinearMap RingHomInvPair.ids MulOpposite.opLinearEquiv Submodule mul IsScalarTower.right MulOpposite.instSemiring MulOpposite.instAlgebra	—	le_antisymm RingHomSurjective.ids RingHomInvPair.ids IsScalarTower.right mul_le mem_comap RingHomSurjective.invPair map_equiv_eq_comap_symm mul_mem_mul mem_map_equiv
map_op_one 📖	mathematical	—	map MulOpposite CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulOpposite.instAddCommMonoid Algebra.toModule MulOpposite.instModule RingHom.id RingHomSurjective.ids LinearEquiv.toLinearMap RingHomInvPair.ids MulOpposite.opLinearEquiv Submodule one MulOpposite.instSemiring	—	ext RingHomSurjective.ids RingHomInvPair.ids RingHomSurjective.invPair
map_op_pow 📖	mathematical	—	map MulOpposite CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulOpposite.instAddCommMonoid Algebra.toModule MulOpposite.instModule RingHom.id RingHomSurjective.ids LinearEquiv.toLinearMap RingHomInvPair.ids MulOpposite.opLinearEquiv Submodule instPowNat IsScalarTower.right MulOpposite.instSemiring MulOpposite.instAlgebra	—	RingHomSurjective.ids RingHomInvPair.ids IsScalarTower.right RingHomSurjective.invPair map_equiv_eq_comap_symm comap_unop_pow
map_pow 📖	mathematical	—	map CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule RingHom.id RingHomSurjective.ids AlgHom.toLinearMap Submodule instPowNat IsScalarTower.right	—	map_pow MonoidWithZeroHomClass.toMonoidHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass
map_unop_mul 📖	mathematical	—	map MulOpposite CommSemiring.toSemiring MulOpposite.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulOpposite.instModule Algebra.toModule RingHom.id RingHomSurjective.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm MulOpposite.opLinearEquiv Submodule mul MulOpposite.instSemiring IsScalarTower.right MulOpposite.instAlgebra	—	RingHomInvPair.ids LinearEquiv.injective map_injective_of_injective RingHomSurjective.ids IsScalarTower.right RingHomCompTriple.ids map_comp map_op_mul LinearEquiv.comp_coe RingHomInvPair.triples₂ LinearEquiv.symm_trans_self LinearEquiv.refl_toLinearMap map_id
map_unop_one 📖	mathematical	—	map MulOpposite CommSemiring.toSemiring MulOpposite.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulOpposite.instModule Algebra.toModule RingHom.id RingHomSurjective.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm MulOpposite.opLinearEquiv Submodule one MulOpposite.instSemiring	—	RingHomSurjective.ids RingHomInvPair.ids RingHomSurjective.invPair comap_equiv_eq_map_symm comap_op_one
map_unop_pow 📖	mathematical	—	map MulOpposite CommSemiring.toSemiring MulOpposite.instAddCommMonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring MulOpposite.instModule Algebra.toModule RingHom.id RingHomSurjective.ids LinearEquiv.toLinearMap RingHomInvPair.ids LinearEquiv.symm MulOpposite.opLinearEquiv Submodule instPowNat MulOpposite.instSemiring IsScalarTower.right MulOpposite.instAlgebra	—	RingHomSurjective.ids RingHomInvPair.ids IsScalarTower.right RingHomSurjective.invPair comap_equiv_eq_map_symm comap_op_pow
mem_div_iff_forall_mul_mem 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SetLike.instMembership setLike instDiv Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	—
mem_div_iff_smul_subset 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SetLike.instMembership setLike instDiv Set Set.instHasSubset Set.smulSet Algebra.toSMul Algebra.id SetLike.coe	—	Set.smul_mem_smul_set
mem_mul_span_singleton 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SetLike.instMembership setLike mul IsScalarTower.right span Set Set.instSingletonSet Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	IsScalarTower.right Algebra.to_smulCommClass mul_eq_map₂ RingHomSurjective.ids SMulCommClass.symm smulCommClass_self map₂_span_singleton_eq_map_flip
mem_one 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SetLike.instMembership setLike one DFunLike.coe RingHom RingHom.instFunLike algebraMap	—	RingHomSurjective.ids one_eq_range
mem_smul_iff_inv_mul_mem 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring DivisionSemiring.toSemiring Algebra.toModule SetLike.instMembership setLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero pointwiseDistribMulAction Module.toDistribMulAction Semiring.toModule IsScalarTower.to_smulCommClass' IsScalarTower.right Distrib.toMul NonUnitalNonAssocSemiring.toDistrib InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid DivisionSemiring.toGroupWithZero	—	IsScalarTower.to_smulCommClass' IsScalarTower.right inv_mul_cancel_left₀ mul_inv_cancel_left₀
mem_span_mul_finite_of_mem_mul 📖	mathematical	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SetLike.instMembership setLike mul IsScalarTower.right	Finset Set Set.instHasSubset SetLike.coe Finset.instSetLike Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule setLike SetLike.instMembership span Set.mul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	IsScalarTower.right mem_span_mul_finite_of_mem_span_mul span_mul_span span_eq
mem_span_mul_finite_of_mem_span_mul 📖	mathematical	Submodule SetLike.instMembership setLike span Set Set.mul	Finset Set Set.instHasSubset SetLike.coe Finset.instSetLike Submodule SetLike.instMembership setLike span Set.mul	—	mem_span_finite_of_mem_span Finset.subset_mul instIsConcreteLE span_mono
mem_span_singleton_mul 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SetLike.instMembership setLike mul IsScalarTower.right span Set Set.instSingletonSet Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	IsScalarTower.right Algebra.to_smulCommClass mul_eq_map₂ RingHomSurjective.ids smulCommClass_self map₂_span_singleton_eq_map
mker_spanSingleton 📖	mathematical	—	MonoidHom.mker Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass IdemSemiring.toSemiring idemSemiring MonoidWithZeroHom MonoidWithZeroHom.funLike MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass spanSingleton Submonoid.map Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero RingHom RingHom.instFunLike RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass algebraMap IsUnit.submonoid	—	Submonoid.ext MonoidWithZeroHomClass.toMonoidHomClass MonoidWithZeroHom.monoidWithZeroHomClass RingHomClass.toMonoidWithZeroHomClass RingHom.instRingHomClass span_singleton_eq_one_iff
mul_bot 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring mul Bot.bot instBot	—	smul_bot
mul_comm 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule mul IsScalarTower.right	—	le_antisymm IsScalarTower.right mul_le mul_mem_mul_rev
mul_comm_of_commute 📖	mathematical	Commute Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring mul	—	toAddSubmonoid_injective AddSubmonoid.mul_comm_of_commute
mul_def 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule mul IsScalarTower.right span Set Set.mul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SetLike.coe setLike	—	IsScalarTower.right IsScalarTower.left span_coe_eq_restrictScalars restrictScalars_self
mul_eq_map₂ 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule mul IsScalarTower.right map₂ LinearMap.mul Algebra.to_smulCommClass	—	le_antisymm IsScalarTower.right Algebra.to_smulCommClass mul_le apply_mem_map₂ smulCommClass_self map₂_le mul_mem_mul
mul_eq_span_mul_set 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule mul IsScalarTower.right span Set Set.mul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SetLike.coe setLike	—	IsScalarTower.right Algebra.to_smulCommClass mul_eq_map₂ map₂_eq_span_image2
mul_iSup 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring mul iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	—	smul_iSup
mul_induction_on 📖	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership setLike mul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib Distrib.toAdd	—	—	smul_induction_on
mul_induction_on' 📖	—	Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring mul_mem_mul Distrib.toAdd AddMemClass.add_mem Submodule NonUnitalNonAssocSemiring.toAddCommMonoid setLike AddSubmonoidClass.toAddMemClass AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addSubmonoidClass mul SetLike.instMembership	—	—	mul_mem_mul AddMemClass.add_mem AddSubmonoidClass.toAddMemClass addSubmonoidClass smul_induction_on'
mul_le 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrder mul SetLike.instMembership setLike Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	smul_le
mul_mem_mul 📖	mathematical	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership setLike	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership setLike mul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	smul_mem_smul
mul_mem_mul_rev 📖	mathematical	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SetLike.instMembership setLike	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SetLike.instMembership setLike mul IsScalarTower.right Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	IsScalarTower.right mul_mem_mul mul_comm
mul_mem_smul_iff 📖	mathematical	Submonoid MulZeroOneClass.toMulOneClass MonoidWithZero.toMulZeroOneClass Semiring.toMonoidWithZero Ring.toSemiring SetLike.instMembership Submonoid.instSetLike nonZeroDivisors	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing Algebra.toModule Ring.toSemiring SetLike.instMembership setLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero pointwiseDistribMulAction Module.toDistribMulAction Semiring.toModule IsScalarTower.to_smulCommClass' IsScalarTower.right Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	IsScalarTower.to_smulCommClass' IsScalarTower.right mul_cancel_left_mem_nonZeroDivisors
mul_one 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule mul IsScalarTower.right one	—	IsScalarTower.right one_eq_span span_eq span_mul_span IsScalarTower.left Set.mul_singleton Set.image_congr mul_one Set.image_id' span_coe_eq_restrictScalars restrictScalars_self
mul_one_div_le_one 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder instPartialOrder mul IsScalarTower.right instDiv one	—	IsScalarTower.right mul_le mul_comm mem_div_iff_forall_mul_mem
mul_smul_mul_eq_smul_mul_smul 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero pointwiseDistribMulAction Module.toDistribMulAction smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Distrib.toMul NonUnitalNonAssocSemiring.toDistrib mul IsScalarTower.right	—	mul_smul_mul_comm IsScalarTower.right smulCommClass_self instIsScalarTower IsScalarTower.left instSMulCommClass Algebra.to_smulCommClass
mul_subset_mul 📖	mathematical	—	Set Set.instHasSubset Set.mul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SetLike.coe Submodule NonUnitalNonAssocSemiring.toAddCommMonoid setLike mul	—	smul_subset_smul
mul_sup 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring mul SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice	—	smul_sup
mul_toAddSubmonoid 📖	mathematical	—	toAddSubmonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submodule mul AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.mul	—	—
mul_top_eq_top_of_mul_eq_one 📖	mathematical	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring mul one	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring mul Top.top instTop	—	top_unique one_mul mul_assoc smul_mono le_rfl le_top
one_eq_range 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule one LinearMap.range Semiring.toModule RingHom.id RingHomSurjective.ids Algebra.linearMap	—	RingHomSurjective.ids one_eq_span LinearMap.span_singleton_eq_range LinearMap.toSpanSingleton_one_eq_algebraLinearMap
one_eq_span 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring one span Set Set.instSingletonSet AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	RingHomSurjective.ids LinearMap.span_singleton_eq_range
one_eq_span_one_set 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring one span Set Set.one AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	one_eq_span
one_le 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrder one SetLike.instMembership setLike AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	one_eq_span
one_le_one_div 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder instPartialOrder one instDiv	—	IsScalarTower.right le_div_iff_mul_le one_mul
one_mem_div 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SetLike.instMembership setLike instDiv AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	one_le IsScalarTower.right le_div_iff_mul_le one_mul
one_mul 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring mul one	—	one_smul
one_smul 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSMul one	—	le_antisymm smul_le LinearMap.toSpanSingleton_apply smul_one_smul smul_mem one_smul smul_mem_smul one_le le_rfl
pow_add 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instPowNat mul	—	npowRec_add one_mul
pow_eq_npowRec 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instPowNat one mul	—	—
pow_eq_span_pow_set 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instPowNat IsScalarTower.right span Set Set.NPow AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib SetLike.coe setLike	—	IsScalarTower.right span_pow span_eq
pow_induction_on_left 📖	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toMul Submodule NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule SetLike.instMembership setLike instPowNat IsScalarTower.right	—	—	IsScalarTower.right pow_induction_on_left'
pow_induction_on_left' 📖	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap algebraMap_mem Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring AddMemClass.add_mem Submodule NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule setLike AddSubmonoidClass.toAddMemClass AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addSubmonoidClass instPowNat IsScalarTower.right Distrib.toMul MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring idemSemiring Monoid.toPow SetLike.instMembership mul_mem_mul pow_succ'	—	—	IsScalarTower.right algebraMap_mem AddMemClass.add_mem AddSubmonoidClass.toAddMemClass addSubmonoidClass mul_mem_mul pow_succ' mem_one pow_zero mul_induction_on'
pow_induction_on_right 📖	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring Distrib.toMul Submodule NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule SetLike.instMembership setLike instPowNat IsScalarTower.right	—	—	IsScalarTower.right pow_induction_on_right'
pow_induction_on_right' 📖	—	DFunLike.coe RingHom Semiring.toNonAssocSemiring CommSemiring.toSemiring RingHom.instFunLike algebraMap algebraMap_mem Distrib.toAdd NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring AddMemClass.add_mem Submodule NonUnitalNonAssocSemiring.toAddCommMonoid Algebra.toModule setLike AddSubmonoidClass.toAddMemClass AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addSubmonoidClass instPowNat IsScalarTower.right Distrib.toMul mul_mem_mul one mul SetLike.instMembership	—	—	IsScalarTower.right algebraMap_mem AddMemClass.add_mem AddSubmonoidClass.toAddMemClass addSubmonoidClass mul_mem_mul mem_one pow_zero pow_succ mul_induction_on'
pow_mem_pow 📖	mathematical	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership setLike	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership setLike instPowNat Monoid.toPow MonoidWithZero.toMonoid Semiring.toMonoidWithZero	—	pow_subset_pow Set.pow_mem_pow
pow_one 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instPowNat	—	pow_succ pow_zero one_mul
pow_subset_pow 📖	mathematical	—	Set Set.instHasSubset Set.NPow AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring SetLike.coe Submodule NonUnitalNonAssocSemiring.toAddCommMonoid setLike instPowNat	—	trans Set.instIsTransSubset AddSubmonoid.pow_subset_pow le_pow_toAddSubmonoid
pow_succ 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instPowNat mul	—	—
pow_succ' 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instPowNat mul	—	add_comm pow_add pow_one
pow_toAddSubmonoid 📖	mathematical	—	toAddSubmonoid NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submodule instPowNat AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Monoid.toPow AddSubmonoid.monoid	—	pow_succ pow_succ mul_toAddSubmonoid pow_zero pow_zero one_mul one_mul
pow_zero 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instPowNat one	—	—
prod_span 📖	mathematical	—	Finset.prod Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule CommSemiring.toCommMonoid IdemCommSemiring.toCommSemiring instIdemCommSemiring span Set Set.commMonoid	—	Finset.induction_on one_eq_span Finset.prod_insert IsScalarTower.right span_mul_span
prod_span_singleton 📖	mathematical	—	Finset.prod Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule CommSemiring.toCommMonoid IdemCommSemiring.toCommSemiring instIdemCommSemiring span Set Set.instSingletonSet	—	prod_span Set.finset_prod_singleton
restrictScalars_image_smul_eq 📖	mathematical	—	restrictScalars CommSemiring.toSemiring Algebra.toSMul Set Submodule pointwiseSetSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.image DFunLike.coe RingHom Semiring.toNonAssocSemiring RingHom.instFunLike algebraMap	—	le_antisymm set_smul_inductionOn restrictScalars_mem algebraMap_smul mem_set_smul_of_mem_mem IsScalarTower.left mem_set_smul smulCommClass_self smul_mem Finset.sum_congr AddSubmonoidClass.coe_finset_sum addSubmonoidClass sum_mem Finset.mem_coe coe_mem AddMemClass.add_mem AddSubmonoidClass.toAddMemClass ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass set_smul_le Set.mem_image_of_mem
restrictScalars_mul 📖	mathematical	—	restrictScalars NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submodule mul	—	—
restrictScalars_pow 📖	mathematical	—	restrictScalars NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submodule instPowNat	—	restrictScalars.congr_simp pow_one pow_succ
setSemiring_smul_def 📖	mathematical	—	SetSemiring Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring SetSemiring.instIdemSemiringOfMonoid Module.toDistribMulAction pointwiseAddCommMonoid moduleSet mul IsScalarTower.right span DFunLike.coe Equiv Set EquivLike.toFunLike Equiv.instEquivLike SetSemiring.down	—	—
singleton_smul 📖	mathematical	—	SetSemiring Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring SetSemiring.instIdemSemiringOfMonoid Module.toDistribMulAction pointwiseAddCommMonoid moduleSet DFunLike.coe Equiv Set EquivLike.toFunLike Equiv.instEquivLike Set.up Set.instSingletonSet map RingHom.id RingHomSurjective.ids LinearMap.mulLeft Algebra.to_smulCommClass	—	RingHomSurjective.ids Algebra.to_smulCommClass span_eq IsScalarTower.right setSemiring_smul_def SetSemiring.down_up span_mul_span Set.singleton_mul
smul_assoc 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSMul	—	le_antisymm smul_le smul_induction_on smul_mem_smul smul_assoc AddMemClass.add_mem AddSubmonoidClass.toAddMemClass addSubmonoidClass add_smul smul_add
smul_bot 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSMul Bot.bot instBot	—	toAddSubmonoid_injective AddSubmonoid.addSubmonoid_smul_bot
smul_iSup 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSMul iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	—	toAddSubmonoid_injective iSup_toAddSubmonoid AddSubmonoid.smul_iSup
smul_induction_on 📖	—	Submodule SetLike.instMembership setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup	—	—	AddSubmonoid.smul_induction_on
smul_induction_on' 📖	—	Submodule SetLike.instMembership setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smul_mem_smul AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup AddMemClass.add_mem AddSubmonoidClass.toAddMemClass addSubmonoidClass	—	—	smul_mem_smul AddMemClass.add_mem AddSubmonoidClass.toAddMemClass addSubmonoidClass smul_induction_on
smul_le 📖	mathematical	—	Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSMul SetLike.instMembership setLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	AddSubmonoid.smul_le
smul_le_smul 📖	mathematical	Set Set.instHasSubset DFunLike.coe Equiv SetSemiring EquivLike.toFunLike Equiv.instEquivLike SetSemiring.down Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder instPartialOrder	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Preorder.toLE PartialOrder.toPreorder instPartialOrder SetSemiring SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero IdemSemiring.toSemiring SetSemiring.instIdemSemiringOfMonoid Module.toDistribMulAction pointwiseAddCommMonoid moduleSet	—	mul_le_mul' instMulLeftMono instMulRightMono span_mono
smul_mem_smul 📖	mathematical	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring SetLike.instMembership setLike	Submodule SetLike.instMembership setLike NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	AddSubmonoid.smul_mem_smul
smul_mono 📖	mathematical	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrder	Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSMul	—	AddSubmonoid.smul_le_smul
smul_mono_left 📖	mathematical	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Preorder.toLE PartialOrder.toPreorder instPartialOrder	Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSMul	—	smul_mono le_rfl
smul_one_eq_span 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero pointwiseDistribMulAction Module.toDistribMulAction Semiring.toModule IsScalarTower.to_smulCommClass' IsScalarTower.right one span Set Set.instSingletonSet	—	IsScalarTower.to_smulCommClass' IsScalarTower.right one_eq_span smul_span Set.smul_set_singleton smul_eq_mul mul_one
smul_subset_smul 📖	mathematical	—	Set Set.instHasSubset Set.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SetLike.coe Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring setLike instSMul	—	AddSubmonoid.smul_subset_smul
smul_sup 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSMul SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice	—	toAddSubmonoid_injective sup_toAddSubmonoid AddSubmonoid.addSubmonoid_smul_sup
smul_toAddSubmonoid 📖	mathematical	—	toAddSubmonoid Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSMul AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.smul AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	—
spanSingleton_apply 📖	mathematical	—	DFunLike.coe MonoidWithZeroHom Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule NonAssocSemiring.toMulZeroOneClass IdemSemiring.toSemiring idemSemiring MonoidWithZeroHom.funLike spanSingleton span Set Set.instSingletonSet	—	—
span_mul_span 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule mul IsScalarTower.right span Set Set.mul Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	IsScalarTower.right Algebra.to_smulCommClass mul_eq_map₂ map₂_span_span
span_pow 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule instPowNat IsScalarTower.right span Set Set.NPow AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Distrib.toMul NonUnitalNonAssocSemiring.toDistrib	—	IsScalarTower.right pow_zero one_eq_span_one_set pow_succ span_mul_span
span_singleton_algebraMap_of_isUnit 📖	mathematical	IsUnit MonoidWithZero.toMonoid Semiring.toMonoidWithZero CommSemiring.toSemiring	span CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Set Set.instSingletonSet DFunLike.coe RingHom RingHom.instFunLike algebraMap Submodule one	—	one_eq_span span_singleton_smul_eq Algebra.algebraMap_eq_smul_one
span_singleton_eq_one_iff 📖	mathematical	—	span CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule Set Set.instSingletonSet Submodule one Units MonoidWithZero.toMonoid Semiring.toMonoidWithZero DFunLike.coe RingHom RingHom.instFunLike algebraMap Units.val	—	mem_one mem_span_singleton_self mem_span_singleton algebraMap_mem instIsDedekindFiniteMonoid FaithfulSMul.algebraMap_injective map_mul NonUnitalRingHomClass.toMulHomClass RingHomClass.toNonUnitalRingHomClass RingHom.instRingHomClass Algebra.smul_def mul_comm span_singleton_algebraMap_of_isUnit Units.isUnit
span_singleton_mul 📖	mathematical	—	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule mul IsScalarTower.right span Set Set.instSingletonSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne instAddCommMonoidWithOne DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero pointwiseDistribMulAction Module.toDistribMulAction Semiring.toModule IsScalarTower.to_smulCommClass'	—	ext IsScalarTower.right IsScalarTower.to_smulCommClass' mem_span_singleton_mul
sup_mul 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring mul SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice	—	sup_smul
sup_smul 📖	mathematical	—	Submodule NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring instSMul SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice	—	le_antisymm smul_le mem_sup add_smul add_mem_sup smul_mem_smul sup_le smul_mono_left le_sup_left le_sup_right
toSubMulAction_one 📖	mathematical	—	toSubMulAction NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Submodule one SubMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction SubMulAction.instOne DistribMulAction.toMulAction AddMonoidWithOne.toOne AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	SetLike.ext one_eq_span SubMulAction.mem_one mem_span_singleton
top_mul_eq_top_of_mul_eq_one 📖	mathematical	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule mul IsScalarTower.right one	Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule mul IsScalarTower.right Top.top instTop	—	IsScalarTower.right top_unique mul_one mul_assoc smul_mono_left le_top

Submodule.span

Definitions

Name	Category	Theorems
ringHom 📖	CompOp	1 math math: ringHom_apply

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
ringHom_apply 📖	mathematical	—	DFunLike.coe RingHom SetSemiring Submodule CommSemiring.toSemiring NonUnitalNonAssocSemiring.toAddCommMonoid NonAssocSemiring.toNonUnitalNonAssocSemiring Semiring.toNonAssocSemiring Algebra.toModule SetSemiring.instNonAssocSemiringOfMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass IdemSemiring.toSemiring Submodule.idemSemiring RingHom.instFunLike ringHom Submodule.span Equiv Set EquivLike.toFunLike Equiv.instEquivLike SetSemiring.down	—	—

---

← Back to Index