Commit 2021-05-28 11:55 5fff3b19

View on Github →

feat(ring_theory/mv_polynomial/basic): add polynomial.basis_monomials (#7728) We add polynomial.basis_monomials : the monomials form a basis on polynomial R. Because of the structure of the import, it seems to me a little complicated to do it directly, so I use mv_polynomial.punit_alg_equiv

Estimated changes

Modified src/data/finsupp/basic.lean

modified def finsupp.equiv_fun_on_fintype

Modified src/data/polynomial/algebra_map.lean

modified theorem polynomial.C_eq_algebra_map

added def polynomial.to_finsupp_iso_alg

Modified src/data/polynomial/basic.lean

modified theorem polynomial.monomial_one_right_eq_X_pow

Modified src/data/polynomial/monomial.lean

Modified src/ring_theory/mv_polynomial/basic.lean

added theorem polynomial.coe_basis_monomials