Documentation Verification Report

Centralizer

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

Statistics

Metric	Count
Definitions `centralizer`, `closureAddCommMonoidOfComm`, `decidableMemCentralizer`, `centralizer`, `closureCommMonoidOfComm`, `decidableMemCentralizer`	6
Theorems `center_le_centralizer`, `centralizer_centralizer_centralizer`, `centralizer_eq_top_iff_subset`, `centralizer_le`, `centralizer_toAddSubsemigroup`, `centralizer_univ`, `closure_le_centralizer_centralizer`, `coe_centralizer`, `instIsAddCommutative_closure`, `isAddCommutative_closure`, `le_centralizer_centralizer`, `mem_centralizer_iff`, `center_le_centralizer`, `centralizer_centralizer_centralizer`, `centralizer_eq_top_iff_subset`, `centralizer_le`, `centralizer_toSubsemigroup`, `centralizer_univ`, `closure_le_centralizer_centralizer`, `coe_centralizer`, `instIsMulCommutative_closure`, `isMulCommutative_closure`, `le_centralizer_centralizer`, `mem_centralizer_iff`	24
Total	30

AddSubmonoid

Definitions

Name	Category	Theorems
`centralizer` 📖	CompOp	10 math math: `le_centralizer_centralizer`, `centralizer_centralizer_centralizer`, `centralizer_toAddSubsemigroup`, `closure_le_centralizer_centralizer`, `coe_centralizer`, `centralizer_le`, `centralizer_univ`, `centralizer_eq_top_iff_subset`, `mem_centralizer_iff`, `center_le_centralizer`
`closureAddCommMonoidOfComm` 📖	CompOp	—
`decidableMemCentralizer` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`center_le_centralizer` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `center` `centralizer`	—	`Set.addCenter_subset_addCentralizer`
`centralizer_centralizer_centralizer` 📖	mathematical	—	`centralizer` `Set.addCentralizer` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	—	`SetLike.coe_injective` `Set.addCentralizer_addCentralizer_addCentralizer`
`centralizer_eq_top_iff_subset` 📖	mathematical	—	`centralizer` `Top.top` `AddSubmonoid` `AddMonoid.toAddZeroClass` `instTop` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike` `center`	—	`SetLike.ext'_iff` `Set.addCentralizer_eq_top_iff_subset`
`centralizer_le` 📖	mathematical	`Set` `Set.instHasSubset`	`AddSubmonoid` `AddMonoid.toAddZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `centralizer`	—	`Set.addCentralizer_subset`
`centralizer_toAddSubsemigroup` 📖	mathematical	—	`toAddSubsemigroup` `AddMonoid.toAddZeroClass` `centralizer` `AddSubsemigroup.centralizer` `AddMonoid.toAddSemigroup`	—	—
`centralizer_univ` 📖	mathematical	—	`centralizer` `Set.univ` `center` `AddMonoid.toAddZeroClass`	—	`SetLike.ext'` `Set.addCentralizer_univ`
`closure_le_centralizer_centralizer` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `centralizer` `SetLike.coe` `instSetLike`	—	`closure_le` `Set.subset_addCentralizer_addCentralizer`
`coe_centralizer` 📖	mathematical	—	`SetLike.coe` `AddSubmonoid` `AddMonoid.toAddZeroClass` `instSetLike` `centralizer` `Set.addCentralizer` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	—
`instIsAddCommutative_closure` 📖	mathematical	—	`IsAddCommutative` `AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike` `closure` `SetLike.coe` `add`	—	`isAddCommutative_closure` `setLike_add_comm`
`isAddCommutative_closure` 📖	mathematical	`AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass`	`IsAddCommutative` `AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike` `closure` `add`	—	`closure_le_centralizer_centralizer` `IsAddCommutative.of_setLike_add_comm` `AddSubmonoidClass.toAddMemClass` `instAddSubmonoidClass` `Set.addCentralizer_addCentralizer_comm_of_comm`
`le_centralizer_centralizer` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `centralizer` `SetLike.coe` `instSetLike`	—	`Set.subset_addCentralizer_addCentralizer`
`mem_centralizer_iff` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike` `centralizer` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	—

Submonoid

Definitions

Name	Category	Theorems
`centralizer` 📖	CompOp	14 math math: `centralizer_toSubsemigroup`, `le_centralizer_centralizer`, `centralizer_eq_top_iff_subset`, `val_unitsCentralizerEquiv_apply_coe`, `centralizer_univ`, `centralizer_le`, `val_unitsCentralizerEquiv_symm_apply_coe`, `closure_le_centralizer_centralizer`, `Subsemiring.centralizer_toSubmonoid`, `mem_centralizer_iff`, `centralizer_centralizer_centralizer`, `coe_centralizer`, `center_le_centralizer`, `Subring.centralizer_toSubmonoid`
`closureCommMonoidOfComm` 📖	CompOp	—
`decidableMemCentralizer` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`center_le_centralizer` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `center` `centralizer`	—	`Set.center_subset_centralizer`
`centralizer_centralizer_centralizer` 📖	mathematical	—	`centralizer` `Set.centralizer` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	`SetLike.coe_injective` `Set.centralizer_centralizer_centralizer`
`centralizer_eq_top_iff_subset` 📖	mathematical	—	`centralizer` `Top.top` `Submonoid` `Monoid.toMulOneClass` `instTop` `Set` `Set.instHasSubset` `SetLike.coe` `instSetLike` `center`	—	`SetLike.ext'_iff` `Set.centralizer_eq_top_iff_subset`
`centralizer_le` 📖	mathematical	`Set` `Set.instHasSubset`	`Submonoid` `Monoid.toMulOneClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `centralizer`	—	`Set.centralizer_subset`
`centralizer_toSubsemigroup` 📖	mathematical	—	`toSubsemigroup` `Monoid.toMulOneClass` `centralizer` `Subsemigroup.centralizer` `Monoid.toSemigroup`	—	—
`centralizer_univ` 📖	mathematical	—	`centralizer` `Set.univ` `center` `Monoid.toMulOneClass`	—	`SetLike.ext'` `Set.centralizer_univ`
`closure_le_centralizer_centralizer` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `closure` `centralizer` `SetLike.coe` `instSetLike`	—	`closure_le` `Set.subset_centralizer_centralizer`
`coe_centralizer` 📖	mathematical	—	`SetLike.coe` `Submonoid` `Monoid.toMulOneClass` `instSetLike` `centralizer` `Set.centralizer` `MulOne.toMul` `MulOneClass.toMulOne`	—	—
`instIsMulCommutative_closure` 📖	mathematical	—	`IsMulCommutative` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `instSetLike` `closure` `SetLike.coe` `mul`	—	`isMulCommutative_closure` `setLike_mul_comm`
`isMulCommutative_closure` 📖	mathematical	`MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`IsMulCommutative` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `instSetLike` `closure` `mul`	—	`closure_le_centralizer_centralizer` `IsMulCommutative.of_setLike_mul_comm` `SubmonoidClass.toMulMemClass` `instSubmonoidClass` `Set.centralizer_centralizer_comm_of_comm`
`le_centralizer_centralizer` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `centralizer` `SetLike.coe` `instSetLike`	—	`Set.subset_centralizer_centralizer`
`mem_centralizer_iff` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `instSetLike` `centralizer` `MulOne.toMul` `MulOneClass.toMulOne`	—	—

---

← Back to Index