Centralizer

📁 Source: Mathlib/GroupTheory/Subsemigroup/Centralizer.lean

Statistics

Metric	Count
Definitions centralizer, closureAddCommSemigroupOfComm, decidableMemCentralizer, centralizer, closureCommSemigroupOfComm, decidableMemCentralizer	6
Theorems center_le_centralizer, centralizer_eq_top_iff_subset, centralizer_le, centralizer_univ, closure_le_centralizer_centralizer, coe_centralizer, mem_centralizer_iff, center_le_centralizer, centralizer_eq_top_iff_subset, centralizer_le, centralizer_univ, closure_le_centralizer_centralizer, coe_centralizer, mem_centralizer_iff	14
Total	20

AddSubsemigroup

Definitions

Name	Category	Theorems
centralizer 📖	CompOp	8 math math: closure_le_centralizer_centralizer, AddSubmonoid.centralizer_toAddSubsemigroup, center_le_centralizer, mem_centralizer_iff, centralizer_le, centralizer_eq_top_iff_subset, coe_centralizer, centralizer_univ
closureAddCommSemigroupOfComm 📖	CompOp	—
decidableMemCentralizer 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
center_le_centralizer 📖	mathematical	—	AddSubsemigroup AddSemigroup.toAdd Preorder.toLE PartialOrder.toPreorder instPartialOrder center centralizer	—	Set.addCenter_subset_addCentralizer
centralizer_eq_top_iff_subset 📖	mathematical	—	centralizer Top.top AddSubsemigroup AddSemigroup.toAdd instTop Set Set.instHasSubset SetLike.coe instSetLike center	—	SetLike.ext'_iff Set.addCentralizer_eq_top_iff_subset
centralizer_le 📖	mathematical	Set Set.instHasSubset	AddSubsemigroup AddSemigroup.toAdd Preorder.toLE PartialOrder.toPreorder instPartialOrder centralizer	—	Set.addCentralizer_subset
centralizer_univ 📖	mathematical	—	centralizer Set.univ center AddSemigroup.toAdd	—	SetLike.ext' Set.addCentralizer_univ
closure_le_centralizer_centralizer 📖	mathematical	—	AddSubsemigroup AddSemigroup.toAdd Preorder.toLE PartialOrder.toPreorder instPartialOrder closure centralizer SetLike.coe instSetLike	—	closure_le Set.subset_addCentralizer_addCentralizer
coe_centralizer 📖	mathematical	—	SetLike.coe AddSubsemigroup AddSemigroup.toAdd instSetLike centralizer Set.addCentralizer	—	—
mem_centralizer_iff 📖	mathematical	—	AddSubsemigroup AddSemigroup.toAdd SetLike.instMembership instSetLike centralizer	—	—

Subsemigroup

Definitions

Name	Category	Theorems
centralizer 📖	CompOp	9 math math: Submonoid.centralizer_toSubsemigroup, centralizer_univ, coe_centralizer, closure_le_centralizer_centralizer, mem_centralizer_iff, centralizer_eq_top_iff_subset, NonUnitalSubsemiring.centralizer_toSubsemigroup, center_le_centralizer, centralizer_le
closureCommSemigroupOfComm 📖	CompOp	—
decidableMemCentralizer 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
center_le_centralizer 📖	mathematical	—	Subsemigroup Semigroup.toMul Preorder.toLE PartialOrder.toPreorder instPartialOrder center centralizer	—	Set.center_subset_centralizer
centralizer_eq_top_iff_subset 📖	mathematical	—	centralizer Top.top Subsemigroup Semigroup.toMul instTop Set Set.instHasSubset SetLike.coe instSetLike center	—	SetLike.ext'_iff Set.centralizer_eq_top_iff_subset
centralizer_le 📖	mathematical	Set Set.instHasSubset	Subsemigroup Semigroup.toMul Preorder.toLE PartialOrder.toPreorder instPartialOrder centralizer	—	Set.centralizer_subset
centralizer_univ 📖	mathematical	—	centralizer Set.univ center Semigroup.toMul	—	SetLike.ext' Set.centralizer_univ
closure_le_centralizer_centralizer 📖	mathematical	—	Subsemigroup Semigroup.toMul Preorder.toLE PartialOrder.toPreorder instPartialOrder closure centralizer SetLike.coe instSetLike	—	closure_le Set.subset_centralizer_centralizer
coe_centralizer 📖	mathematical	—	SetLike.coe Subsemigroup Semigroup.toMul instSetLike centralizer Set.centralizer	—	—
mem_centralizer_iff 📖	mathematical	—	Subsemigroup Semigroup.toMul SetLike.instMembership instSetLike centralizer	—	—

---

← Back to Index