Documentation
LeanPool
.
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'
Pointwise set operations
#
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