feat(RingTheory/MvPolynomial/Ideal): introduce new lemmas about MvPolynomial Ideals

[archiebrowne]

Four new lemmas about MvPolynomialIdeals sub_span_span_sub, span_eq_iff_basis_sub, mem_basis_mem_span, mem_span_exists_dvd_mem_basis.

---

[github-actions]

PR summary ab19632c08

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

+ mem_basis_mem_span
+ mem_span_exists_dvd_mem_basis
+ span_eq_iff_basis_sub
+ sub_span_span_sub

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

[Ruben-VandeVelde]

Some stylistic comments, but no other objections from me.

[riccardobrasca]

mem_basis_mem_span seems essentially the same as Ideal.subset_span, and also the first two lemmas are essentially already in the library.

What about removing them and just keep the last one?

[riccardobrasca]

Suggested change

	/-- If a monomial `m` is contained in the span of a basis of monomials, there must be an
	/-- If a monomial `m` is contained in the span of a set of monomials, there must be an

[riccardobrasca]

@archiebrowne are you still interested in working on this PR?