feat(data/mv_polynomial): some lemmas on constant_coeff and rename (#…

…4231)

Snippet from the Witt project

Co-Authored-By: Rob Y. Lewis <rob.y.lewis@gmail.com>

src/data/mv_polynomial/basic.lean

@@ -506,6 +506,16 @@ lemma constant_coeff_monomial (d : σ →₀ ℕ) (r : R) :
   constant_coeff (monomial d r) = if d = 0 then r else 0 :=
 by rw [constant_coeff_eq, coeff_monomial]
 
+variables (σ R)
+
+@[simp] lemma constant_coeff_comp_C :
+  constant_coeff.comp (C : R →+* mv_polynomial σ R) = ring_hom.id R :=
+by { ext, apply constant_coeff_C }
+
+@[simp] lemma constant_coeff_comp_algebra_map :
+  constant_coeff.comp (algebra_map R (mv_polynomial σ R)) = ring_hom.id R :=
+constant_coeff_comp_C _ _
+
 end constant_coeff
 
 section as_sum

src/data/mv_polynomial/rename.lean

@@ -210,6 +210,15 @@ lemma coeff_rename_ne_zero (f : σ → τ) (φ : mv_polynomial σ R) (d : τ →
   ∃ u : σ →₀ ℕ, u.map_domain f = d ∧ φ.coeff u ≠ 0 :=
 by { contrapose! h, apply coeff_rename_eq_zero _ _ _ h }
 
+@[simp] lemma constant_coeff_rename {τ : Type*} (f : σ → τ) (φ : mv_polynomial σ R) :
+  constant_coeff (rename f φ) = constant_coeff φ :=
+begin
+  apply φ.induction_on,
+  { intro a, simp only [constant_coeff_C, rename_C]},
+  { intros p q hp hq, simp only [hp, hq, ring_hom.map_add, alg_hom.map_add] },
+  { intros p n hp, simp only [hp, rename_X, constant_coeff_X, ring_hom.map_mul, alg_hom.map_mul] }
+end
+
 end coeff
 
 end mv_polynomial