Support

📁 Source: Mathlib/Algebra/Group/Submonoid/Support.lean

Statistics

Metric	Count
Definitions IsPointed, IsSpanning, support, IsMulPointed, IsMulSpanning, mulSupport	6
Theorems gc_toAddSubmonoid_support, eq_zero_of_mem_of_neg_mem, eq_zero_of_mem_of_neg_mem₂, mk, of_support_eq_bot, support_eq_bot, maximal_isPointed, mem_or_neg_mem, mk, of_le, coe_support, mem_support, support_toAddSubmonoid, gc_toSubmonoid_mulSupport, eq_one_of_mem_of_inv_mem, eq_one_of_mem_of_inv_mem₂, mk, mulSupport_eq_bot, of_mulSupport_eq_bot, maximal_isMulPointed, mem_or_inv_mem, mk, of_le, coe_mulSupport, mem_mulSupport, mulSupport_toSubmonoid, isMulPointed_iff_mulSupport_eq_bot, isPointed_iff_support_eq_bot	28
Total	34

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gc_toAddSubmonoid_support 📖	mathematical	—	GaloisConnection AddSubgroup AddSubmonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid PartialOrder.toPreorder instPartialOrder AddSubmonoid.instPartialOrder toAddSubmonoid AddSubmonoid.support	—	AddSubmonoid.mem_support mem_toAddSubmonoid neg_mem_iff AddSubgroupClass.toNegMemClass instAddSubgroupClass

AddSubmonoid

Definitions

Name	Category	Theorems
IsPointed 📖	MathDef	4 math math: IsPointed.of_support_eq_bot, isPointed_iff_support_eq_bot, IsPointed.mk, IsSpanning.maximal_isPointed
IsSpanning 📖	MathDef	2 math math: IsSpanning.mk, IsSpanning.of_le
support 📖	CompOp	7 math math: coe_support, mem_support, AddSubgroup.gc_toAddSubmonoid_support, isPointed_iff_support_eq_bot, support_toAddSubmonoid, PointedCone.support_eq, IsPointed.support_eq_bot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_support 📖	mathematical	—	SetLike.coe AddSubgroup AddSubgroup.instSetLike support Set Set.instInter AddSubmonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instSetLike Set.neg NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	—
mem_support 📖	mathematical	—	AddSubgroup SetLike.instMembership AddSubgroup.instSetLike support AddSubmonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instSetLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	—
support_toAddSubmonoid 📖	mathematical	—	AddSubgroup.toAddSubmonoid support AddSubmonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid instMin neg	—	—

AddSubmonoid.IsPointed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_zero_of_mem_of_neg_mem 📖	mathematical	AddSubmonoid.IsPointed AddSubmonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SetLike.instMembership AddSubmonoid.instSetLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	—
eq_zero_of_mem_of_neg_mem₂ 📖	mathematical	AddSubmonoid.IsPointed AddSubmonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SetLike.instMembership AddSubmonoid.instSetLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	eq_zero_of_mem_of_neg_mem
mk 📖	mathematical	NegZeroClass.toZero SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	AddSubmonoid.IsPointed	—	—
of_support_eq_bot 📖	mathematical	AddSubmonoid.support Bot.bot AddSubgroup AddSubgroup.instBot	AddSubmonoid.IsPointed	—	isPointed_iff_support_eq_bot
support_eq_bot 📖	mathematical	AddSubmonoid.IsPointed	AddSubmonoid.support Bot.bot AddSubgroup AddSubgroup.instBot	—	isPointed_iff_support_eq_bot

AddSubmonoid.IsSpanning

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
maximal_isPointed 📖	mathematical	AddSubmonoid.IsPointed AddSubmonoid.IsSpanning	Maximal AddSubmonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Preorder.toLE PartialOrder.toPreorder AddSubmonoid.instPartialOrder AddSubmonoid.IsPointed	—	SetLike.le_def instIsConcreteLE mem_or_neg_mem AddSubmonoid.IsPointed.eq_zero_of_mem_of_neg_mem ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass AddSubmonoid.instAddSubmonoidClass
mem_or_neg_mem 📖	mathematical	AddSubmonoid.IsSpanning	AddSubmonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SetLike.instMembership AddSubmonoid.instSetLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	—	—
mk 📖	mathematical	AddSubmonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid SetLike.instMembership AddSubmonoid.instSetLike NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid AddGroup.toSubtractionMonoid	AddSubmonoid.IsSpanning	—	—
of_le 📖	mathematical	AddSubmonoid.IsSpanning AddSubmonoid AddMonoid.toAddZeroClass SubNegMonoid.toAddMonoid AddGroup.toSubNegMonoid Preorder.toLE PartialOrder.toPreorder AddSubmonoid.instPartialOrder	AddSubmonoid.IsSpanning	—	mem_or_neg_mem

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
gc_toSubmonoid_mulSupport 📖	mathematical	—	GaloisConnection Subgroup Submonoid Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid PartialOrder.toPreorder instPartialOrder Submonoid.instPartialOrder toSubmonoid Submonoid.mulSupport	—	SubgroupClass.toInvMemClass instSubgroupClass

Submonoid

Definitions

Name	Category	Theorems
IsMulPointed 📖	MathDef	4 math math: IsMulPointed.mk, isMulPointed_iff_mulSupport_eq_bot, IsMulPointed.of_mulSupport_eq_bot, IsMulSpanning.maximal_isMulPointed
IsMulSpanning 📖	MathDef	2 math math: IsMulSpanning.mk, IsMulSpanning.of_le
mulSupport 📖	CompOp	6 math math: coe_mulSupport, isMulPointed_iff_mulSupport_eq_bot, mem_mulSupport, Subgroup.gc_toSubmonoid_mulSupport, mulSupport_toSubmonoid, IsMulPointed.mulSupport_eq_bot

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
coe_mulSupport 📖	mathematical	—	SetLike.coe Subgroup Subgroup.instSetLike mulSupport Set Set.instInter Submonoid Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instSetLike Set.inv InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
mem_mulSupport 📖	mathematical	—	Subgroup SetLike.instMembership Subgroup.instSetLike mulSupport Submonoid Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instSetLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
mulSupport_toSubmonoid 📖	mathematical	—	Subgroup.toSubmonoid mulSupport Submonoid Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid instMin inv	—	—

Submonoid.IsMulPointed

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
eq_one_of_mem_of_inv_mem 📖	mathematical	Submonoid.IsMulPointed Submonoid Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SetLike.instMembership Submonoid.instSetLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
eq_one_of_mem_of_inv_mem₂ 📖	mathematical	Submonoid.IsMulPointed Submonoid Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SetLike.instMembership Submonoid.instSetLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	eq_one_of_mem_of_inv_mem
mk 📖	mathematical	InvOneClass.toOne DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	Submonoid.IsMulPointed	—	—
mulSupport_eq_bot 📖	mathematical	Submonoid.IsMulPointed	Submonoid.mulSupport Bot.bot Subgroup Subgroup.instBot	—	isMulPointed_iff_mulSupport_eq_bot
of_mulSupport_eq_bot 📖	mathematical	Submonoid.mulSupport Bot.bot Subgroup Subgroup.instBot	Submonoid.IsMulPointed	—	isMulPointed_iff_mulSupport_eq_bot

Submonoid.IsMulSpanning

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
maximal_isMulPointed 📖	mathematical	Submonoid.IsMulPointed Submonoid.IsMulSpanning	Maximal Submonoid Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder Submonoid.IsMulPointed	—	SetLike.le_def instIsConcreteLE mem_or_inv_mem Submonoid.IsMulPointed.eq_one_of_mem_of_inv_mem SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass
mem_or_inv_mem 📖	mathematical	Submonoid.IsMulSpanning	Submonoid Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SetLike.instMembership Submonoid.instSetLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	—	—
mk 📖	mathematical	Submonoid Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid SetLike.instMembership Submonoid.instSetLike InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid Group.toDivisionMonoid	Submonoid.IsMulSpanning	—	—
of_le 📖	mathematical	Submonoid.IsMulSpanning Submonoid Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid Preorder.toLE PartialOrder.toPreorder Submonoid.instPartialOrder	Submonoid.IsMulSpanning	—	mem_or_inv_mem

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isMulPointed_iff_mulSupport_eq_bot 📖	mathematical	—	Submonoid.IsMulPointed Submonoid.mulSupport Bot.bot Subgroup Subgroup.instBot	—	Subgroup.ext Submonoid.IsMulPointed.eq_one_of_mem_of_inv_mem SubmonoidClass.toOneMemClass Submonoid.instSubmonoidClass inv_one
isPointed_iff_support_eq_bot 📖	mathematical	—	AddSubmonoid.IsPointed AddSubmonoid.support Bot.bot AddSubgroup AddSubgroup.instBot	—	AddSubgroup.ext AddSubmonoid.mem_support AddSubgroup.mem_bot AddSubmonoid.IsPointed.eq_zero_of_mem_of_neg_mem ZeroMemClass.zero_mem AddSubmonoidClass.toZeroMemClass AddSubmonoid.instAddSubmonoidClass neg_zero

---

← Back to Index