Documentation
Mathlib
.
Algebra
.
Ring
.
Center
Search
return to top
source
Imports
Init
Mathlib.Algebra.Group.Center
Mathlib.Data.Int.Cast.Lemmas
Imported by
Set
.
natCast_mem_center
Set
.
ofNat_mem_center
Set
.
intCast_mem_center
Set
.
add_mem_center
Set
.
neg_mem_center
Centers of rings
#
source
@[simp]
theorem
Set
.
natCast_mem_center
(M :
Type
u_1)
[
NonAssocSemiring
M
]
(n :
ℕ
)
:
↑
n
∈
center
M
source
@[simp]
theorem
Set
.
ofNat_mem_center
(M :
Type
u_1)
[
NonAssocSemiring
M
]
(n :
ℕ
)
[
n
.
AtLeastTwo
]
:
OfNat.ofNat
n
∈
center
M
source
@[simp]
theorem
Set
.
intCast_mem_center
(M :
Type
u_1)
[
NonAssocRing
M
]
(n :
ℤ
)
:
↑
n
∈
center
M
source
@[simp]
theorem
Set
.
add_mem_center
{M :
Type
u_1}
[
Distrib
M
]
{a b :
M
}
(ha :
a
∈
center
M
)
(hb :
b
∈
center
M
)
:
a
+
b
∈
center
M
source
@[simp]
theorem
Set
.
neg_mem_center
{M :
Type
u_1}
[
NonUnitalNonAssocRing
M
]
{a :
M
}
(ha :
a
∈
center
M
)
:
-
a
∈
center
M