Documentation Verification Report

Center

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

Statistics

Metric	Count
Definitions `center`, `addCommMonoid`, `addCommMonoid'`, `centerCongr`, `centerToAddOpposite`, `decidableMemCenter`, `centerCongr`, `centerToAddOpposite`, `center`, `commMonoid`, `commMonoid'`, `centerCongr`, `centerToMulOpposite`, `decidableMemCenter`, `centerCongr`, `centerToMulOpposite`, `addUnitsCenterToCenterAddUnits`, `unitsCenterToCenterUnits`	18
Theorems `apply_mem_center`, `apply_mem_center_iff`, `op_mem_center_iff`, `unop_mem_center_iff`, `centerCongr_apply_coe`, `centerCongr_symm_apply_coe`, `centerToAddOpposite_apply_coe`, `centerToAddOpposite_symm_apply_coe`, `center_toAddSubsemigroup`, `coe_center`, `mem_center_iff`, `centerCongr_apply_coe`, `centerCongr_symm_apply_coe`, `centerToAddOpposite_apply_coe`, `centerToAddOpposite_symm_apply_coe`, `apply_mem_center`, `apply_mem_center_iff`, `op_mem_center_iff`, `unop_mem_center_iff`, `smulCommClass_left`, `smulCommClass_right`, `centerCongr_apply_coe`, `centerCongr_symm_apply_coe`, `centerToMulOpposite_apply_coe`, `centerToMulOpposite_symm_apply_coe`, `center_eq_top`, `center_toSubsemigroup`, `coe_center`, `instSMulCommClassSubtypeMemCenter`, `instSMulCommClassSubtypeMemCenter_1`, `mem_center_iff`, `centerCongr_apply_coe`, `centerCongr_symm_apply_coe`, `centerToMulOpposite_apply_coe`, `centerToMulOpposite_symm_apply_coe`, `addUnitsCenterToCenterAddUnits_injective`, `unitsCenterToCenterUnits_injective`, `val_addUnitsCenterToCenterAddUnits_apply_coe`, `val_unitsCenterToCenterUnits_apply_coe`	39
Total	57

AddEquivClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_mem_center` 📖	mathematical	`Set` `Set.instMembership` `Set.addCenter`	`DFunLike.coe` `EquivLike.toFunLike`	—	`AddEquiv.injective` `map_add` `instAddHomClass` `AddEquiv.instAddEquivClass` `AddEquiv.symm_apply_apply` `AddCommute.eq` `IsAddCentral.comm` `isAddCentral_iff` `IsAddCentral.right_comm`
`apply_mem_center_iff` 📖	mathematical	—	`Set` `Set.instMembership` `Set.addCenter` `DFunLike.coe` `EquivLike.toFunLike`	—	`coe_symm_apply_apply` `apply_mem_center` `AddEquiv.instAddEquivClass`

AddOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`op_mem_center_iff` 📖	mathematical	—	`AddOpposite` `Set` `Set.instMembership` `Set.addCenter` `instAdd` `op`	—	`Set.mem_addCenter_iff` `isAddCentral_iff` `forall` `addCommute_op`
`unop_mem_center_iff` 📖	mathematical	—	`Set` `Set.instMembership` `Set.addCenter` `unop` `AddOpposite` `instAdd`	—	`op_mem_center_iff`

AddSubmonoid

Definitions

Name	Category	Theorems
`center` 📖	CompOp	13 math math: `mem_center_iff`, `centerCongr_symm_apply_coe`, `centerToAddOpposite_symm_apply_coe`, `center_toAddSubsemigroup`, `AddSubgroup.center_toAddSubmonoid`, `centralizer_univ`, `centralizer_eq_top_iff_subset`, `centerCongr_apply_coe`, `coe_center`, `center_le_centralizer`, `val_addUnitsCenterToCenterAddUnits_apply_coe`, `addUnitsCenterToCenterAddUnits_injective`, `centerToAddOpposite_apply_coe`
`centerCongr` 📖	CompOp	2 math math: `centerCongr_symm_apply_coe`, `centerCongr_apply_coe`
`centerToAddOpposite` 📖	CompOp	2 math math: `centerToAddOpposite_symm_apply_coe`, `centerToAddOpposite_apply_coe`
`decidableMemCenter` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`centerCongr_apply_coe` 📖	mathematical	—	`AddSubsemigroup` `AddZero.toAdd` `AddZeroClass.toAddZero` `SetLike.instMembership` `AddSubsemigroup.instSetLike` `AddSubsemigroup.center` `DFunLike.coe` `AddEquiv` `AddSubmonoid` `instSetLike` `center` `add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `centerCongr`	—	—
`centerCongr_symm_apply_coe` 📖	mathematical	—	`AddSubsemigroup` `AddZero.toAdd` `AddZeroClass.toAddZero` `SetLike.instMembership` `AddSubsemigroup.instSetLike` `AddSubsemigroup.center` `DFunLike.coe` `AddEquiv` `AddSubmonoid` `instSetLike` `center` `add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `centerCongr`	—	—
`centerToAddOpposite_apply_coe` 📖	mathematical	—	`AddOpposite` `AddSubsemigroup` `AddOpposite.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `SetLike.instMembership` `AddSubsemigroup.instSetLike` `AddSubsemigroup.center` `DFunLike.coe` `AddEquiv` `AddSubmonoid` `instSetLike` `center` `AddOpposite.instAddZeroClass` `add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `centerToAddOpposite` `AddOpposite.op`	—	—
`centerToAddOpposite_symm_apply_coe` 📖	mathematical	—	`AddSubsemigroup` `AddZero.toAdd` `AddZeroClass.toAddZero` `SetLike.instMembership` `AddSubsemigroup.instSetLike` `AddSubsemigroup.center` `DFunLike.coe` `AddEquiv` `AddOpposite` `AddSubmonoid` `AddOpposite.instAddZeroClass` `instSetLike` `center` `add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `centerToAddOpposite` `AddOpposite.unop` `AddOpposite.instAdd`	—	—
`center_toAddSubsemigroup` 📖	mathematical	—	`toAddSubsemigroup` `center` `AddSubsemigroup.center` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	—
`coe_center` 📖	mathematical	—	`SetLike.coe` `AddSubmonoid` `instSetLike` `center` `Set.addCenter` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	—
`mem_center_iff` 📖	mathematical	—	`AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `instSetLike` `center` `AddZero.toAdd` `AddZeroClass.toAddZero`	—	`AddSemigroup.mem_center_iff`

AddSubmonoid.center

Definitions

Name	Category	Theorems
`addCommMonoid` 📖	CompOp	—
`addCommMonoid'` 📖	CompOp	—

AddSubsemigroup

Definitions

Name	Category	Theorems
`centerCongr` 📖	CompOp	2 math math: `centerCongr_apply_coe`, `centerCongr_symm_apply_coe`
`centerToAddOpposite` 📖	CompOp	2 math math: `centerToAddOpposite_symm_apply_coe`, `centerToAddOpposite_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`centerCongr_apply_coe` 📖	mathematical	—	`AddSubsemigroup` `SetLike.instMembership` `instSetLike` `center` `DFunLike.coe` `AddEquiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `center.addCommSemigroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `centerCongr`	—	—
`centerCongr_symm_apply_coe` 📖	mathematical	—	`AddSubsemigroup` `SetLike.instMembership` `instSetLike` `center` `DFunLike.coe` `AddEquiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `center.addCommSemigroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `centerCongr`	—	—
`centerToAddOpposite_apply_coe` 📖	mathematical	—	`AddOpposite` `AddSubsemigroup` `AddOpposite.instAdd` `SetLike.instMembership` `instSetLike` `center` `DFunLike.coe` `AddEquiv` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `center.addCommSemigroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `centerToAddOpposite` `AddOpposite.op`	—	—
`centerToAddOpposite_symm_apply_coe` 📖	mathematical	—	`AddSubsemigroup` `SetLike.instMembership` `instSetLike` `center` `DFunLike.coe` `AddEquiv` `AddOpposite` `AddOpposite.instAdd` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `center.addCommSemigroup` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `centerToAddOpposite` `AddOpposite.unop`	—	—

MulEquivClass

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`apply_mem_center` 📖	mathematical	`Set` `Set.instMembership` `Set.center`	`DFunLike.coe` `EquivLike.toFunLike`	—	`MulEquiv.injective` `map_mul` `instMulHomClass` `MulEquiv.instMulEquivClass` `MulEquiv.symm_apply_apply` `Commute.eq` `IsMulCentral.comm` `isMulCentral_iff` `IsMulCentral.right_comm`
`apply_mem_center_iff` 📖	mathematical	—	`Set` `Set.instMembership` `Set.center` `DFunLike.coe` `EquivLike.toFunLike`	—	`coe_symm_apply_apply` `apply_mem_center` `MulEquiv.instMulEquivClass`

MulOpposite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`op_mem_center_iff` 📖	mathematical	—	`MulOpposite` `Set` `Set.instMembership` `Set.center` `instMul` `op`	—	—
`unop_mem_center_iff` 📖	mathematical	—	`Set` `Set.instMembership` `Set.center` `unop` `MulOpposite` `instMul`	—	`op_mem_center_iff`

Submonoid

Definitions

Name	Category	Theorems
`center` 📖	CompOp	22 math math: `centralizer_eq_top_iff_subset`, `val_unitsCenterToCenterUnits_apply_coe`, `coe_center`, `center_toSubsemigroup`, `centerToMulOpposite_apply_coe`, `centralizer_univ`, `instSMulCommClassSubtypeMemCenter_1`, `center_eq_top`, `Subgroup.val_centerUnitsEquivUnitsCenter_symm_apply_coe`, `centerToMulOpposite_symm_apply_coe`, `unitsCenterToCenterUnits_injective`, `instSMulCommClassSubtypeMemCenter`, `centerCongr_symm_apply_coe`, `Matrix.submonoidCenter_eq_scalar_map`, `Subgroup.val_centerUnitsEquivUnitsCenter_apply_coe`, `center.smulCommClass_left`, `center.smulCommClass_right`, `mem_center_iff`, `Module.End.mem_submonoidCenter_iff`, `centerCongr_apply_coe`, `center_le_centralizer`, `Subgroup.center_toSubmonoid`
`centerCongr` 📖	CompOp	2 math math: `centerCongr_symm_apply_coe`, `centerCongr_apply_coe`
`centerToMulOpposite` 📖	CompOp	2 math math: `centerToMulOpposite_apply_coe`, `centerToMulOpposite_symm_apply_coe`
`decidableMemCenter` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`centerCongr_apply_coe` 📖	mathematical	—	`Subsemigroup` `MulOne.toMul` `MulOneClass.toMulOne` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `MulEquiv` `Submonoid` `instSetLike` `center` `mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `centerCongr`	—	—
`centerCongr_symm_apply_coe` 📖	mathematical	—	`Subsemigroup` `MulOne.toMul` `MulOneClass.toMulOne` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `MulEquiv` `Submonoid` `instSetLike` `center` `mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `centerCongr`	—	—
`centerToMulOpposite_apply_coe` 📖	mathematical	—	`MulOpposite` `Subsemigroup` `MulOpposite.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `MulEquiv` `Submonoid` `instSetLike` `center` `MulOpposite.instMulOneClass` `mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `centerToMulOpposite` `MulOpposite.op`	—	—
`centerToMulOpposite_symm_apply_coe` 📖	mathematical	—	`Subsemigroup` `MulOne.toMul` `MulOneClass.toMulOne` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `MulEquiv` `MulOpposite` `Submonoid` `MulOpposite.instMulOneClass` `instSetLike` `center` `mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `centerToMulOpposite` `MulOpposite.unop` `MulOpposite.instMul`	—	—
`center_eq_top` 📖	mathematical	—	`center` `Monoid.toMulOneClass` `CommMonoid.toMonoid` `Top.top` `Submonoid` `instTop`	—	`SetLike.coe_injective` `Set.center_eq_univ`
`center_toSubsemigroup` 📖	mathematical	—	`toSubsemigroup` `center` `Subsemigroup.center` `MulOne.toMul` `MulOneClass.toMulOne`	—	—
`coe_center` 📖	mathematical	—	`SetLike.coe` `Submonoid` `instSetLike` `center` `Set.center` `MulOne.toMul` `MulOneClass.toMulOne`	—	—
`instSMulCommClassSubtypeMemCenter` 📖	mathematical	—	`SMulCommClass` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `instSetLike` `center` `smul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction`	—	`Semigroup.mem_center_iff` `smul_smul`
`instSMulCommClassSubtypeMemCenter_1` 📖	mathematical	—	`SMulCommClass` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `instSetLike` `center` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `smul`	—	`SMulCommClass.symm` `instSMulCommClassSubtypeMemCenter`
`mem_center_iff` 📖	mathematical	—	`Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `instSetLike` `center` `MulOne.toMul` `MulOneClass.toMulOne`	—	`Semigroup.mem_center_iff`

Submonoid.center

Definitions

Name	Category	Theorems
`commMonoid` 📖	CompOp	—
`commMonoid'` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`smulCommClass_left` 📖	mathematical	—	`SMulCommClass` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.center` `Submonoid.smul` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction`	—	`Commute.left_comm` `IsMulCentral.comm` `Subtype.prop`
`smulCommClass_right` 📖	mathematical	—	`SMulCommClass` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.center` `SemigroupAction.toSMul` `Monoid.toSemigroup` `MulAction.toSemigroupAction` `Monoid.toMulAction` `Submonoid.smul`	—	`SMulCommClass.symm` `smulCommClass_left`

Subsemigroup

Definitions

Name	Category	Theorems
`centerCongr` 📖	CompOp	2 math math: `centerCongr_symm_apply_coe`, `centerCongr_apply_coe`
`centerToMulOpposite` 📖	CompOp	2 math math: `centerToMulOpposite_apply_coe`, `centerToMulOpposite_symm_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`centerCongr_apply_coe` 📖	mathematical	—	`Subsemigroup` `SetLike.instMembership` `instSetLike` `center` `DFunLike.coe` `MulEquiv` `CommMagma.toMul` `CommSemigroup.toCommMagma` `center.commSemigroup` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `centerCongr`	—	—
`centerCongr_symm_apply_coe` 📖	mathematical	—	`Subsemigroup` `SetLike.instMembership` `instSetLike` `center` `DFunLike.coe` `MulEquiv` `CommMagma.toMul` `CommSemigroup.toCommMagma` `center.commSemigroup` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `centerCongr`	—	—
`centerToMulOpposite_apply_coe` 📖	mathematical	—	`MulOpposite` `Subsemigroup` `MulOpposite.instMul` `SetLike.instMembership` `instSetLike` `center` `DFunLike.coe` `MulEquiv` `CommMagma.toMul` `CommSemigroup.toCommMagma` `center.commSemigroup` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `centerToMulOpposite` `MulOpposite.op`	—	—
`centerToMulOpposite_symm_apply_coe` 📖	mathematical	—	`Subsemigroup` `SetLike.instMembership` `instSetLike` `center` `DFunLike.coe` `MulEquiv` `MulOpposite` `MulOpposite.instMul` `CommMagma.toMul` `CommSemigroup.toCommMagma` `center.commSemigroup` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `centerToMulOpposite` `MulOpposite.unop`	—	—

(root)

Definitions

Name	Category	Theorems
`addUnitsCenterToCenterAddUnits` 📖	CompOp	2 math math: `val_addUnitsCenterToCenterAddUnits_apply_coe`, `addUnitsCenterToCenterAddUnits_injective`
`unitsCenterToCenterUnits` 📖	CompOp	2 math math: `val_unitsCenterToCenterUnits_apply_coe`, `unitsCenterToCenterUnits_injective`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addUnitsCenterToCenterAddUnits_injective` 📖	mathematical	—	`AddUnits` `AddSubmonoid` `AddMonoid.toAddZeroClass` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.center` `AddSubmonoid.toAddMonoid` `AddUnits.instAddZeroClass` `DFunLike.coe` `AddMonoidHom` `AddZeroClass.toAddZero` `AddSubmonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `addUnitsCenterToCenterAddUnits`	—	`AddUnits.ext`
`unitsCenterToCenterUnits_injective` 📖	mathematical	—	`Units` `Submonoid` `Monoid.toMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.center` `Submonoid.toMonoid` `Units.instMulOneClass` `DFunLike.coe` `MonoidHom` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `MonoidHom.instFunLike` `unitsCenterToCenterUnits`	—	`Units.ext`
`val_addUnitsCenterToCenterAddUnits_apply_coe` 📖	mathematical	—	`AddUnits.val` `AddUnits` `AddSubmonoid` `AddUnits.instAddZeroClass` `SetLike.instMembership` `AddSubmonoid.instSetLike` `AddSubmonoid.center` `DFunLike.coe` `AddMonoidHom` `AddMonoid.toAddZeroClass` `AddSubmonoid.toAddMonoid` `AddZeroClass.toAddZero` `AddSubmonoid.toAddZeroClass` `AddMonoidHom.instFunLike` `addUnitsCenterToCenterAddUnits`	—	—
`val_unitsCenterToCenterUnits_apply_coe` 📖	mathematical	—	`Units.val` `Units` `Submonoid` `Units.instMulOneClass` `SetLike.instMembership` `Submonoid.instSetLike` `Submonoid.center` `DFunLike.coe` `MonoidHom` `Monoid.toMulOneClass` `Submonoid.toMonoid` `MulOneClass.toMulOne` `Submonoid.toMulOneClass` `MonoidHom.instFunLike` `unitsCenterToCenterUnits`	—	—

---

← Back to Index