English
One can lift a basis of M to a basis of SymmetricAlgebra R M by transporting the monomial basis of MvPolynomial κ R through the inverse of the mv-polynomial equivalence.
Русский
Базис элемента M можно перенести на симметрическую алгебру, переведя базис мономиальных элементов MvPolynomial κ R через обратную сторону эквивалентности mvPolynomial.
LaTeX
$$$\text{Basis}_{\text{symmetricAlgebra}}\;b := (MvPolynomial.basisMonomials κ R).map( (\equivMvPolynomial b)^{-1}.toLinearEquiv )$$$
Lean4
/-- A basis on `M` can be lifted to a basis on `SymmetricAlgebra R M`. -/
@[simps! repr_apply]
noncomputable def _root_.Module.Basis.symmetricAlgebra (b : Basis κ R M) : Basis (κ →₀ ℕ) R (SymmetricAlgebra R M) :=
(MvPolynomial.basisMonomials κ R).map <| (SymmetricAlgebra.equivMvPolynomial b).symm.toLinearEquiv
