Documentation Verification Report

Center

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

Statistics

Metric	Count
Definitions `center`, `addCommSemigroup`, `decidableMemCenter`, `center`, `commSemigroup`, `decidableMemCenter`	6
Theorems `center_eq_top`, `mem_center_iff`, `center_eq_top`, `mem_center_iff`	4
Total	10

AddSubsemigroup

Definitions

Name	Category	Theorems
`center` 📖	CompOp	18 math math: `AddSubgroup.centerToAddOpposite_apply_coe`, `center_eq_top`, `center_le_centralizer`, `AddSubmonoid.centerCongr_symm_apply_coe`, `AddSubmonoid.centerToAddOpposite_symm_apply_coe`, `centerToAddOpposite_symm_apply_coe`, `mem_center_iff`, `AddSubgroup.centerCongr_apply_coe`, `centerCongr_apply_coe`, `AddSubmonoid.center_toAddSubsemigroup`, `AddSubgroup.centerCongr_symm_apply_coe`, `centralizer_eq_top_iff_subset`, `centerCongr_symm_apply_coe`, `AddSubgroup.centerToAddOpposite_symm_apply_coe`, `AddSubmonoid.centerCongr_apply_coe`, `centralizer_univ`, `centerToAddOpposite_apply_coe`, `AddSubmonoid.centerToAddOpposite_apply_coe`
`decidableMemCenter` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`center_eq_top` 📖	mathematical	—	`center` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `Top.top` `AddSubsemigroup` `instTop`	—	`SetLike.coe_injective` `Set.addCenter_eq_univ`
`mem_center_iff` 📖	mathematical	—	`AddSubsemigroup` `AddSemigroup.toAdd` `SetLike.instMembership` `instSetLike` `center`	—	`AddSemigroup.mem_center_iff`

AddSubsemigroup.center

Definitions

Name	Category	Theorems
`addCommSemigroup` 📖	CompOp	4 math math: `AddSubsemigroup.centerToAddOpposite_symm_apply_coe`, `AddSubsemigroup.centerCongr_apply_coe`, `AddSubsemigroup.centerCongr_symm_apply_coe`, `AddSubsemigroup.centerToAddOpposite_apply_coe`

Subsemigroup

Definitions

Name	Category	Theorems
`center` 📖	CompOp	37 math math: `Subgroup.centerCongr_symm_apply_coe`, `centerToMulOpposite_apply_coe`, `centerCongr_symm_apply_coe`, `Subring.centerCongr_apply_coe`, `NonUnitalSubsemiring.centerCongr_symm_apply_coe`, `centralizer_univ`, `NonUnitalSubring.centerCongr_apply_coe`, `Subsemiring.centerCongr_symm_apply_coe`, `NonUnitalSubsemiring.centerToMulOpposite_symm_apply_coe`, `Subgroup.centerCongr_apply_coe`, `Submonoid.center_toSubsemigroup`, `Submonoid.centerToMulOpposite_apply_coe`, `Subgroup.centerToMulOpposite_apply_coe`, `mem_center_iff`, `Subsemiring.centerCongr_apply_coe`, `Subring.centerToMulOpposite_symm_apply_coe`, `Subsemiring.centerToMulOpposite_symm_apply_coe`, `NonUnitalSubring.centerCongr_symm_apply_coe`, `Subsemiring.centerToMulOpposite_apply_coe`, `Submonoid.centerToMulOpposite_symm_apply_coe`, `centralizer_eq_top_iff_subset`, `Submonoid.centerCongr_symm_apply_coe`, `Subring.centerToMulOpposite_apply_coe`, `centerToMulOpposite_symm_apply_coe`, `Module.End.mem_subsemigroupCenter_iff`, `Matrix.subsemigroupCenter_eq_scalar_map`, `NonUnitalSubring.centerToMulOpposite_symm_apply_coe`, `Subring.centerCongr_symm_apply_coe`, `center_eq_top`, `NonUnitalSubsemiring.centerToMulOpposite_apply_coe`, `center_le_centralizer`, `NonUnitalSubsemiring.center_toSubsemigroup`, `NonUnitalSubsemiring.centerCongr_apply_coe`, `Submonoid.centerCongr_apply_coe`, `Subgroup.centerToMulOpposite_symm_apply_coe`, `NonUnitalSubring.centerToMulOpposite_apply_coe`, `centerCongr_apply_coe`
`decidableMemCenter` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`center_eq_top` 📖	mathematical	—	`center` `CommMagma.toMul` `CommSemigroup.toCommMagma` `Top.top` `Subsemigroup` `instTop`	—	`SetLike.coe_injective` `Set.center_eq_univ`
`mem_center_iff` 📖	mathematical	—	`Subsemigroup` `Semigroup.toMul` `SetLike.instMembership` `instSetLike` `center`	—	`Semigroup.mem_center_iff`

Subsemigroup.center

Definitions

Name	Category	Theorems
`commSemigroup` 📖	CompOp	4 math math: `Subsemigroup.centerToMulOpposite_apply_coe`, `Subsemigroup.centerCongr_symm_apply_coe`, `Subsemigroup.centerToMulOpposite_symm_apply_coe`, `Subsemigroup.centerCongr_apply_coe`

---

← Back to Index