Documentation
Toric
.
Mathlib
.
Algebra
.
MonoidAlgebra
.
Module
Search
return to top
source
Imports
Init
Mathlib.Algebra.MonoidAlgebra.Module
Mathlib.LinearAlgebra.Finsupp.LinearCombination
Imported by
MonoidAlgebra
.
linearCombination_of
AddMonoidAlgebra
.
linearCombination_of
source
@[simp]
theorem
MonoidAlgebra
.
linearCombination_of
{
R
:
Type
u_1}
{
M
:
Type
u_2}
[
Semiring
R
]
[
MulOneClass
M
]
:
Finsupp.linearCombination
R
⇑
(
of
R
M
)
=
LinearMap.id
source
@[simp]
theorem
AddMonoidAlgebra
.
linearCombination_of
{
R
:
Type
u_1}
{
M
:
Type
u_2}
[
Semiring
R
]
[
AddZeroClass
M
]
:
Finsupp.linearCombination
R
⇑
(
of
R
M
)
=
LinearMap.id