Documentation
Mathlib
.
Algebra
.
Group
.
Submonoid
.
Finsupp
Search
return to top
source
Imports
Init
Mathlib.Algebra.BigOperators.Finsupp
Imported by
Submonoid
.
exists_finsupp_of_mem_closure_range
AddSubmonoid
.
exists_finsupp_of_mem_closure_range
Submonoid
.
mem_closure_range_iff
AddSubmonoid
.
mem_closure_range_iff
Submonoid
.
exists_of_mem_closure_range
AddSubmonoid
.
exists_of_mem_closure_range
Submonoid
.
mem_closure_range_iff_of_fintype
AddSubmonoid
.
mem_closure_range_iff_of_fintype
Connection between
Submonoid.closure
and
Finsupp.prod
#
source
theorem
Submonoid
.
exists_finsupp_of_mem_closure_range
{M :
Type
u_1}
[
CommMonoid
M
]
{ι :
Type
u_2}
(f :
ι
→
M
)
(x :
M
)
(hx :
x
∈
closure
(
Set.range
f
)
)
:
∃ (
a
:
ι
→₀
ℕ
),
x
=
a
.prod
fun (
x1
:
ι
) (
x2
:
ℕ
) =>
f
x1
^
x2
source
theorem
AddSubmonoid
.
exists_finsupp_of_mem_closure_range
{M :
Type
u_1}
[
AddCommMonoid
M
]
{ι :
Type
u_2}
(f :
ι
→
M
)
(x :
M
)
(hx :
x
∈
closure
(
Set.range
f
)
)
:
∃ (
a
:
ι
→₀
ℕ
),
x
=
a
.sum
fun (
x1
:
ι
) (
x2
:
ℕ
) =>
x2
•
f
x1
source
theorem
Submonoid
.
mem_closure_range_iff
{M :
Type
u_1}
[
CommMonoid
M
]
{ι :
Type
u_2}
{f :
ι
→
M
}
{x :
M
}
:
x
∈
closure
(
Set.range
f
)
↔
∃ (
a
:
ι
→₀
ℕ
),
x
=
a
.prod
fun (
x1
:
ι
) (
x2
:
ℕ
) =>
f
x1
^
x2
source
theorem
AddSubmonoid
.
mem_closure_range_iff
{M :
Type
u_1}
[
AddCommMonoid
M
]
{ι :
Type
u_2}
{f :
ι
→
M
}
{x :
M
}
:
x
∈
closure
(
Set.range
f
)
↔
∃ (
a
:
ι
→₀
ℕ
),
x
=
a
.sum
fun (
x1
:
ι
) (
x2
:
ℕ
) =>
x2
•
f
x1
source
theorem
Submonoid
.
exists_of_mem_closure_range
{M :
Type
u_1}
[
CommMonoid
M
]
{ι :
Type
u_2}
(f :
ι
→
M
)
(x :
M
)
[
Fintype
ι
]
(hx :
x
∈
closure
(
Set.range
f
)
)
:
∃ (
a
:
ι
→
ℕ
),
x
=
∏
i
:
ι
,
f
i
^
a
i
source
theorem
AddSubmonoid
.
exists_of_mem_closure_range
{M :
Type
u_1}
[
AddCommMonoid
M
]
{ι :
Type
u_2}
(f :
ι
→
M
)
(x :
M
)
[
Fintype
ι
]
(hx :
x
∈
closure
(
Set.range
f
)
)
:
∃ (
a
:
ι
→
ℕ
),
x
=
∑
i
:
ι
,
a
i
•
f
i
source
theorem
Submonoid
.
mem_closure_range_iff_of_fintype
{M :
Type
u_1}
[
CommMonoid
M
]
{ι :
Type
u_2}
{f :
ι
→
M
}
{x :
M
}
[
Fintype
ι
]
:
x
∈
closure
(
Set.range
f
)
↔
∃ (
a
:
ι
→
ℕ
),
x
=
∏
i
:
ι
,
f
i
^
a
i
source
theorem
AddSubmonoid
.
mem_closure_range_iff_of_fintype
{M :
Type
u_1}
[
AddCommMonoid
M
]
{ι :
Type
u_2}
{f :
ι
→
M
}
{x :
M
}
[
Fintype
ι
]
:
x
∈
closure
(
Set.range
f
)
↔
∃ (
a
:
ι
→
ℕ
),
x
=
∑
i
:
ι
,
a
i
•
f
i