Documentation Verification Report

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`, `instIsAddCommutative_closure`, `isAddCommutative_closure`, `mem_centralizer_iff`, `center_le_centralizer`, `centralizer_eq_top_iff_subset`, `centralizer_le`, `centralizer_univ`, `closure_le_centralizer_centralizer`, `coe_centralizer`, `instIsMulCommutative_closure`, `isMulCommutative_closure`, `mem_centralizer_iff`	18
Total	24

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`	—	—
`instIsAddCommutative_closure` 📖	mathematical	—	`IsAddCommutative` `AddSubsemigroup` `AddSemigroup.toAdd` `SetLike.instMembership` `instSetLike` `closure` `SetLike.coe` `AddMemClass.toAddSemigroup` `instAddMemClass`	—	`isAddCommutative_closure` `setLike_add_comm`
`isAddCommutative_closure` 📖	mathematical	`AddSemigroup.toAdd`	`IsAddCommutative` `AddSubsemigroup` `AddSemigroup.toAdd` `SetLike.instMembership` `instSetLike` `closure` `AddMemClass.toAddSemigroup` `instAddMemClass`	—	`closure_le_centralizer_centralizer` `IsAddCommutative.of_setLike_add_comm` `instAddMemClass` `Set.addCentralizer_addCentralizer_comm_of_comm`
`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`	—	—
`instIsMulCommutative_closure` 📖	mathematical	—	`IsMulCommutative` `Subsemigroup` `Semigroup.toMul` `SetLike.instMembership` `instSetLike` `closure` `SetLike.coe` `MulMemClass.toSemigroup` `instMulMemClass`	—	`isMulCommutative_closure` `setLike_mul_comm`
`isMulCommutative_closure` 📖	mathematical	`Semigroup.toMul`	`IsMulCommutative` `Subsemigroup` `Semigroup.toMul` `SetLike.instMembership` `instSetLike` `closure` `MulMemClass.toSemigroup` `instMulMemClass`	—	`closure_le_centralizer_centralizer` `IsMulCommutative.of_setLike_mul_comm` `instMulMemClass` `Set.centralizer_centralizer_comm_of_comm`
`mem_centralizer_iff` 📖	mathematical	—	`Subsemigroup` `Semigroup.toMul` `SetLike.instMembership` `instSetLike` `centralizer`	—	—

---

← Back to Index