Documentation Verification Report

Center

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

Statistics

Metric	Count
Definitions `center`, `centerCongr`, `centerToAddOpposite`, `commGroupOfCenterEqTop`, `center`, `centerCongr`, `centerToMulOpposite`, `decidableMemCenter`	8
Theorems `centerCharacteristic`, `centerCongr_apply_coe`, `centerCongr_symm_apply_coe`, `centerToAddOpposite_apply_coe`, `centerToAddOpposite_symm_apply_coe`, `center_le_normalizer`, `center_toAddSubmonoid`, `coe_center`, `instNormalCenter`, `mem_center_iff`, `center_eq_top`, `mk_bijOn`, `eq_of_left_mem_center`, `eq_of_right_mem_center`, `isMulCommutative`, `centerCharacteristic`, `centerCongr_apply_coe`, `centerCongr_symm_apply_coe`, `centerToMulOpposite_apply_coe`, `centerToMulOpposite_symm_apply_coe`, `center_le_normalizer`, `center_toSubmonoid`, `coe_center`, `instNormalCenter`, `mem_center_iff`	25
Total	33

AddSubgroup

Definitions

Name	Category	Theorems
`center` 📖	CompOp	16 math math: `centerToAddOpposite_apply_coe`, `instNormalCenter`, `centerCongr_apply_coe`, `center_eq_infi'`, `center_toAddSubmonoid`, `coe_center`, `centerCongr_symm_apply_coe`, `centralizer_eq_top_iff_subset`, `QuotientAddGroup.comap_comap_center`, `mem_center_iff`, `centerToAddOpposite_symm_apply_coe`, `center_eq_iInf`, `centralizer_univ`, `center_le_normalizer`, `center_le_centralizer`, `centerCharacteristic`
`centerCongr` 📖	CompOp	2 math math: `centerCongr_apply_coe`, `centerCongr_symm_apply_coe`
`centerToAddOpposite` 📖	CompOp	2 math math: `centerToAddOpposite_apply_coe`, `centerToAddOpposite_symm_apply_coe`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`centerCharacteristic` 📖	mathematical	—	`Characteristic` `center`	—	`characteristic_iff_comap_le` `mem_center_iff` `AddEquiv.injective` `map_add` `AddMonoidHomClass.toAddHomClass` `AddEquivClass.instAddMonoidHomClass` `AddEquiv.instAddEquivClass` `AddCommute.symm` `IsAddCentral.comm`
`centerCongr_apply_coe` 📖	mathematical	—	`AddSubsemigroup` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SetLike.instMembership` `AddSubsemigroup.instSetLike` `AddSubsemigroup.center` `DFunLike.coe` `AddEquiv` `AddSubgroup` `instSetLike` `center` `add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `centerCongr`	—	—
`centerCongr_symm_apply_coe` 📖	mathematical	—	`AddSubsemigroup` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SetLike.instMembership` `AddSubsemigroup.instSetLike` `AddSubsemigroup.center` `DFunLike.coe` `AddEquiv` `AddSubgroup` `instSetLike` `center` `add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `centerCongr`	—	—
`centerToAddOpposite_apply_coe` 📖	mathematical	—	`AddOpposite` `AddSubsemigroup` `AddOpposite.instAdd` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SetLike.instMembership` `AddSubsemigroup.instSetLike` `AddSubsemigroup.center` `DFunLike.coe` `AddEquiv` `AddSubgroup` `instSetLike` `center` `AddOpposite.instAddGroup` `add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `centerToAddOpposite` `AddOpposite.op`	—	—
`centerToAddOpposite_symm_apply_coe` 📖	mathematical	—	`AddSubsemigroup` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid` `SetLike.instMembership` `AddSubsemigroup.instSetLike` `AddSubsemigroup.center` `DFunLike.coe` `AddEquiv` `AddOpposite` `AddSubgroup` `AddOpposite.instAddGroup` `instSetLike` `center` `add` `EquivLike.toFunLike` `AddEquiv.instEquivLike` `AddEquiv.symm` `centerToAddOpposite` `AddOpposite.unop` `AddOpposite.instAdd`	—	—
`center_le_normalizer` 📖	mathematical	—	`AddSubgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `center` `normalizer`	—	`mem_center_iff` `add_assoc` `add_neg_cancel` `add_zero`
`center_toAddSubmonoid` 📖	mathematical	—	`toAddSubmonoid` `center` `AddSubmonoid.center` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—
`coe_center` 📖	mathematical	—	`SetLike.coe` `AddSubgroup` `instSetLike` `center` `Set.addCenter` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	—
`instNormalCenter` 📖	mathematical	—	`Normal` `center`	—	`mem_center_iff` `add_assoc` `add_neg_cancel` `add_zero`
`mem_center_iff` 📖	mathematical	—	`AddSubgroup` `SetLike.instMembership` `instSetLike` `center` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	—	`AddSemigroup.mem_center_iff`

CommGroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`center_eq_top` 📖	mathematical	—	`Subgroup.center` `toGroup` `Top.top` `Subgroup` `Subgroup.instTop`	—	`Subgroup.eq_top_iff'` `Subgroup.mem_center_iff` `mul_comm`

ConjClasses

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mk_bijOn` 📖	mathematical	—	`Set.BijOn` `ConjClasses` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.coe` `Subgroup` `Subgroup.instSetLike` `Subgroup.center` `Compl.compl` `Set` `Set.instCompl` `noncenter`	—	`IsConj.eq_of_right_mem_center` `IsConj.eq_of_left_mem_center` `mk_eq_mk_iff_isConj` `SetLike.mem_coe` `Subgroup.mem_center_iff` `mul_inv_eq_iff_eq_mul` `mem_carrier_iff_mk_eq` `isConj_comm` `isConj_iff`

Group

Definitions

Name	Category	Theorems
`commGroupOfCenterEqTop` 📖	CompOp	—

IsConj

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`eq_of_left_mem_center` 📖	—	`IsConj` `Set` `Set.instMembership` `Set.center` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—	`IsMulCentral.comm`
`eq_of_right_mem_center` 📖	—	`IsConj` `Set` `Set.instMembership` `Set.center` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	—	—	`eq_of_left_mem_center` `symm`

Subgroup

Definitions

Name	Category	Theorems
`center` 📖	CompOp	63 math math: `IsPGroup.center_nontrivial`, `ConjAct.fixedPoints_eq_center`, `Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_apply`, `index_center_le_pow`, `IsPGroup.card_center_eq_prime_pow`, `centerCongr_symm_apply_coe`, `nilpotencyClass_quotient_center`, `Matrix.GeneralLinearGroup.mem_center_iff_val_mem_range_scalar`, `centralizer_univ`, `finiteIndex_center`, `SpecialLinearGroup.mem_center_iff`, `center.smulCommClass_right`, `centerCharacteristic`, `Matrix.SpecialLinearGroup.center_equiv_rootsOfUnity'_symm_apply_coe_coe`, `CommGroup.center_eq_top`, `Matrix.GeneralLinearGroup.center_eq_range_scalar`, `Matrix.SpecialLinearGroup.center_eq_bot_of_subsingleton`, `SpecialLinearGroup.centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq`, `centerCongr_apply_coe`, `centerToMulOpposite_apply_coe`, `mem_center_iff`, `alternatingGroup.center_eq_bot`, `centralizer_eq_top_iff_subset`, `instNormalCenter`, `SpecialLinearGroup.centerEquivRootsOfUnity_symm_apply`, `center_le_normalizer`, `val_centerUnitsEquivUnitsCenter_symm_apply_coe`, `Matrix.SpecialLinearGroup.scalar_eq_coe_self_center`, `card_commutator_dvd_index_center_pow`, `IsPGroup.cyclic_center_quotient_of_card_eq_prime_sq`, `Sylow.le_center_or_le_commutator`, `MonoidHom.transfer_center_eq_pow`, `DihedralGroup.center_eq_bot_of_odd_ne_one`, `IsPGroup.bot_lt_center`, `val_centerUnitsEquivUnitsCenter_apply_coe`, `comap_upperCentralSeries_quotient_center`, `center.smulCommClass_left`, `Matrix.GeneralLinearGroup.mem_center_iff_val_eq_scalar`, `SpecialLinearGroup.centerEquivRootsOfUnity_apply`, `commutator_centralizer_commutator_le_center`, `SpecialLinearGroup.center_eq_bot_of_finrank_le_one`, `MonoidHom.transferCenterPow_apply`, `ConjClasses.mk_bijOn`, `Matrix.GeneralLinearGroup.center_eq_range_units`, `Matrix.SpecialLinearGroup.eq_scalar_center_equiv_rootsOfUnity`, `coe_center`, `center_le_centralizer`, `upperCentralSeries_one`, `quotientCenterEmbedding_apply`, `center_eq_infi'`, `center_eq_iInf`, `SpecialLinearGroup.centerEquivRootsOfUnity_apply_apply`, `upperCentralSeriesStep_eq_comap_center`, `nilpotencyClass_eq_quotient_center_plus_one`, `QuotientGroup.comap_comap_center`, `Group.nat_card_center_add_sum_card_noncenter_eq_card`, `centerToMulOpposite_symm_apply_coe`, `Group.card_center_add_sum_card_noncenter_eq_card`, `commutator_eq_bot_iff_center_eq_top`, `SpecialLinearGroup.centerEquivRootsOfUnity_apply_of_finrank_le_one`, `center_toSubmonoid`, `Matrix.SpecialLinearGroup.mem_center_iff`, `center.isMulCommutative`
`centerCongr` 📖	CompOp	3 math math: `centerCongr_symm_apply_coe`, `SpecialLinearGroup.centerCongr_toLin_equiv_trans_centerEquivRootsOfUnity_eq`, `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
`centerCharacteristic` 📖	mathematical	—	`Characteristic` `center`	—	`characteristic_iff_comap_le` `mem_center_iff` `MulEquiv.injective` `map_mul` `MonoidHomClass.toMulHomClass` `MulEquivClass.instMonoidHomClass` `MulEquiv.instMulEquivClass` `Commute.symm` `IsMulCentral.comm`
`centerCongr_apply_coe` 📖	mathematical	—	`Subsemigroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `MulEquiv` `Subgroup` `instSetLike` `center` `mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `centerCongr`	—	—
`centerCongr_symm_apply_coe` 📖	mathematical	—	`Subsemigroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `MulEquiv` `Subgroup` `instSetLike` `center` `mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `centerCongr`	—	—
`centerToMulOpposite_apply_coe` 📖	mathematical	—	`MulOpposite` `Subsemigroup` `MulOpposite.instMul` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `MulEquiv` `Subgroup` `instSetLike` `center` `MulOpposite.instGroup` `mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `centerToMulOpposite` `MulOpposite.op`	—	—
`centerToMulOpposite_symm_apply_coe` 📖	mathematical	—	`Subsemigroup` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid` `SetLike.instMembership` `Subsemigroup.instSetLike` `Subsemigroup.center` `DFunLike.coe` `MulEquiv` `MulOpposite` `Subgroup` `MulOpposite.instGroup` `instSetLike` `center` `mul` `EquivLike.toFunLike` `MulEquiv.instEquivLike` `MulEquiv.symm` `centerToMulOpposite` `MulOpposite.unop` `MulOpposite.instMul`	—	—
`center_le_normalizer` 📖	mathematical	—	`Subgroup` `Preorder.toLE` `PartialOrder.toPreorder` `instPartialOrder` `center` `normalizer`	—	`mem_center_iff` `mul_assoc` `mul_inv_cancel` `mul_one`
`center_toSubmonoid` 📖	mathematical	—	`toSubmonoid` `center` `Submonoid.center` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`coe_center` 📖	mathematical	—	`SetLike.coe` `Subgroup` `instSetLike` `center` `Set.center` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	—
`instNormalCenter` 📖	mathematical	—	`Normal` `center`	—	`mem_center_iff` `mul_assoc` `mul_inv_cancel` `mul_one`
`mem_center_iff` 📖	mathematical	—	`Subgroup` `SetLike.instMembership` `instSetLike` `center` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	—	`Semigroup.mem_center_iff`

Subgroup.center

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isMulCommutative` 📖	mathematical	—	`IsMulCommutative` `Subgroup` `SetLike.instMembership` `Subgroup.instSetLike` `Subgroup.center` `Subgroup.mul`	—	`Commute.symm` `IsMulCentral.comm`

---

← Back to Index