Documentation
LeanOA
.
Mathlib
.
Algebra
.
Group
.
Idempotent
Search
return to top
source
Imports
Init
Mathlib.Algebra.Group.Idempotent
Imported by
IsIdempotentElem
.
idempotent_mul_mul
source
theorem
IsIdempotentElem
.
idempotent_mul_mul
{
M
:
Type
u_1}
[
Semigroup
M
]
{
e
:
M
}
(
he
:
IsIdempotentElem
e
)
:
(
(fun (
x
:
M
) =>
e
*
x
*
e
)
∘
fun (
x
:
M
) =>
e
*
x
*
e
)
=
fun (
x
:
M
) =>
e
*
x
*
e