Center

📁 Source: Mathlib/Algebra/Group/Center.lean

Statistics

Metric	Count
Definitions `IsAddCentral`, `IsMulCentral`, `addCenter`, `addCentralizer`, `center`, `centralizer`, `decidableMemAddCenter`, `decidableMemAddCentralizer`, `decidableMemCenter`, `decidableMemCentralizer`	10
Theorems `mem_center_iff`, `comm`, `left_assoc`, `left_comm`, `mid_assoc`, `right_assoc`, `right_comm`, `comm`, `left_assoc`, `left_comm`, `mid_assoc`, `right_assoc`, `right_comm`, `mem_center_iff`, `addCenter_eq_univ`, `addCenter_pi`, `addCenter_prod`, `addCenter_subset_addCentralizer`, `addCentralizer_addCentralizer_addCentralizer`, `addCentralizer_addCentralizer_comm_of_comm`, `addCentralizer_empty`, `addCentralizer_eq_top_iff_subset`, `addCentralizer_eq_univ`, `addCentralizer_prod`, `addCentralizer_subset`, `addCentralizer_union`, `addCentralizer_univ`, `addUnits_neg_mem_center`, `add_mem_addCenter`, `add_mem_addCentralizer`, `center_eq_univ`, `center_pi`, `center_prod`, `center_subset_centralizer`, `centralizer_centralizer_centralizer`, `centralizer_centralizer_comm_of_comm`, `centralizer_empty`, `centralizer_eq_top_iff_subset`, `centralizer_eq_univ`, `centralizer_prod`, `centralizer_subset`, `centralizer_union`, `centralizer_univ`, `div_mem_center`, `div_mem_centralizer`, `invOf_mem_center`, `inv_mem_center`, `inv_mem_centralizer`, `mem_addCenter_iff`, `mem_addCentralizer`, `mem_center_iff`, `mem_centralizer_iff`, `mul_mem_center`, `mul_mem_centralizer`, `neg_mem_addCenter`, `neg_mem_addCentralizer`, `one_mem_center`, `one_mem_centralizer`, `prod_addCentralizer_subset_addCentralizer_prod`, `prod_centralizer_subset_centralizer_prod`, `sub_mem_addCenter`, `sub_mem_addCentralizer`, `subset_addCenter_add_units`, `subset_addCentralizer_addCentralizer`, `subset_center_units`, `subset_centralizer_centralizer`, `units_inv_mem_center`, `zero_mem_addCenter`, `zero_mem_addCentralizer`, `isAddCentral_iff`, `isMulCentral_iff`	71
Total	81

AddSemigroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_center_iff` 📖	mathematical	—	`Set` `Set.instMembership` `Set.addCenter` `toAdd`	—	`IsAddCentral.comm` `add_assoc`

IsAddCentral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comm` 📖	mathematical	`IsAddCentral`	`AddCommute`	—	—
`left_assoc` 📖	—	`IsAddCentral`	—	—	—
`left_comm` 📖	—	`IsAddCentral`	—	—	`AddCommute.eq` `comm` `right_assoc`
`mid_assoc` 📖	—	`IsAddCentral`	—	—	`comm` `right_assoc` `left_assoc`
`right_assoc` 📖	—	`IsAddCentral`	—	—	—
`right_comm` 📖	—	`IsAddCentral`	—	—	`right_assoc` `mid_assoc` `AddCommute.eq` `comm`

IsMulCentral

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`comm` 📖	mathematical	`IsMulCentral`	`Commute`	—	—
`left_assoc` 📖	—	`IsMulCentral`	—	—	—
`left_comm` 📖	—	`IsMulCentral`	—	—	`Commute.eq` `comm` `right_assoc`
`mid_assoc` 📖	—	`IsMulCentral`	—	—	`comm` `right_assoc` `left_assoc`
`right_assoc` 📖	—	`IsMulCentral`	—	—	—
`right_comm` 📖	—	`IsMulCentral`	—	—	`right_assoc` `mid_assoc` `Commute.eq` `comm`

Semigroup

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`mem_center_iff` 📖	mathematical	—	`Set` `Set.instMembership` `Set.center` `toMul`	—	`IsMulCentral.comm` `mul_assoc`

Set

Definitions

Name	Category	Theorems
`addCenter` 📖	CompOp	15 math math: `mem_addCenter_iff`, `AddSemigroup.mem_center_iff`, `zero_mem_addCenter`, `AddOpposite.unop_mem_center_iff`, `addCenter_prod`, `addCentralizer_univ`, `addCenter_eq_univ`, `AddSubgroup.coe_center`, `AddOpposite.op_mem_center_iff`, `subset_addCenter_add_units`, `addCenter_pi`, `addCentralizer_eq_top_iff_subset`, `AddSubmonoid.coe_center`, `addCenter_subset_addCentralizer`, `AddEquivClass.apply_mem_center_iff`
`addCentralizer` 📖	CompOp	16 math math: `addCentralizer_eq_univ`, `AddSubmonoid.centralizer_centralizer_centralizer`, `AddSubmonoid.coe_centralizer`, `zero_mem_addCentralizer`, `addCentralizer_univ`, `addCentralizer_empty`, `addCentralizer_subset`, `AddSubsemigroup.coe_centralizer`, `addCentralizer_prod`, `prod_addCentralizer_subset_addCentralizer_prod`, `addCentralizer_eq_top_iff_subset`, `subset_addCentralizer_addCentralizer`, `addCenter_subset_addCentralizer`, `addCentralizer_union`, `addCentralizer_addCentralizer_addCentralizer`, `mem_addCentralizer`
`center` 📖	CompOp	32 math math: `center_units_subset`, `mem_center_iff_addMonoidHom`, `Module.Basis.mem_center_iff`, `Matrix.center_eq_range`, `MulOpposite.op_mem_center_iff`, `one_mem_center`, `Submonoid.coe_center`, `center_eq_univ`, `centralizer_eq_top_iff_subset`, `NonUnitalSubsemiring.coe_center`, `Semigroup.mem_center_iff`, `Module.End.mem_center_iff`, `mem_center_iff`, `MulEquivClass.apply_mem_center_iff`, `center_prod`, `NonUnitalSubring.coe_center`, `NonUnitalStarSubalgebra.coe_center`, `NonUnitalSubalgebra.coe_center`, `algebraMap_mem_center`, `Subgroup.coe_center`, `intCast_mem_center`, `MulOpposite.unop_mem_center_iff`, `subset_center_units`, `center_units_eq`, `center_subset_centralizer`, `Subring.coe_center`, `center_pi`, `ofNat_mem_center`, `natCast_mem_center`, `centralizer_univ`, `zero_mem_center`, `Matrix.center_eq_scalar_image`
`centralizer` 📖	CompOp	34 math math: `algebraMap_mem_centralizer`, `star_centralizer`, `Subsemiring.centralizer_centralizer_centralizer`, `centralizer_eq_univ`, `centralizer_centralizer_centralizer`, `centralizer_prod`, `Subsemigroup.coe_centralizer`, `centralizer_eq_top_iff_subset`, `VonNeumannAlgebra.centralizer_centralizer'`, `VonNeumannAlgebra.centralizer_centralizer`, `NonUnitalStarSubalgebra.coe_centralizer`, `zero_mem_centralizer`, `Subalgebra.centralizer_centralizer_centralizer`, `centralizer_subset`, `mem_centralizer_iff`, `Subsemiring.coe_centralizer`, `NonUnitalSubalgebra.coe_centralizer`, `NonUnitalSubsemiring.coe_centralizer`, `StarSubalgebra.coe_centralizer_centralizer`, `NonUnitalStarSubalgebra.coe_centralizer_centralizer`, `subset_centralizer_centralizer`, `one_mem_centralizer`, `Submonoid.centralizer_centralizer_centralizer`, `centralizer_empty`, `StarSubalgebra.coe_centralizer`, `isClosed_centralizer`, `VonNeumannAlgebra.coe_commutant`, `centralizer_union`, `center_subset_centralizer`, `prod_centralizer_subset_centralizer_prod`, `Submonoid.coe_centralizer`, `Subalgebra.coe_centralizer`, `Subring.coe_centralizer`, `centralizer_univ`
`decidableMemAddCenter` 📖	CompOp	—
`decidableMemAddCentralizer` 📖	CompOp	—
`decidableMemCenter` 📖	CompOp	—
`decidableMemCentralizer` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`addCenter_eq_univ` 📖	mathematical	—	`addCenter` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `univ`	—	`Subset.antisymm` `subset_univ` `AddSemigroup.mem_center_iff` `add_comm`
`addCenter_pi` 📖	mathematical	—	`addCenter` `Pi.instAdd` `pi` `univ`	—	`ext` `mem_addCenter_iff` `isAddCentral_iff` `addCommute_iff_eq` `mem_pi` `mem_univ` `forall_true_left` `Function.update_self`
`addCenter_prod` 📖	mathematical	—	`addCenter` `Prod.instAdd` `SProd.sprod` `Set` `instSProd`	—	`ext` `mem_addCenter_iff` `isAddCentral_iff` `addCommute_iff_eq` `mem_prod`
`addCenter_subset_addCentralizer` 📖	mathematical	—	`Set` `instHasSubset` `addCenter` `addCentralizer`	—	`AddCommute.symm` `IsAddCentral.comm`
`addCentralizer_addCentralizer_addCentralizer` 📖	mathematical	—	`addCentralizer`	—	`Subset.antisymm` `subset_addCentralizer_addCentralizer`
`addCentralizer_addCentralizer_comm_of_comm` 📖	—	`Set` `instMembership` `addCentralizer`	—	—	—
`addCentralizer_empty` 📖	mathematical	—	`addCentralizer` `Set` `instEmptyCollection` `Top.top` `OrderTop.toTop` `instLE` `BoundedOrder.toOrderTop` `instBoundedOrder`	—	`mem_empty_iff_false` `IsEmpty.forall_iff` `instIsEmptyFalse`
`addCentralizer_eq_top_iff_subset` 📖	mathematical	—	`addCentralizer` `AddSemigroup.toAdd` `univ` `Set` `instHasSubset` `addCenter`	—	`eq_top_iff` `AddSemigroup.mem_center_iff` `IsAddCentral.comm`
`addCentralizer_eq_univ` 📖	mathematical	—	`addCentralizer` `AddCommMagma.toAdd` `AddCommSemigroup.toAddCommMagma` `univ`	—	`eq_univ_of_forall` `add_comm`
`addCentralizer_prod` 📖	mathematical	`Nonempty`	`addCentralizer` `SProd.sprod` `Set` `instSProd` `Prod.instAdd`	—	`ext` `mem_addCentralizer` `mem_prod`
`addCentralizer_subset` 📖	mathematical	`Set` `instHasSubset`	`addCentralizer`	—	—
`addCentralizer_union` 📖	mathematical	—	`addCentralizer` `Set` `instUnion` `instInter`	—	`mem_union`
`addCentralizer_univ` 📖	mathematical	—	`addCentralizer` `univ` `AddSemigroup.toAdd` `addCenter`	—	`Subset.antisymm` `AddSemigroup.mem_center_iff` `mem_univ` `AddCommute.symm` `IsAddCentral.comm`
`addUnits_neg_mem_center` 📖	mathematical	`Set` `instMembership` `addCenter` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddUnits.val`	`AddUnits` `AddUnits.instNeg`	—	`AddSemigroup.mem_center_iff` `AddCommute.addUnits_neg_right`
`add_mem_addCenter` 📖	—	`Set` `instMembership` `addCenter`	—	—	`mem_addCenter_iff` `isAddCentral_iff` `addCommute_iff_eq`
`add_mem_addCentralizer` 📖	—	`Set` `instMembership` `addCentralizer` `AddSemigroup.toAdd`	—	—	`add_assoc`
`center_eq_univ` 📖	mathematical	—	`center` `CommMagma.toMul` `CommSemigroup.toCommMagma` `univ`	—	`Subset.antisymm` `subset_univ` `Semigroup.mem_center_iff` `mul_comm`
`center_pi` 📖	mathematical	—	`center` `Pi.instMul` `pi` `univ`	—	`ext` `Function.update_self`
`center_prod` 📖	mathematical	—	`center` `Prod.instMul` `SProd.sprod` `Set` `instSProd`	—	`ext`
`center_subset_centralizer` 📖	mathematical	—	`Set` `instHasSubset` `center` `centralizer`	—	`Commute.symm` `IsMulCentral.comm`
`centralizer_centralizer_centralizer` 📖	mathematical	—	`centralizer`	—	`Subset.antisymm` `subset_centralizer_centralizer`
`centralizer_centralizer_comm_of_comm` 📖	—	`Set` `instMembership` `centralizer`	—	—	—
`centralizer_empty` 📖	mathematical	—	`centralizer` `Set` `instEmptyCollection` `Top.top` `OrderTop.toTop` `instLE` `BoundedOrder.toOrderTop` `instBoundedOrder`	—	`instIsEmptyFalse`
`centralizer_eq_top_iff_subset` 📖	mathematical	—	`centralizer` `Semigroup.toMul` `univ` `Set` `instHasSubset` `center`	—	`eq_top_iff` `Semigroup.mem_center_iff` `IsMulCentral.comm`
`centralizer_eq_univ` 📖	mathematical	—	`centralizer` `CommMagma.toMul` `CommSemigroup.toCommMagma` `univ`	—	`eq_univ_of_forall` `mul_comm`
`centralizer_prod` 📖	mathematical	`Nonempty`	`centralizer` `SProd.sprod` `Set` `instSProd` `Prod.instMul`	—	`ext`
`centralizer_subset` 📖	mathematical	`Set` `instHasSubset`	`centralizer`	—	—
`centralizer_union` 📖	mathematical	—	`centralizer` `Set` `instUnion` `instInter`	—	—
`centralizer_univ` 📖	mathematical	—	`centralizer` `univ` `Semigroup.toMul` `center`	—	`Subset.antisymm` `Semigroup.mem_center_iff` `mem_univ` `Commute.symm` `IsMulCentral.comm`
`div_mem_center` 📖	mathematical	`Set` `instMembership` `center` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid`	`DivInvMonoid.toDiv`	—	`div_eq_mul_inv` `mul_mem_center` `inv_mem_center`
`div_mem_centralizer` 📖	mathematical	`Set` `instMembership` `centralizer` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`DivInvMonoid.toDiv`	—	`div_eq_mul_inv` `mul_mem_centralizer` `inv_mem_centralizer`
`invOf_mem_center` 📖	mathematical	`Set` `instMembership` `center` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass`	`Invertible.invOf` `MulOne.toOne`	—	`Semigroup.mem_center_iff` `Commute.invOf_right`
`inv_mem_center` 📖	mathematical	`Set` `instMembership` `center` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `DivisionMonoid.toDivInvMonoid`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid`	—	`Semigroup.mem_center_iff` `mul_inv_rev` `inv_inv` `IsMulCentral.comm`
`inv_mem_centralizer` 📖	mathematical	`Set` `instMembership` `centralizer` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `DivInvMonoid.toMonoid` `Group.toDivInvMonoid`	`InvOneClass.toInv` `DivInvOneMonoid.toInvOneClass` `DivisionMonoid.toDivInvOneMonoid` `Group.toDivisionMonoid`	—	`mul_inv_eq_iff_eq_mul` `mul_assoc` `eq_inv_mul_iff_mul_eq`
`mem_addCenter_iff` 📖	mathematical	—	`Set` `instMembership` `addCenter` `IsAddCentral`	—	—
`mem_addCentralizer` 📖	mathematical	—	`Set` `instMembership` `addCentralizer`	—	—
`mem_center_iff` 📖	mathematical	—	`Set` `instMembership` `center` `IsMulCentral`	—	—
`mem_centralizer_iff` 📖	mathematical	—	`Set` `instMembership` `centralizer`	—	—
`mul_mem_center` 📖	—	`Set` `instMembership` `center`	—	—	—
`mul_mem_centralizer` 📖	—	`Set` `instMembership` `centralizer` `Semigroup.toMul`	—	—	`mul_assoc`
`neg_mem_addCenter` 📖	mathematical	`Set` `instMembership` `addCenter` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid`	—	`AddSemigroup.mem_center_iff` `neg_add_rev` `neg_neg` `IsAddCentral.comm`
`neg_mem_addCentralizer` 📖	mathematical	`Set` `instMembership` `addCentralizer` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`NegZeroClass.toNeg` `SubNegZeroMonoid.toNegZeroClass` `SubtractionMonoid.toSubNegZeroMonoid` `AddGroup.toSubtractionMonoid`	—	`add_neg_eq_iff_eq_add` `add_assoc` `eq_neg_add_iff_add_eq`
`one_mem_center` 📖	mathematical	—	`Set` `instMembership` `center` `MulOne.toMul` `MulOneClass.toMulOne` `MulOne.toOne`	—	`commute_iff_eq` `one_mul` `mul_one`
`one_mem_centralizer` 📖	mathematical	—	`Set` `instMembership` `centralizer` `MulOne.toMul` `MulOneClass.toMulOne` `MulOne.toOne`	—	`mul_one` `one_mul`
`prod_addCentralizer_subset_addCentralizer_prod` 📖	mathematical	—	`Set` `instHasSubset` `SProd.sprod` `instSProd` `addCentralizer` `Prod.instAdd`	—	`mem_prod` `mem_addCentralizer`
`prod_centralizer_subset_centralizer_prod` 📖	mathematical	—	`Set` `instHasSubset` `SProd.sprod` `instSProd` `centralizer` `Prod.instMul`	—	—
`sub_mem_addCenter` 📖	mathematical	`Set` `instMembership` `addCenter` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `SubtractionMonoid.toSubNegMonoid`	`SubNegMonoid.toSub`	—	`sub_eq_add_neg` `add_mem_addCenter` `neg_mem_addCenter`
`sub_mem_addCentralizer` 📖	mathematical	`Set` `instMembership` `addCentralizer` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `SubNegMonoid.toAddMonoid` `AddGroup.toSubNegMonoid`	`SubNegMonoid.toSub`	—	`sub_eq_add_neg` `add_mem_addCentralizer` `neg_mem_addCentralizer`
`subset_addCenter_add_units` 📖	mathematical	—	`Set` `AddUnits` `instHasSubset` `preimage` `AddUnits.val` `addCenter` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddMonoid.toAddZeroClass` `AddUnits.instAdd`	—	`AddSemigroup.mem_center_iff` `AddUnits.val_add` `IsAddCentral.comm`
`subset_addCentralizer_addCentralizer` 📖	mathematical	—	`Set` `instHasSubset` `addCentralizer`	—	—
`subset_center_units` 📖	mathematical	—	`Set` `Units` `instHasSubset` `preimage` `Units.val` `center` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Units.instMul`	—	`Semigroup.mem_center_iff` `Units.val_mul` `IsMulCentral.comm`
`subset_centralizer_centralizer` 📖	mathematical	—	`Set` `instHasSubset` `centralizer`	—	—
`units_inv_mem_center` 📖	mathematical	`Set` `instMembership` `center` `MulOne.toMul` `MulOneClass.toMulOne` `Monoid.toMulOneClass` `Units.val`	`Units` `Units.instInv`	—	`Semigroup.mem_center_iff` `Commute.units_inv_right`
`zero_mem_addCenter` 📖	mathematical	—	`Set` `instMembership` `addCenter` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddZero.toZero`	—	`addCommute_iff_eq` `zero_add` `add_zero`
`zero_mem_addCentralizer` 📖	mathematical	—	`Set` `instMembership` `addCentralizer` `AddZero.toAdd` `AddZeroClass.toAddZero` `AddZero.toZero`	—	`mem_addCentralizer` `add_zero` `zero_add`

(root)

Definitions

Name	Category	Theorems
`IsAddCentral` 📖	CompData	2 math math: `Set.mem_addCenter_iff`, `isAddCentral_iff`
`IsMulCentral` 📖	CompData	2 math math: `isMulCentral_iff`, `Set.mem_center_iff`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`isAddCentral_iff` 📖	mathematical	—	`IsAddCentral` `AddCommute`	—	—
`isMulCentral_iff` 📖	mathematical	—	`IsMulCentral` `Commute`	—	—

---

← Back to Index