chore(ring_theory/mv_polynomial/basic): golf (#13765)

leanprover-community · Apr 29, 2022 · b4cad37 · b4cad37
1 parent 5c1ee35
commit b4cad37
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/src/ring_theory/mv_polynomial/basic.lean b/src/ring_theory/mv_polynomial/basic.lean
@@ -125,7 +125,7 @@ namespace polynomial
 
 /-- The monomials form a basis on `polynomial R`. -/
 noncomputable def basis_monomials : basis ℕ R R[X] :=
-finsupp.basis_single_one.map (to_finsupp_iso_alg R).to_linear_equiv.symm
+basis.of_repr (to_finsupp_iso_alg R).to_linear_equiv
 
 @[simp] lemma coe_basis_monomials :
   (basis_monomials R : ℕ → R[X]) = λ s, monomial s 1 :=