Basic

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

Statistics

Metric	Count
Definitions instVAddSubtypeMem	1
Theorems instFaithfulVAddSubtypeMem, instIsTorsionFree, isCentralScalar, ne_zero_of_ortho, neg_coe, notMem_of_ortho, smul_mem_iff, sum_mem, sum_smul_mem, toAddSubgroup_le, toAddSubgroup_mono, toAddSubgroup_strictMono, toAddSubgroup_toAddSubmonoid, toAddSubmonoid_le, toAddSubmonoid_mono, toAddSubmonoid_strictMono, toSubMulAction_mono, toSubMulAction_strictMono, vaddCommClass, vadd_def	20
Total	21

Submodule

Definitions

Name	Category	Theorems
instVAddSubtypeMem 📖	CompOp	9 math math: NumberField.mixedEmbedding.fundamentalDomain_integerLattice, vadd_def, NumberField.mixedEmbedding.fundamentalDomain_idealLattice, ZSpan.exist_unique_vadd_mem_fundamentalDomain, ZSpan.isAddFundamentalDomain, ZLattice.isAddFundamentalDomain, vaddCommClass, ZSpan.vadd_mem_fundamentalDomain, instFaithfulVAddSubtypeMem

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
instFaithfulVAddSubtypeMem 📖	mathematical	—	FaithfulVAdd Submodule SetLike.instMembership setLike instVAddSubtypeMem	—	FaithfulVAdd.eq_of_vadd_eq_vadd
instIsTorsionFree 📖	mathematical	—	Module.IsTorsionFree Submodule SetLike.instMembership setLike addCommMonoid module	—	Function.Injective.moduleIsTorsionFree Subtype.coe_injective
isCentralScalar 📖	mathematical	—	IsCentralScalar Submodule SetLike.instMembership setLike smul MulOpposite	—	SubMulAction.isCentralScalar
ne_zero_of_ortho 📖	—	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	—	—	zero_mem notMem_of_ortho
neg_coe 📖	mathematical	—	Set InvolutiveNeg.toNeg Set.involutiveNeg SubtractionMonoid.toInvolutiveNeg SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid SetLike.coe Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid setLike	—	Set.ext neg_mem_iff
notMem_of_ortho 📖	mathematical	MulZeroClass.toZero NonUnitalNonAssocSemiring.toMulZeroClass NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing Ring.toNonAssocRing	Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid SetLike.instMembership setLike	—	neg_smul one_smul neg_add_cancel NeZero.one IsDomain.toNontrivial
smul_mem_iff 📖	mathematical	—	Submodule SetLike.instMembership setLike SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero DivisionSemiring.toSemiring Module.toDistribMulAction	—	SubMulAction.smul_mem_iff
sum_mem 📖	mathematical	Submodule SetLike.instMembership setLike	Finset.sum	—	sum_mem addSubmonoidClass
sum_smul_mem 📖	mathematical	Submodule SetLike.instMembership setLike	Finset.sum SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction	—	sum_mem addSubmonoidClass smul_mem
toAddSubgroup_le 📖	mathematical	—	AddSubgroup AddCommGroup.toAddGroup Preorder.toLE PartialOrder.toPreorder AddSubgroup.instPartialOrder toAddSubgroup Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid instPartialOrder	—	—
toAddSubgroup_mono 📖	mathematical	—	Monotone Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid AddSubgroup AddCommGroup.toAddGroup PartialOrder.toPreorder instPartialOrder AddSubgroup.instPartialOrder toAddSubgroup	—	StrictMono.monotone toAddSubgroup_strictMono
toAddSubgroup_strictMono 📖	mathematical	—	StrictMono Submodule Ring.toSemiring AddCommGroup.toAddCommMonoid AddSubgroup AddCommGroup.toAddGroup PartialOrder.toPreorder instPartialOrder AddSubgroup.instPartialOrder toAddSubgroup	—	—
toAddSubgroup_toAddSubmonoid 📖	mathematical	—	AddSubgroup.toAddSubmonoid AddCommGroup.toAddGroup toAddSubgroup toAddSubmonoid Ring.toSemiring AddCommGroup.toAddCommMonoid	—	—
toAddSubmonoid_le 📖	mathematical	—	AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid Preorder.toLE PartialOrder.toPreorder AddSubmonoid.instPartialOrder toAddSubmonoid Submodule instPartialOrder	—	—
toAddSubmonoid_mono 📖	mathematical	—	Monotone Submodule AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid PartialOrder.toPreorder instPartialOrder AddSubmonoid.instPartialOrder toAddSubmonoid	—	StrictMono.monotone toAddSubmonoid_strictMono
toAddSubmonoid_strictMono 📖	mathematical	—	StrictMono Submodule AddSubmonoid AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid PartialOrder.toPreorder instPartialOrder AddSubmonoid.instPartialOrder toAddSubmonoid	—	—
toSubMulAction_mono 📖	mathematical	—	Monotone Submodule SubMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction PartialOrder.toPreorder instPartialOrder SubMulAction.instPartialOrder toSubMulAction	—	StrictMono.monotone toSubMulAction_strictMono
toSubMulAction_strictMono 📖	mathematical	—	StrictMono Submodule SubMulAction SMulZeroClass.toSMul AddZero.toZero AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid DistribSMul.toSMulZeroClass DistribMulAction.toDistribSMul MonoidWithZero.toMonoid Semiring.toMonoidWithZero Module.toDistribMulAction PartialOrder.toPreorder instPartialOrder SubMulAction.instPartialOrder toSubMulAction	—	—
vaddCommClass 📖	mathematical	—	VAddCommClass Submodule SetLike.instMembership setLike instVAddSubtypeMem	—	VAddCommClass.vadd_comm
vadd_def 📖	mathematical	—	HVAdd.hVAdd Submodule SetLike.instMembership setLike instHVAdd instVAddSubtypeMem	—	—

---

← Back to Index