Order

📁 Source: Mathlib/Algebra/Group/Subgroup/Order.lean

Statistics

Metric	Count
Definitions	0
Theorems strictMono_subsemigroupCongr, strictMono_symm, toIsOrderedAddMonoid, strictMono_topEquiv, strictMono_subsemigroupCongr, strictMono_symm, normal_of_coatom, isCoatom_comap, isCoatom_comap_of_surjective, isCoatom_map, toIsOrderedMonoid, strictMono_topEquiv, abs_mem_iff, instIsModularLatticeAddSubgroup, instIsModularLatticeSubgroup, mabs_mem_iff	16
Total	16

AddEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strictMono_subsemigroupCongr 📖	mathematical	—	StrictMono AddSubsemigroup AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership AddSubsemigroup.instSetLike Subtype.preorder PartialOrder.toPreorder DFunLike.coe AddEquiv AddMemClass.add AddSubsemigroup.instAddMemClass EquivLike.toFunLike instEquivLike subsemigroupCongr	—	—
strictMono_symm 📖	mathematical	StrictMono PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DFunLike.coe AddEquiv AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid EquivLike.toFunLike instEquivLike	symm	—	StrictMono.lt_iff_lt apply_symm_apply

AddSubgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
toIsOrderedAddMonoid 📖	mathematical	—	IsOrderedAddMonoid AddSubgroup AddCommGroup.toAddGroup SetLike.instMembership instSetLike AddCommGroup.toAddCommMonoid toAddCommGroup Subtype.partialOrder	—	Function.Injective.isOrderedAddMonoid

AddSubsemigroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strictMono_topEquiv 📖	mathematical	—	StrictMono AddSubsemigroup AddZero.toAdd AddZeroClass.toAddZero AddMonoid.toAddZeroClass AddCommMonoid.toAddMonoid SetLike.instMembership instSetLike Top.top instTop Subtype.preorder PartialOrder.toPreorder DFunLike.coe AddEquiv AddMemClass.add instAddMemClass EquivLike.toFunLike AddEquiv.instEquivLike topEquiv	—	—

MulEquiv

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strictMono_subsemigroupCongr 📖	mathematical	—	StrictMono Subsemigroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership Subsemigroup.instSetLike Subtype.preorder PartialOrder.toPreorder DFunLike.coe MulEquiv MulMemClass.mul Subsemigroup.instMulMemClass EquivLike.toFunLike instEquivLike subsemigroupCongr	—	—
strictMono_symm 📖	mathematical	StrictMono PartialOrder.toPreorder SemilatticeInf.toPartialOrder Lattice.toSemilatticeInf DistribLattice.toLattice instDistribLatticeOfLinearOrder DFunLike.coe MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid EquivLike.toFunLike instEquivLike	symm	—	StrictMono.lt_iff_lt apply_symm_apply

Subgroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
isCoatom_comap 📖	mathematical	—	IsCoatom Subgroup PartialOrder.toPreorder instPartialOrder BoundedOrder.toOrderTop Preorder.toLE CompleteLattice.toBoundedOrder instCompleteLattice comap MonoidHomClass.toMonoidHom MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid EquivLike.toFunLike MulEquiv.instEquivLike MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass	—	OrderIso.isCoatom_iff
isCoatom_comap_of_surjective 📖	mathematical	DFunLike.coe MonoidHom MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid MonoidHom.instFunLike IsCoatom Subgroup PartialOrder.toPreorder instPartialOrder BoundedOrder.toOrderTop Preorder.toLE CompleteLattice.toBoundedOrder instCompleteLattice	comap	—	comap_top comap_injective comap_map_eq_self LE.le.trans ker_le_comap LT.lt.le comap_lt_comap_of_surjective
isCoatom_map 📖	mathematical	—	IsCoatom Subgroup SetLike.instMembership instSetLike toGroup PartialOrder.toPreorder instPartialOrder BoundedOrder.toOrderTop Preorder.toLE CompleteLattice.toBoundedOrder instCompleteLattice map MonoidHomClass.toMonoidHom MulEquiv MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass DivInvMonoid.toMonoid Group.toDivInvMonoid mul EquivLike.toFunLike MulEquiv.instEquivLike MulEquivClass.instMonoidHomClass MulEquiv.instMulEquivClass	—	OrderIso.isCoatom_iff
toIsOrderedMonoid 📖	mathematical	—	IsOrderedMonoid Subgroup CommGroup.toGroup SetLike.instMembership instSetLike CommGroup.toCommMonoid toCommGroup Subtype.partialOrder	—	Function.Injective.isOrderedMonoid

Subgroup.NormalizerCondition

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
normal_of_coatom 📖	mathematical	NormalizerCondition IsCoatom Subgroup PartialOrder.toPreorder Subgroup.instPartialOrder BoundedOrder.toOrderTop Preorder.toLE CompleteLattice.toBoundedOrder Subgroup.instCompleteLattice	Subgroup.Normal	—	Subgroup.normalizer_eq_top_iff lt_top_iff_ne_top

Subsemigroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
strictMono_topEquiv 📖	mathematical	—	StrictMono Subsemigroup MulOne.toMul MulOneClass.toMulOne Monoid.toMulOneClass CommMonoid.toMonoid SetLike.instMembership instSetLike Top.top instTop Subtype.preorder PartialOrder.toPreorder DFunLike.coe MulEquiv MulMemClass.mul instMulMemClass EquivLike.toFunLike MulEquiv.instEquivLike topEquiv	—	—

(root)

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
abs_mem_iff 📖	mathematical	—	SetLike.instMembership abs DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	abs_choice neg_mem_iff
instIsModularLatticeAddSubgroup 📖	mathematical	—	IsModularLattice AddSubgroup AddCommGroup.toAddGroup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice AddSubgroup.instCompleteLattice	—	AddSubgroup.mem_sup AddSubgroup.mem_inf add_mem_cancel_left AddSubgroup.instAddSubgroupClass
instIsModularLatticeSubgroup 📖	mathematical	—	IsModularLattice Subgroup CommGroup.toGroup ConditionallyCompleteLattice.toLattice CompleteLattice.toConditionallyCompleteLattice Subgroup.instCompleteLattice	—	Subgroup.mem_sup Subgroup.mem_inf mul_mem_cancel_left Subgroup.instSubgroupClass
mabs_mem_iff 📖	mathematical	—	SetLike.instMembership mabs DistribLattice.toLattice instDistribLatticeOfLinearOrder	—	mabs_choice

---

← Back to Index