Documentation
PFR
.
Mathlib
.
Algebra
.
Group
.
Action
.
Pointwise
.
Set
.
Basic
Search
return to top
source
Imports
Init
Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Imported by
Set
.
singleton_mul'
Set
.
singleton_add'
Set
.
mul_singleton'
Set
.
add_singleton'
source
theorem
Set
.
singleton_mul'
{
α
:
Type
u_1}
[
Mul
α
]
(
a
:
α
)
(
s
:
Set
α
)
:
{
a
}
*
s
=
a
•
s
source
theorem
Set
.
singleton_add'
{
α
:
Type
u_1}
[
Add
α
]
(
a
:
α
)
(
s
:
Set
α
)
:
{
a
}
+
s
=
a
+ᵥ
s
source
theorem
Set
.
mul_singleton'
{
α
:
Type
u_1}
[
Mul
α
]
(
s
:
Set
α
)
(
a
:
α
)
:
s
*
{
a
}
=
MulOpposite.op
a
•
s
source
theorem
Set
.
add_singleton'
{
α
:
Type
u_1}
[
Add
α
]
(
s
:
Set
α
)
(
a
:
α
)
:
s
+
{
a
}
=
AddOpposite.op
a
+ᵥ
s