Center

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

Statistics

Metric	Count
Definitions	0
Theorems add_mem_center, intCast_mem_center, natCast_mem_center, neg_mem_center, ofNat_mem_center	5
Total	5

Set

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
add_mem_center 📖	mathematical	Set instMembership center Distrib.toMul	Distrib.toAdd	—	commute_iff_eq add_mul Distrib.rightDistribClass mul_add Distrib.leftDistribClass IsMulCentral.comm IsMulCentral.left_assoc IsMulCentral.right_assoc
intCast_mem_center 📖	mathematical	—	Set instMembership center Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring NonAssocRing.toNonUnitalNonAssocRing AddGroupWithOne.toIntCast AddCommGroupWithOne.toAddGroupWithOne NonAssocRing.toAddCommGroupWithOne	—	commute_iff_eq Int.commute_cast Int.cast_natCast IsMulCentral.left_assoc natCast_mem_center Int.cast_negSucc Nat.cast_add Nat.cast_one neg_add_rev add_mul Distrib.rightDistribClass neg_mul one_mul AddLeftCancelSemigroup.toIsLeftCancelAdd IsMulCentral.right_assoc mul_add Distrib.leftDistribClass mul_neg mul_one
natCast_mem_center 📖	mathematical	—	Set instMembership center Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring AddMonoidWithOne.toNatCast AddCommMonoidWithOne.toAddMonoidWithOne NonAssocSemiring.toAddCommMonoidWithOne	—	commute_iff_eq Nat.commute_cast Nat.cast_zero MulZeroClass.zero_mul Nat.cast_succ add_mul Distrib.rightDistribClass one_mul MulZeroClass.mul_zero mul_add Distrib.leftDistribClass mul_one
neg_mem_center 📖	mathematical	Set instMembership center Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonUnitalNonAssocRing.toNonUnitalNonAssocSemiring	NegZeroClass.toNeg SubNegZeroMonoid.toNegZeroClass SubtractionMonoid.toSubNegZeroMonoid SubtractionCommMonoid.toSubtractionMonoid AddCommGroup.toDivisionAddCommMonoid NonUnitalNonAssocRing.toAddCommGroup	—	commute_iff_eq neg_mul_comm IsMulCentral.comm neg_mul IsMulCentral.left_assoc mul_neg IsMulCentral.right_assoc
ofNat_mem_center 📖	mathematical	—	Set instMembership center Distrib.toMul NonUnitalNonAssocSemiring.toDistrib NonAssocSemiring.toNonUnitalNonAssocSemiring	—	natCast_mem_center

---

← Back to Index