Center

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

Statistics

Metric	Count
Definitions	0
Theorems center_units_eq, center_units_subset, div_mem_centralizer₀, inv_mem_centralizer₀, zero_mem_center, zero_mem_centralizer	6
Total	6

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
center_units_eq 📖	mathematical	—	center Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero Units.instMul preimage Units.val MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	—	HasSubset.Subset.antisymm instAntisymmSubset center_units_subset subset_center_units
center_units_subset 📖	mathematical	—	Set Units MonoidWithZero.toMonoid GroupWithZero.toMonoidWithZero instHasSubset center Units.instMul preimage Units.val MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass	—	eq_or_ne MulZeroClass.zero_mul MulZeroClass.mul_zero
div_mem_centralizer₀ 📖	mathematical	Set instMembership centralizer MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	DivInvMonoid.toDiv GroupWithZero.toDivInvMonoid	—	div_eq_mul_inv mul_mem_centralizer inv_mem_centralizer₀
inv_mem_centralizer₀ 📖	mathematical	Set instMembership centralizer MulZeroClass.toMul MulZeroOneClass.toMulZeroClass MonoidWithZero.toMulZeroOneClass GroupWithZero.toMonoidWithZero	InvOneClass.toInv DivInvOneMonoid.toInvOneClass DivisionMonoid.toDivInvOneMonoid GroupWithZero.toDivisionMonoid	—	eq_or_ne inv_zero zero_mem_centralizer mul_inv_eq_iff_eq_mul₀ mul_assoc eq_inv_mul_iff_mul_eq₀
zero_mem_center 📖	mathematical	—	Set instMembership center MulZeroClass.toMul MulZeroClass.toZero	—	commute_iff_eq MulZeroClass.zero_mul MulZeroClass.mul_zero
zero_mem_centralizer 📖	mathematical	—	Set instMembership centralizer MulZeroClass.toMul MulZeroClass.toZero	—	MulZeroClass.mul_zero MulZeroClass.zero_mul

---

← Back to Index