Commit 2021-02-22 17:14 4daac664

View on Github →

chore(field_theory/mv_polynomial): generalised to comm_ring and module doc (#6341) This PR generalises most of field_theory/mv_polynomial from polynomial rings over fields to polynomial rings over commutative rings. This is put into a separate file. Also renamed the field to K and did one tiny golf.

Estimated changes

Modified src/field_theory/mv_polynomial.lean

modified theorem mv_polynomial.dim_mv_polynomial

deleted theorem mv_polynomial.is_basis_monomials

deleted theorem mv_polynomial.map_range_eq_map

deleted theorem mv_polynomial.mem_restrict_degree

deleted theorem mv_polynomial.mem_restrict_degree_iff_sup

deleted theorem mv_polynomial.mem_restrict_total_degree

modified theorem mv_polynomial.quotient_mk_comp_C_injective

deleted def mv_polynomial.restrict_degree

deleted def mv_polynomial.restrict_total_degree

Created src/ring_theory/mv_polynomial/basic.lean

added theorem mv_polynomial.is_basis_monomials

added theorem mv_polynomial.map_range_eq_map

added theorem mv_polynomial.mem_restrict_degree

added theorem mv_polynomial.mem_restrict_degree_iff_sup

added theorem mv_polynomial.mem_restrict_total_degree

added def mv_polynomial.restrict_degree

added def mv_polynomial.restrict_total_degree