From b4cad37932a9475ae1cd1f014ea6e00a0d1848d5 Mon Sep 17 00:00:00 2001 From: negiizhao Date: Fri, 29 Apr 2022 06:35:25 +0000 Subject: [PATCH] chore(ring_theory/mv_polynomial/basic): golf (#13765) --- src/ring_theory/mv_polynomial/basic.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ring_theory/mv_polynomial/basic.lean b/src/ring_theory/mv_polynomial/basic.lean index 96d2d3134a810..1bd49bdd30719 100644 --- 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 :=