Pointwise

📁 Source: Mathlib/Algebra/Module/Submodule/Pointwise.lean

Statistics

Metric	Count
Definitions involutivePointwiseNeg, negOrderIso, pointwiseAdd, pointwiseAddCommMonoid, pointwiseDistribMulAction, pointwiseMulActionWithZero, pointwiseNeg, pointwiseSetDistribMulAction, pointwiseSetMulAction, pointwiseSetSMul, pointwiseZero	11
Theorems add_eq_sup, coe_pointwise_smul, coe_set_neg, empty_set_smul, instCanonicallyOrderedAdd, instCovariantClassHSMulLe, instCovariantClassSetHSMulLe, instIsOrderedAddMonoid, mem_neg, mem_set_smul, mem_set_smul_def, mem_set_smul_of_mem_mem, mem_singleton_set_smul, mem_smul_pointwise_iff_exists, neg_bot, neg_eq_self, neg_iInf, neg_iSup, neg_inf, neg_le, neg_le_neg, neg_sup, neg_toAddSubmonoid, neg_top, pointwiseCentralScalar, pointwise_smul_toAddSubgroup, pointwise_smul_toAddSubmonoid, set_smul_bot, set_smul_eq_iSup, set_smul_eq_map, set_smul_eq_of_le, set_smul_inductionOn, set_smul_le, set_smul_le_iff, set_smul_le_of_le_le, set_smul_mono_left, set_smul_span, singleton_set_smul, smul_bot', smul_def, smul_iSup', smul_inductionOn_pointwise, smul_le_self_of_tower, smul_mem_pointwise_smul, smul_span, smul_sup', span_neg_eq_neg, span_set_smul, span_smul, sup_set_smul, zero_eq_bot	51
Total	62

Submodule

Definitions

Name	Category	Theorems
involutivePointwiseNeg 📖	CompOp	—
negOrderIso 📖	CompOp	—
pointwiseAdd 📖	CompOp	16 math math: HomogeneousIdeal.toIdeal_add, LinearDisjoint.op, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_apply, AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_symm_apply, equivOpposite_apply, FractionalIdeal.coe_add, Ideal.add_eq_one_iff, Ideal.isCoprime_tfae, instCanonicallyOrderedAdd, linearDisjoint_op, Ideal.add_eq_sup, Ideal.isCoprime_iff_add, equivOpposite_symm_apply, mulMap_op, add_eq_sup, IsCoprime.add_eq
pointwiseAddCommMonoid 📖	CompOp	65 math math: smul_def, RingTheory.Sequence.isWeaklyRegular_cons_iff', RingTheory.Sequence.isWeaklyRegular_cons_iff, Ideal.sum_eq_sup, QuotSMulTop.equivTensorQuot_naturality, ideal_span_singleton_smul, top_eq_ofList_cons_smul_iff, ZSpan.smul, RingTheory.Sequence.isRegular_cons_iff, QuotSMulTop.equivTensorQuot_naturality_mk, smul_iSup', QuotSMulTop.map_comp_mkQ, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson, pointwise_smul_toAddSubgroup, ModuleCat.smulShortComplex_X₃_isAddCommGroup, smul_bot', smul_mem_pointwise_smul, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim, element_smul_restrictScalars, smul_sup', QuotSMulTop.map_surjective, smul_le_self_of_tower, Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_maximalIdeal, pointwise_smul_toAddSubmonoid, ModuleCat.smulShortComplex_g, coe_pointwise_smul, IsLattice.smul, smul_le_smul, smul_top_inf_eq_smul_of_isSMulRegular_on_quot, mem_colon_iff_le, QuotSMulTop.equivQuotTensor_naturality, LinearMap.exact_smul_id_smul_top_mkQ, instCovariantClassHSMulLe, quotOfListConsSMulTopEquivQuotSMulTopInner_naturality, singleton_smul, QuotSMulTop.map_exact, Module.supportDim_quotSMulTop_succ_eq_supportDim, mem_smul_pointwise_iff_exists, singleton_set_smul, Module.supportDim_le_supportDim_quotSMulTop_succ, QuotSMulTop.equivQuotTensor_naturality_mk, Module.supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson, SubmodulesRingBasis.leftMul, Module.support_quotSMulTop, span_smul, map_pointwise_smul, set_smul_eq_iSup, QuotSMulTop.map_first_exact_on_four_term_exact_of_isSMulRegular_last, Ideal.ofList_cons_smul, Module.supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson, QuotSMulTop.map_comp, IsSMulRegular.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, smul_span, QuotSMulTop.map_apply_mk, setSemiring_smul_def, ModuleCat.smulShortComplex_X₃_isModule, instIsOrderedAddMonoid, Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson, QuotSMulTop.map_id, Module.supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes, RingTheory.Sequence.isRegular_cons_iff', isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul, Module.isTorsionBy_quotient_element_smul, pointwiseCentralScalar, exists_sub_one_mem_and_smul_le_of_fg_of_le_sup
pointwiseDistribMulAction 📖	CompOp	82 math math: smul_def, RingTheory.Sequence.isWeaklyRegular_cons_iff', RingTheory.Sequence.isWeaklyRegular_cons_iff, QuotSMulTop.equivTensorQuot_naturality, ideal_span_singleton_smul, top_eq_ofList_cons_smul_iff, BoxIntegral.unitPartition.mem_smul_span_iff, ZSpan.smul, RingTheory.Sequence.isRegular_cons_iff, QuotSMulTop.equivTensorQuot_naturality_mk, smul_iSup', QuotSMulTop.map_comp_mkQ, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim_of_mem_jacobson, pointwise_smul_toAddSubgroup, ModuleCat.smulShortComplex_X₃_isAddCommGroup, smul_bot', smul_mem_pointwise_smul, instSMulCommClass, ringKrullDim_quotSMulTop_succ_eq_ringKrullDim, element_smul_restrictScalars, smul_sup', QuotSMulTop.map_surjective, mul_mem_smul_iff, smul_le_self_of_tower, mem_smul_iff_inv_mul_mem, Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_maximalIdeal, spinGroup.conjAct_smul_range_ι, Ideal.Quotient.smul_top, pointwise_smul_toAddSubmonoid, traceForm_dualSubmodule_adjoin, ModuleCat.smulShortComplex_g, coe_pointwise_smul, IsLattice.smul, smul_top_inf_eq_smul_of_isSMulRegular_on_quot, Ideal.exact_mulQuot_quotOfMul, mem_colon_iff_le, QuotSMulTop.equivQuotTensor_naturality, LinearMap.exact_smul_id_smul_top_mkQ, instCovariantClassHSMulLe, quotOfListConsSMulTopEquivQuotSMulTopInner_naturality, mul_smul_mul_eq_smul_mul_smul, pinGroup.conjAct_smul_range_ι, QuotSMulTop.map_exact, Module.supportDim_quotSMulTop_succ_eq_supportDim, mem_smul_pointwise_iff_exists, Ideal.quotOfMul_surjective, singleton_set_smul, FractionalIdeal.den_mul_self_eq_num, Module.supportDim_le_supportDim_quotSMulTop_succ, QuotSMulTop.equivQuotTensor_naturality_mk, Module.supportDim_quotSMulTop_succ_eq_supportDim_mem_jacobson, SubmodulesRingBasis.leftMul, Module.support_quotSMulTop, smul_one_eq_span, span_smul, map_pointwise_smul, set_smul_eq_iSup, QuotSMulTop.map_first_exact_on_four_term_exact_of_isSMulRegular_last, Ideal.ofList_cons_smul, Module.supportDim_le_supportDim_quotSMulTop_succ_of_mem_jacobson, QuotSMulTop.map_comp, span_singleton_mul, IsSMulRegular.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul, smul_span, QuotSMulTop.map_apply_mk, instSMulCommClass_1, ModuleCat.smulShortComplex_X₃_isModule, Module.supportDim_quotSMulTop_succ_eq_of_notMem_minimalPrimes_of_mem_jacobson, Subalgebra.pointwise_smul_toSubmodule, QuotSMulTop.map_id, Ideal.map_pointwise_smul, ringKrullDim_le_ringKrullDim_quotSMulTop_succ, Module.supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes, RingTheory.Sequence.isRegular_cons_iff', lipschitzGroup.conjAct_smul_range_ι, isPrimary_iff_zero_divisor_quotient_imp_nilpotent_smul, Module.isTorsionBy_quotient_element_smul, BoxIntegral.unitPartition.tag_mem_smul_span, pointwiseCentralScalar, instIsScalarTower, exists_sub_one_mem_and_smul_le_of_fg_of_le_sup, Ideal.mulQuot_injective
pointwiseMulActionWithZero 📖	CompOp	—
pointwiseNeg 📖	CompOp	13 math math: neg_top, neg_sup, neg_iSup, neg_bot, neg_iInf, neg_eq_self, neg_inf, neg_toAddSubmonoid, coe_set_neg, span_neg_eq_neg, mem_neg, neg_le_neg, neg_le
pointwiseSetDistribMulAction 📖	CompOp	—
pointwiseSetMulAction 📖	CompOp	—
pointwiseSetSMul 📖	CompOp	23 math math: set_smul_le_iff, set_smul_span, Module.isTorsionBySet_quotient_set_smul, set_smul_mono_left, coe_span_smul, mem_set_smul_def, mem_singleton_set_smul, set_smul_eq_map, mem_set_smul_of_mem_mem, span_set_smul, empty_set_smul, singleton_set_smul, set_smul_le_of_le_le, set_smul_eq_iSup, set_smul_bot, span_smul_eq, coe_set_smul, mem_set_smul, sup_set_smul, set_smul_top_eq_span, smul_le_span, set_smul_le, instCovariantClassSetHSMulLe
pointwiseZero 📖	CompOp	21 math math: Valuation.supp_quot_supp, nilradical_eq_zero, instPosMulStrictMonoIdeal, IsSemiprimaryRing.isNilpotent, FractionalIdeal.num_zero_eq, Ideal.zero_eq_bot, Ideal.isCancelMulZero, IsNoetherianRing.isNilpotent_nilradical, IsArtinianRing.isNilpotent_jacobson_bot, Ideal.FG.isNilpotent_iff_le_nilradical, isArtinianRing_iff_isNilpotent_maximalIdeal, FractionalIdeal.instPosMulReflectLEIdealOfIsDedekindDomain, zero_eq_bot, instMulPosStrictMonoIdeal, Ideal.instNoZeroDivisors, Ideal.associatesEquivIsPrincipal_map_zero, isSemiprimaryRing_iff, IsArtinianRing.isNilpotent_nilradical, FractionalIdeal.num_eq_zero_iff, AddValuation.supp_quot_supp, PointedCone.dual_univ

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_eq_sup 📖	mathematical	—	Submodule pointwiseAdd SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice	—	—
coe_pointwise_smul 📖	mathematical	—	SetLike.coe Submodule setLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction Set Set.smulSet	—	—
coe_set_neg 📖	mathematical	—	SetLike.coe Submodule AddCommGroup.toAddCommMonoid setLike pointwiseNeg Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
empty_set_smul 📖	mathematical	—	Set Submodule pointwiseSetSMul Set.instEmptyCollection Bot.bot instBot	—	ext mem_sInf mem_set_smul_def zero_mem
instCanonicallyOrderedAdd 📖	mathematical	—	CanonicallyOrderedAdd Submodule pointwiseAdd Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	sup_eq_right le_sup_right le_sup_left
instCovariantClassHSMulLe 📖	mathematical	—	CovariantClass Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	map_mono RingHomSurjective.ids
instCovariantClassSetHSMulLe 📖	mathematical	—	CovariantClass Set Submodule pointwiseSetSMul Preorder.toLE PartialOrder.toPreorder instPartialOrder	—	set_smul_le mem_set_smul_of_mem_mem
instIsOrderedAddMonoid 📖	mathematical	—	IsOrderedAddMonoid Submodule pointwiseAddCommMonoid instPartialOrder	—	sup_le_sup_right
mem_neg 📖	mathematical	—	Submodule AddCommGroup.toAddCommMonoid SetLike.instMembership setLike pointwiseNeg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid	—	—
mem_set_smul 📖	mathematical	—	Submodule SetLike.instMembership setLike Set pointwiseSetSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction Set.instHasSubset SetLike.coe Finset Finset.instSetLike Finsupp.support zero Finsupp.sum addCommMonoid smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddMonoidWithOne.toAddMonoid AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne Semiring.toNonAssocSemiring DistribSMul.toSMulZeroClass instDistribSMul NonAssocSemiring.toNonUnitalNonAssocSemiring AddCommMonoid.toAddMonoid DistribMulAction.toDistribSMul IsScalarTower.left DistribMulAction.toMulAction	—	IsScalarTower.left RingHomCompTriple.ids RingHomInvPair.ids RingHomSurjective.ids set_smul_eq_map mem_set_smul_def mem_sInf Finsupp.sum.eq_1 AddSubmonoid.coe_finset_sum sum_mem
mem_set_smul_def 📖	mathematical	—	Submodule SetLike.instMembership setLike Set pointwiseSetSMul InfSet.sInf instInfSet setOf	—	—
mem_set_smul_of_mem_mem 📖	mathematical	Set Set.instMembership Submodule SetLike.instMembership setLike	pointwiseSetSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	mem_set_smul_def mem_sInf
mem_singleton_set_smul 📖	mathematical	—	Submodule SetLike.instMembership setLike Set pointwiseSetSMul Set.instSingletonSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	set_smul_inductionOn SMulMemClass.smul_mem smulMemClass SMulCommClass.smul_comm add_mem smul_add zero_mem smul_zero mem_set_smul_of_mem_mem
mem_smul_pointwise_iff_exists 📖	mathematical	—	Submodule SetLike.instMembership setLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction	—	Set.mem_smul_set
neg_bot 📖	mathematical	—	Submodule AddCommGroup.toAddCommMonoid pointwiseNeg Bot.bot instBot	—	SetLike.coe_injective Set.neg_singleton neg_zero
neg_eq_self 📖	mathematical	—	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid pointwiseNeg	—	ext neg_mem_iff
neg_iInf 📖	mathematical	—	Submodule AddCommGroup.toAddCommMonoid pointwiseNeg iInf instInfSet	—	OrderIso.map_iInf
neg_iSup 📖	mathematical	—	Submodule AddCommGroup.toAddCommMonoid pointwiseNeg iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	—	OrderIso.map_iSup
neg_inf 📖	mathematical	—	Submodule AddCommGroup.toAddCommMonoid pointwiseNeg instMin	—	—
neg_le 📖	mathematical	—	Submodule AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder pointwiseNeg	—	SetLike.coe_subset_coe instIsConcreteLE Set.neg_subset
neg_le_neg 📖	mathematical	—	Submodule AddCommGroup.toAddCommMonoid Preorder.toLE PartialOrder.toPreorder instPartialOrder pointwiseNeg	—	SetLike.coe_subset_coe instIsConcreteLE Set.neg_subset_neg
neg_sup 📖	mathematical	—	Submodule AddCommGroup.toAddCommMonoid pointwiseNeg SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice	—	OrderIso.map_sup
neg_toAddSubmonoid 📖	mathematical	—	toAddSubmonoid AddCommGroup.toAddCommMonoid Submodule pointwiseNeg AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid AddSubmonoid.neg AddCommGroup.toAddGroup	—	—
neg_top 📖	mathematical	—	Submodule AddCommGroup.toAddCommMonoid pointwiseNeg Top.top instTop	—	SetLike.coe_injective Set.neg_univ
pointwiseCentralScalar 📖	mathematical	—	IsCentralScalar Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction MulOpposite MulOpposite.instMonoid	—	RingHomSurjective.ids LinearMap.ext IsCentralScalar.op_smul_eq_smul
pointwise_smul_toAddSubgroup 📖	mathematical	—	toAddSubgroup Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction AddSubgroup AddCommGroup.toAddGroup SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction AddSubgroup.pointwiseMulAction	—	—
pointwise_smul_toAddSubmonoid 📖	mathematical	—	toAddSubmonoid Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction AddSubmonoid SemigroupAction.toSMul Monoid.toSemigroup MulAction.toSemigroupAction AddSubmonoid.pointwiseMulAction	—	—
set_smul_bot 📖	mathematical	—	Set Submodule pointwiseSetSMul Bot.bot instBot	—	eq_bot_iff set_smul_inductionOn smul_zero AddSubmonoidClass.toZeroMemClass addSubmonoidClass add_zero
set_smul_eq_iSup 📖	mathematical	—	Set Submodule pointwiseSetSMul iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice Set.instMembership SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction	—	Set.ext map_le_iff_le_comap RingHomSurjective.ids csInf_Ici
set_smul_eq_map 📖	mathematical	—	Set Submodule pointwiseSetSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction map Finsupp SetLike.instMembership setLike AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid addCommMonoid Finsupp.instAddCommMonoid Finsupp.module module RingHom.id Semiring.toNonAssocSemiring RingHomSurjective.ids LinearMap.comp RingHomCompTriple.ids subtype DFunLike.coe LinearEquiv RingHomInvPair.ids LinearMap Pi.addCommMonoid LinearMap.addCommMonoid Pi.Function.module LinearMap.module EquivLike.toFunLike LinearEquiv.instEquivLike Finsupp.lsum DistribSMul.toLinearMap DistribMulAction.toDistribSMul Finsupp.supported	—	IsScalarTower.left set_smul_eq_of_le RingHomSurjective.ids RingHomCompTriple.ids RingHomInvPair.ids Finsupp.single_mem_supported SMulMemClass.smul_mem smulMemClass Finsupp.sum_single_index smul_zero Finset.sum_congr AddSubmonoid.coe_finset_sum sum_mem mem_set_smul_def mem_sInf Set.ext
set_smul_eq_of_le 📖	—	Submodule SetLike.instMembership setLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Preorder.toLE PartialOrder.toPreorder instPartialOrder Set pointwiseSetSMul	—	—	le_antisymm set_smul_le
set_smul_inductionOn 📖	—	Submodule SetLike.instMembership setLike Set pointwiseSetSMul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul mem_set_smul_of_mem_mem MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smul_mem AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup add_mem zero_mem	—	—	mem_set_smul_of_mem_mem smul_mem add_mem zero_mem set_smul_le
set_smul_le 📖	mathematical	Submodule SetLike.instMembership setLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	Preorder.toLE PartialOrder.toPreorder instPartialOrder Set pointwiseSetSMul	—	sInf_le
set_smul_le_iff 📖	mathematical	—	Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder Set pointwiseSetSMul SetLike.instMembership setLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	mem_set_smul_of_mem_mem set_smul_le
set_smul_le_of_le_le 📖	mathematical	Set Set.instLE Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder	pointwiseSetSMul	—	le_trans set_smul_mono_left smul_mono_right instCovariantClassSetHSMulLe
set_smul_mono_left 📖	mathematical	Set Set.instLE	Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder pointwiseSetSMul	—	set_smul_le mem_set_smul_of_mem_mem
set_smul_span 📖	mathematical	—	Set Submodule pointwiseSetSMul span Set.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul	—	set_smul_eq_iSup iSup_congr_Prop smul_span iSup_span Set.iUnion_smul_set
singleton_set_smul 📖	mathematical	—	Set Submodule pointwiseSetSMul Set.instSingletonSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction	—	set_smul_eq_of_le mem_set_smul_def mem_sInf
smul_bot' 📖	mathematical	—	Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction Bot.bot instBot	—	map_bot RingHomSurjective.ids
smul_def 📖	mathematical	—	Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction span Set Set.smulSet SetLike.coe setLike	—	IsScalarTower.left span_coe_eq_restrictScalars restrictScalars_self
smul_iSup' 📖	mathematical	—	Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction iSup ConditionallyCompletePartialOrderSup.toSupSet ConditionallyCompletePartialOrder.toConditionallyCompletePartialOrderSup ConditionallyCompleteLattice.toConditionallyCompletePartialOrder CompleteLattice.toConditionallyCompleteLattice completeLattice	—	map_iSup RingHomSurjective.ids
smul_inductionOn_pointwise 📖	—	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul smul_mem_pointwise_smul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction smul_mem Submodule pointwiseAddCommMonoid pointwiseDistribMulAction AddCommMagma.toAdd AddCommSemigroup.toAddCommMagma AddCommMonoid.toAddCommSemigroup add_mem zero_mem SetLike.instMembership setLike	—	—	smul_mem_pointwise_smul smul_mem add_mem zero_mem singleton_set_smul set_smul_inductionOn mem_set_smul_of_mem_mem
smul_le_self_of_tower 📖	mathematical	—	Submodule Preorder.toLE PartialOrder.toPreorder instPartialOrder SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction	—	smul_of_tower_mem
smul_mem_pointwise_smul 📖	mathematical	Submodule SetLike.instMembership setLike	SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction	—	Set.smul_mem_smul_set
smul_span 📖	mathematical	—	Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction span Set Set.smulSet	—	map_span RingHomSurjective.ids
smul_sup' 📖	mathematical	—	Submodule SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid pointwiseAddCommMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul pointwiseDistribMulAction SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice completeLattice	—	map_sup RingHomSurjective.ids
span_neg_eq_neg 📖	mathematical	—	span AddCommGroup.toAddCommMonoid Set Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid Submodule pointwiseNeg	—	le_antisymm span_le coe_set_neg Set.neg_subset neg_neg subset_span neg_le
span_set_smul 📖	mathematical	—	span Set Set.smul SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Submodule pointwiseSetSMul	—	set_smul_span
span_smul 📖	mathematical	—	span Set Set.smulSet SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul Submodule pointwiseAddCommMonoid pointwiseDistribMulAction	—	RingHomSurjective.ids span_image
sup_set_smul 📖	mathematical	—	Set Submodule pointwiseSetSMul SemilatticeSup.toMax Lattice.toSemilatticeSup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice CompleteBooleanAlgebra.toCompleteLattice CompleteAtomicBooleanAlgebra.toCompleteBooleanAlgebra Set.instCompleteAtomicBooleanAlgebra completeLattice	—	set_smul_eq_of_le mem_sup_left mem_set_smul_of_mem_mem mem_sup_right sup_le set_smul_mono_left le_sup_left le_sup_right
zero_eq_bot 📖	mathematical	—	Submodule pointwiseZero Bot.bot instBot	—	—

---

← Back to Index