Submodule

📁 Source: Mathlib/RepresentationTheory/Submodule.lean

Statistics

Metric	Count
Definitions invtSubmodule, instBoundedOrderSubtypeSubmoduleMemSublattice, mapSubmodule	3
Theorems asAlgebraHom_mem_of_forall_mem, bot_mem, coe_bot, coe_top, instNontrivialSubtypeSubmoduleMemSublattice, nontrivial_iff, top_mem, mem_invtSubmodule	8
Total	11

Representation

Definitions

Name	Category	Theorems
invtSubmodule 📖	CompOp	7 math math: invtSubmodule.nontrivial_iff, invtSubmodule.coe_top, invtSubmodule.top_mem, invtSubmodule.coe_bot, invtSubmodule.instNontrivialSubtypeSubmoduleMemSublattice, mem_invtSubmodule, invtSubmodule.bot_mem
mapSubmodule 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
asAlgebraHom_mem_of_forall_mem 📖	mathematical	Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike DFunLike.coe LinearMap RingHom.id Semiring.toNonAssocSemiring LinearMap.instFunLike Representation MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	Submodule CommSemiring.toSemiring SetLike.instMembership Submodule.setLike DFunLike.coe Module.End LinearMap.instFunLike RingHom.id Semiring.toNonAssocSemiring AlgHom MonoidAlgebra MonoidAlgebra.semiring Module.End.instSemiring MonoidAlgebra.algebra Algebra.id Module.End.instAlgebra smulCommClass_self CommSemiring.toCommMonoid DistribMulAction.toMulAction CommMonoid.toMonoid AddCommMonoid.toAddMonoid Module.toDistribMulAction Algebra.toSMul IsScalarTower.left MonoidWithZero.toMonoid Semiring.toMonoidWithZero AlgHom.funLike asAlgebraHom	—	MonoidAlgebra.induction_on smulCommClass_self IsScalarTower.left asAlgebraHom_single one_smul map_add SemilinearMapClass.toAddHomClass NonUnitalAlgHomClass.instLinearMapClass AlgHom.instNonUnitalAlgHomClassOfAlgHomClass AlgHom.algHomClass AddMemClass.add_mem AddSubmonoidClass.toAddMemClass Submodule.addSubmonoidClass map_smul SemilinearMapClass.toMulActionSemiHomClass SMulMemClass.smul_mem Submodule.smulMemClass
mem_invtSubmodule 📖	mathematical	—	Submodule CommSemiring.toSemiring Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike invtSubmodule Module.End.invtSubmodule DFunLike.coe Representation LinearMap RingHom.id Semiring.toNonAssocSemiring MonoidHom.instFunLike MulOneClass.toMulOne Monoid.toMulOneClass MulZeroOneClass.toMulOneClass NonAssocSemiring.toMulZeroOneClass Module.End.instSemiring	—	invtSubmodule.eq_1 Sublattice.mem_iInf

Representation.invtSubmodule

Definitions

Name	Category	Theorems
instBoundedOrderSubtypeSubmoduleMemSublattice 📖	CompOp	2 math math: coe_top, coe_bot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
bot_mem 📖	mathematical	—	Submodule CommSemiring.toSemiring Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Representation.invtSubmodule Bot.bot Submodule.instBot	—	—
coe_bot 📖	mathematical	—	Submodule CommSemiring.toSemiring Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Representation.invtSubmodule Bot.bot OrderBot.toBot Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder BoundedOrder.toOrderBot instBoundedOrderSubtypeSubmoduleMemSublattice Submodule.instBot	—	—
coe_top 📖	mathematical	—	Submodule CommSemiring.toSemiring Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Representation.invtSubmodule Top.top OrderTop.toTop Preorder.toLE PartialOrder.toPreorder Submodule.instPartialOrder BoundedOrder.toOrderTop instBoundedOrderSubtypeSubmoduleMemSublattice Submodule.instTop	—	—
instNontrivialSubtypeSubmoduleMemSublattice 📖	mathematical	—	Nontrivial Submodule CommSemiring.toSemiring Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Representation.invtSubmodule	—	nontrivial_iff
nontrivial_iff 📖	mathematical	—	Nontrivial Submodule CommSemiring.toSemiring Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Representation.invtSubmodule	—	Mathlib.Tactic.Contrapose.contrapose₁ instSubsingletonSubtype_mathlib Unique.instSubsingleton Subtype.coe_ne_coe coe_top coe_bot bot_ne_top Submodule.instNontrivial
top_mem 📖	mathematical	—	Submodule CommSemiring.toSemiring Sublattice ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Submodule.completeLattice SetLike.instMembership Sublattice.instSetLike Representation.invtSubmodule Top.top Submodule.instTop	—	—

---

← Back to Index