HepLean Documentation
Mathlib
.
Algebra
.
Ring
.
Centralizer
Search
Google site search
return to top
source
Imports
Init
Mathlib.Algebra.Group.Center
Mathlib.Algebra.Ring.Defs
Imported by
Set
.
add_mem_centralizer
Set
.
neg_mem_centralizer
Centralizers of rings
#
source
@[simp]
theorem
Set
.
add_mem_centralizer
{M :
Type
u_1}
{S :
Set
M
}
{a :
M
}
{b :
M
}
[
Distrib
M
]
(ha :
a
∈
S
.centralizer
)
(hb :
b
∈
S
.centralizer
)
:
a
+
b
∈
S
.centralizer
source
@[simp]
theorem
Set
.
neg_mem_centralizer
{M :
Type
u_1}
{S :
Set
M
}
{a :
M
}
[
Mul
M
]
[
HasDistribNeg
M
]
(ha :
a
∈
S
.centralizer
)
:
-
a
∈
S
.centralizer