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	Module.End AlgHom MonoidAlgebra MonoidAlgebra.semiring 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